Face and corner matching for targets in tableau row 3

theorem MacMahon.face_corner_30 (p : Pair) (k : Slot) : HasCorner p (cornerAt 3 0 k) ↔ ∃ (r : Fin 24), FaceFits (3, 0) p k r

theorem MacMahon.face_corner_31 (p : Pair) (k : Slot) : HasCorner p (cornerAt 3 1 k) ↔ ∃ (r : Fin 24), FaceFits (3, 1) p k r

theorem MacMahon.face_corner_32 (p : Pair) (k : Slot) : HasCorner p (cornerAt 3 2 k) ↔ ∃ (r : Fin 24), FaceFits (3, 2) p k r

theorem MacMahon.face_corner_34 (p : Pair) (k : Slot) : HasCorner p (cornerAt 3 4 k) ↔ ∃ (r : Fin 24), FaceFits (3, 4) p k r

theorem MacMahon.face_corner_35 (p : Pair) (k : Slot) : HasCorner p (cornerAt 3 5 k) ↔ ∃ (r : Fin 24), FaceFits (3, 5) p k r