Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: 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

pp: 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)

pp: 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)

Tactic:
<;>

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)