Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                        (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                        (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
                (F.mapCone c)).pt).hom ≫
        (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case none
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (F.mapCone c)).π.app
      none =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).pt).hom ≫
      (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app none

case some.left
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (F.mapCone c)).π.app
      (some WalkingPair.left) =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).pt).hom ≫
      (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app (some WalkingPair.left)

case some.right
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (F.mapCone c)).π.app
      (some WalkingPair.right) =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).pt).hom ≫
      (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app (some WalkingPair.right)