[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ (fun j => F.map (Bicone.ι b j)) j ≫ (fun j => F.map (Bicone.π b j)) j' =
    if h : j = j' then eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j') else 0
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j') = if h : j = j' then eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j') else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : j = j'
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j') = eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j')
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j) = eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j)
[PROOFSTEP]
simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]
[GOAL]
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ 𝟙 (F.obj (f j)) = 𝟙 ((F.obj ∘ f) j)
[PROOFSTEP]
dsimp
[GOAL]
case neg
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : ¬j = j'
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j') = 0
[PROOFSTEP]
rw [bicone_ι_π_ne _ h, F.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inl ≫ F.map b.fst = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← F.map_comp, b.inl_fst, F.map_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inl ≫ F.map b.snd = 0
[PROOFSTEP]
rw [← F.map_comp, b.inl_snd, F.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inr ≫ F.map b.fst = 0
[PROOFSTEP]
rw [← F.map_comp, b.inr_fst, F.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inr ≫ F.map b.snd = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← F.map_comp, b.inr_snd, F.map_id]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBiproducts F
J : Type
x✝ : Fintype J
⊢ PreservesBiproductsOfShape J F
[PROOFSTEP]
letI := preservesBiproductsShrink.{0} F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBiproducts F
J : Type
x✝ : Fintype J
this : PreservesBiproducts F := preservesBiproductsShrink F
⊢ PreservesBiproductsOfShape J F
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
          (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).π
      j =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom ≫
      NatTrans.app (BinaryBicone.toCone (mapBinaryBicone F b)).π j
[PROOFSTEP]
rcases j with ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
          (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).π
      { as := WalkingPair.left } =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom ≫
      NatTrans.app (BinaryBicone.toCone (mapBinaryBicone F b)).π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
          (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).π
      { as := WalkingPair.right } =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom ≫
      NatTrans.app (BinaryBicone.toCone (mapBinaryBicone F b)).π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
            (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom =
    NatTrans.app (BinaryBicone.toCocone (mapBinaryBicone F b)).ι j
[PROOFSTEP]
rcases j with ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
            (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).ι
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom =
    NatTrans.app (BinaryBicone.toCocone (mapBinaryBicone F b)).ι { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
            (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).ι
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom =
    NatTrans.app (BinaryBicone.toCocone (mapBinaryBicone F b)).ι { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
classical
ext
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
j✝¹ j✝ : J
⊢ biproduct.ι (F.obj ∘ f) j✝ ≫ (biproductComparison' F f ≫ biproductComparison F f) ≫ biproduct.π (F.obj ∘ f) j✝¹ =
    biproduct.ι (F.obj ∘ f) j✝ ≫ 𝟙 (⨁ F.obj ∘ f) ≫ biproduct.π (F.obj ∘ f) j✝¹
[PROOFSTEP]
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
[PROOFSTEP]
ext
[GOAL]
case h₀.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inl ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.fst =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
case h₀.h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inl ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.snd =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
case h₁.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inr ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.fst =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
case h₁.h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inr ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.snd =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
⊢ F.map (lift g) ≫ (mapBiproduct F f).hom = lift fun j => F.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (F.obj ∘ f) j = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) j
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j
[PROOFSTEP]
haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
this : HasBiproduct fun j => F.obj (f j)
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j
[PROOFSTEP]
simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ (mapBiproduct F f).inv ≫ F.map (desc g) = desc fun j => F.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (F.obj ∘ f) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
[PROOFSTEP]
haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
this : HasBiproduct fun j => F.obj (f j)
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
[PROOFSTEP]
simp only [mapBiproduct_inv, ← Category.assoc, biproduct.ι_desc, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ((mapBiproduct F f).hom ≫ desc fun j => F.map (g j)) = F.map (desc g)
[PROOFSTEP]
rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) ≫ (mapBiprod F X Y).hom = lift (F.map f) (F.map g)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ (F.map (lift f g) ≫ (mapBiprod F X Y).hom) ≫ fst = lift (F.map f) (F.map g) ≫ fst
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ (F.map (lift f g) ≫ (mapBiprod F X Y).hom) ≫ snd = lift (F.map f) (F.map g) ≫ snd
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ lift (F.map f) (F.map g) ≫ (mapBiprod F X Y).inv = F.map (lift f g)
[PROOFSTEP]
rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (mapBiprod F X Y).inv ≫ F.map (desc f g) = desc (F.map f) (F.map g)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ inl ≫ (mapBiprod F X Y).inv ≫ F.map (desc f g) = inl ≫ desc (F.map f) (F.map g)
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ inr ≫ (mapBiprod F X Y).inv ≫ F.map (desc f g) = inr ≫ desc (F.map f) (F.map g)
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (mapBiprod F X Y).hom ≫ desc (F.map f) (F.map g) = F.map (desc f g)
[PROOFSTEP]
rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
⊢ HasLimitsOfShape (Discrete ι) C
[PROOFSTEP]
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasLimitsOfShape (Discrete ι) C
[PROOFSTEP]
haveI : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasLimitsOfShape (Discrete (Fin n)) C
⊢ HasLimitsOfShape (Discrete ι) C
[PROOFSTEP]
exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
⊢ HasColimitsOfShape (Discrete ι) C
[PROOFSTEP]
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape (Discrete ι) C
[PROOFSTEP]
haveI : HasColimitsOfShape (Discrete (Fin n)) C := HasFiniteCoproducts.out n
[GOAL]
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasColimitsOfShape (Discrete (Fin n)) C
⊢ HasColimitsOfShape (Discrete ι) C
[PROOFSTEP]
exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
J : ℕ
⊢ HasColimitsOfShape (Discrete (Fin J)) C
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ ∀ (j : WalkingCospan),
    NatTrans.app
        ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π j =
      (Iso.refl
            ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
                (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
        NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π j
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π none =
    (Iso.refl
          ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
              (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
      NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π none
[PROOFSTEP]
dsimp
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π
      (some WalkingPair.left) =
    (Iso.refl
          ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
              (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
      NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π
        (some WalkingPair.left)
[PROOFSTEP]
dsimp
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone (PullbackCone.mk h k comm))).π
      (some WalkingPair.right) =
    (Iso.refl
          ((Cones.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj
              (G.mapCone (PullbackCone.mk h k comm))).pt).hom ≫
      NatTrans.app (PullbackCone.mk (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)).π
        (some WalkingPair.right)
[PROOFSTEP]
dsimp
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map (h ≫ f) ≫ 𝟙 (G.obj Z) = 𝟙 (G.obj W) ≫ G.map h ≫ G.map f
[PROOFSTEP]
simp only [comp_id, id_comp, G.map_comp]
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map h ≫ 𝟙 (G.obj X) = 𝟙 (G.obj W) ≫ G.map h
[PROOFSTEP]
simp only [comp_id, id_comp, G.map_comp]
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map k ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj W) ≫ G.map k
[PROOFSTEP]
simp only [comp_id, id_comp, G.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
[PROOFSTEP]
rw [← G.map_comp, ← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : ReflectsLimit (cospan f g) G
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
i : HasPullback f g
⊢ G.map pullback.fst ≫ G.map f = G.map pullback.snd ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, pullback.condition]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)
[PROOFSTEP]
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cones.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app (G.mapCone c).π WalkingCospan.left)
      (NatTrans.app (G.mapCone c).π WalkingCospan.right)
      (_ :
        NatTrans.app (G.mapCone c).π WalkingCospan.left ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inl =
          NatTrans.app (G.mapCone c).π WalkingCospan.right ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inr))
[PROOFSTEP]
apply PullbackCone.flipIsLimit
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app (G.mapCone c).π WalkingCospan.right)
      (NatTrans.app (G.mapCone c).π WalkingCospan.left)
      (_ :
        NatTrans.app (G.mapCone c).π WalkingCospan.right ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inr =
          NatTrans.app (G.mapCone c).π WalkingCospan.left ≫ (cospan g f ⋙ G).map WalkingCospan.Hom.inl))
[PROOFSTEP]
apply (isLimitMapConePullbackConeEquiv _ _).toFun
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (G.mapCone (PullbackCone.mk (NatTrans.app c.π WalkingCospan.right) (NatTrans.app c.π WalkingCospan.left) ?m.19346))
[PROOFSTEP]
refine @PreservesLimit.preserves _ _ _ _ _ _ _ _ ?_ _ ?_
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G
[PROOFSTEP]
dsimp
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan f g) G
[PROOFSTEP]
infer_instance
[GOAL]
case t.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (NatTrans.app c.π WalkingCospan.right) (NatTrans.app c.π WalkingCospan.left) ?m.19346)
[PROOFSTEP]
apply PullbackCone.flipIsLimit
[GOAL]
case t.refine_2.t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit
    (PullbackCone.mk (NatTrans.app c.π WalkingCospan.left) (NatTrans.app c.π WalkingCospan.right)
      (_ :
        NatTrans.app c.π WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl =
          NatTrans.app c.π WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cones.postcompose (diagramIsoCospan (cospan g f)).hom).obj c)
[PROOFSTEP]
exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ NatTrans.app c.π WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    NatTrans.app c.π WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl
[PROOFSTEP]
exact (c.π.naturality WalkingCospan.Hom.inr).symm.trans (c.π.naturality WalkingCospan.Hom.inl : _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.fst = G.map pullback.fst
[PROOFSTEP]
simp [PreservesPullback.iso]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.snd = G.map pullback.snd
[PROOFSTEP]
simp [PreservesPullback.iso]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map pullback.fst = pullback.fst
[PROOFSTEP]
simp [PreservesPullback.iso, Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map pullback.snd = pullback.snd
[PROOFSTEP]
simp [PreservesPullback.iso, Iso.inv_comp_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ∀ (j : WalkingSpan),
    NatTrans.app
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).ι
          j ≫
        (Iso.refl
            ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
                (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
      NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι j
[PROOFSTEP]
rintro (_ | _ | _)
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι
        none ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι none
[PROOFSTEP]
dsimp
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι
        (some WalkingPair.left) ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι
      (some WalkingPair.left)
[PROOFSTEP]
dsimp
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι
        (some WalkingPair.right) ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    NatTrans.app (PushoutCocone.mk (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)).ι
      (some WalkingPair.right)
[PROOFSTEP]
dsimp
[GOAL]
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]
[GOAL]
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]
[GOAL]
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
l : IsColimit (PushoutCocone.mk h k comm)
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : ReflectsColimit (span f g) G
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
[PROOFSTEP]
simp only [← G.map_comp, comm]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
i : HasPushout f g
⊢ G.map f ≫ G.map pushout.inl = G.map g ≫ G.map pushout.inr
[PROOFSTEP]
simp only [← G.map_comp, pushout.condition]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)
[PROOFSTEP]
apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit ((Cocones.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app (G.mapCocone c).ι WalkingSpan.left)
      (NatTrans.app (G.mapCocone c).ι WalkingSpan.right)
      (_ :
        (span g f ⋙ G).map WalkingSpan.Hom.fst ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.left =
          (span g f ⋙ G).map WalkingSpan.Hom.snd ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.right))
[PROOFSTEP]
apply PushoutCocone.flipIsColimit
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app (G.mapCocone c).ι WalkingSpan.right)
      (NatTrans.app (G.mapCocone c).ι WalkingSpan.left)
      (_ :
        (span g f ⋙ G).map WalkingSpan.Hom.snd ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.right =
          (span g f ⋙ G).map WalkingSpan.Hom.fst ≫ NatTrans.app (G.mapCocone c).ι WalkingSpan.left))
[PROOFSTEP]
apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
[GOAL]
case t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (G.mapCocone (PushoutCocone.mk (NatTrans.app c.ι WalkingSpan.right) (NatTrans.app c.ι WalkingSpan.left) ?m.60067))
[PROOFSTEP]
refine
  @PreservesColimit.preserves _ _ _ _ _ _ _ _ ?_ _
    ?_
      -- Porting note: more TC coddling
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ PreservesColimit (span ((span g f).map WalkingSpan.Hom.snd) ((span g f).map WalkingSpan.Hom.fst)) G
[PROOFSTEP]
dsimp
[GOAL]
case t.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ PreservesColimit (span f g) G
[PROOFSTEP]
infer_instance
[GOAL]
case t.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (PushoutCocone.mk (NatTrans.app c.ι WalkingSpan.right) (NatTrans.app c.ι WalkingSpan.left) ?m.60067)
[PROOFSTEP]
apply PushoutCocone.flipIsColimit
[GOAL]
case t.refine_2.t
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit
    (PushoutCocone.mk (NatTrans.app c.ι WalkingSpan.left) (NatTrans.app c.ι WalkingSpan.right)
      (_ :
        (span g f).map WalkingSpan.Hom.fst ≫ NatTrans.app c.ι WalkingSpan.left =
          (span g f).map WalkingSpan.Hom.snd ≫ NatTrans.app c.ι WalkingSpan.right))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit ((Cocones.precompose (diagramIsoSpan (span g f)).inv).obj c)
[PROOFSTEP]
exact (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₁} _) _).invFun hc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ (span g f).map WalkingSpan.Hom.snd ≫ NatTrans.app c.ι WalkingSpan.right =
    (span g f).map WalkingSpan.Hom.fst ≫ NatTrans.app c.ι WalkingSpan.left
[PROOFSTEP]
exact (c.ι.naturality WalkingSpan.Hom.snd).trans (c.ι.naturality WalkingSpan.Hom.fst).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl ≫ (iso G f g).hom = G.map pushout.inl
[PROOFSTEP]
delta PreservesPushout.iso
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (span (G.map f) (G.map g)))
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map pushout.inl
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr ≫ (iso G f g).hom = G.map pushout.inr
[PROOFSTEP]
delta PreservesPushout.iso
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (span (G.map f) (G.map g)))
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map pushout.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map pushout.inl ≫ (iso G f g).inv = pushout.inl
[PROOFSTEP]
simp [PreservesPushout.iso, Iso.comp_inv_eq]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map pushout.inr ≫ (iso G f g).inv = pushout.inr
[PROOFSTEP]
simp [PreservesPushout.iso, Iso.comp_inv_eq]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ PreservesLimit (cospan f g) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (pullbackIsPullback f g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk pullback.fst pullback.snd (_ : pullback.fst ≫ f = pullback.snd ≫ g)))
[PROOFSTEP]
apply (isLimitMapConePullbackConeEquiv _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit
    (PullbackCone.mk (G.map pullback.fst) (G.map pullback.snd)
      (_ : G.map pullback.fst ≫ G.map f = G.map pullback.snd ≫ G.map g))
[PROOFSTEP]
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (cospan (G.map f) (G.map g))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsIso
    (IsLimit.lift (limit.isLimit (cospan (G.map f) (G.map g)))
      (PullbackCone.mk (G.map pullback.fst) (G.map pullback.snd)
        (_ : G.map pullback.fst ≫ G.map f = G.map pullback.snd ≫ G.map g)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasPullback f g
inst✝¹ : HasPullback (G.map f) (G.map g)
inst✝ : PreservesLimit (cospan f g) G
⊢ IsIso (pullbackComparison G f g)
[PROOFSTEP]
rw [← PreservesPullback.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasPullback f g
inst✝¹ : HasPullback (G.map f) (G.map g)
inst✝ : PreservesLimit (cospan f g) G
⊢ IsIso (PreservesPullback.iso G f g).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ PreservesColimit (span f g) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (pushoutIsPushout f g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (G.mapCocone (PushoutCocone.mk pushout.inl pushout.inr (_ : f ≫ pushout.inl = g ≫ pushout.inr)))
[PROOFSTEP]
apply
  (isColimitMapCoconePushoutCoconeEquiv _ _).symm
    _
      -- Porting note: apply no longer creates goals for instances
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit
    (PushoutCocone.mk (G.map pushout.inl) (G.map pushout.inr)
      (_ : G.map f ≫ G.map pushout.inl = G.map g ≫ G.map pushout.inr))
[PROOFSTEP]
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (span (G.map f) (G.map g))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsIso
    (IsColimit.desc (colimit.isColimit (span (G.map f) (G.map g)))
      (PushoutCocone.mk (G.map pushout.inl) (G.map pushout.inr)
        (_ : G.map f ≫ G.map pushout.inl = G.map g ≫ G.map pushout.inr)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (pushoutComparison G f g)
[PROOFSTEP]
rw [← PreservesPushout.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₁, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (PreservesPushout.iso G f g).hom
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ G.map (Fork.ι c) ≫ G.map f = 0
[PROOFSTEP]
rw [← G.map_comp, c.condition, G.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ IsLimit (G.mapCone c) ≃ IsLimit (map c G)
[PROOFSTEP]
refine' (IsLimit.postcomposeHomEquiv _ _).symm.trans (IsLimit.equivIsoLimit _)
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
[PROOFSTEP]
refine' parallelPair.ext (Iso.refl _) (Iso.refl _) _ _
[GOAL]
case refine'_1.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.right
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (Cones.postcompose
          (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
              (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
              (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
      (G.mapCone c) ≅
    map c G
[PROOFSTEP]
exact Cones.ext (Iso.refl _) (by rintro (_ | _) <;> aesop_cat)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app
        ((Cones.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                    (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                    (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
            (G.mapCone c)).π
        j =
      (Iso.refl
            ((Cones.postcompose
                    (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                        (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                        (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
                (G.mapCone c)).pt).hom ≫
        NatTrans.app (map c G).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
      ((Cones.postcompose
              (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                  (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                  (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                  (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
          (G.mapCone c)).π
      WalkingParallelPair.zero =
    (Iso.refl
          ((Cones.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
              (G.mapCone c)).pt).hom ≫
      NatTrans.app (map c G).π WalkingParallelPair.zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
      ((Cones.postcompose
              (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                  (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                  (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                  (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
          (G.mapCone c)).π
      WalkingParallelPair.one =
    (Iso.refl
          ((Cones.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ 0)).hom).obj
              (G.mapCone c)).pt).hom ≫
      NatTrans.app (map c G).π WalkingParallelPair.one
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasZeroMorphisms C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms D
G : C ⥤ D
inst✝¹ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝ : PreservesLimit (parallelPair f 0) G
l : IsLimit (KernelFork.ofι h w)
⊢ G.map h ≫ G.map f = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ G.map (kernel.ι f) ≫ G.map f = G.map (kernel.ι f) ≫ 0
[PROOFSTEP]
simp only [← G.map_comp, kernel.condition, comp_zero, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ PreservesLimit (parallelPair f 0) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (kernelIsKernel f)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (G.mapCone (Fork.ofι (kernel.ι f) (_ : kernel.ι f ≫ f = kernel.ι f ≫ 0)))
[PROOFSTEP]
apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (KernelFork.ofι (G.map (kernel.ι f)) (_ : G.map (kernel.ι f) ≫ G.map f = 0))
[PROOFSTEP]
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (kernelIsKernel (G.map f)) i
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom = kernelComparison f G
[PROOFSTEP]
rw [← cancel_mono (kernel.ι _)]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ (iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)
[PROOFSTEP]
simp [PreservesKernel.iso]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ IsIso (kernelComparison f G)
[PROOFSTEP]
rw [← PreservesKernel.iso_hom]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝² : HasKernel f
inst✝¹ : HasKernel (G.map f)
inst✝ : PreservesLimit (parallelPair f 0) G
⊢ IsIso (PreservesKernel.iso G f).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
[PROOFSTEP]
rw [← G.map_comp, hpq, G.map_comp]
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (_ : G.map f ≫ G.map q = G.map p ≫ G.map g) ≫
      (PreservesKernel.iso G g).inv =
    (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq)
[PROOFSTEP]
rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp, PreservesKernel.iso_hom,
  kernelComparison_comp_kernel_map]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ G.map f ≫ G.map (Cofork.π c) = 0
[PROOFSTEP]
rw [← G.map_comp, c.condition, G.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ IsColimit (G.mapCocone c) ≃ IsColimit (map c G)
[PROOFSTEP]
refine' (IsColimit.precomposeHomEquiv _ _).symm.trans (IsColimit.equivIsoColimit _)
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ parallelPair (G.map f) 0 ≅ parallelPair f 0 ⋙ G
[PROOFSTEP]
refine' parallelPair.ext (Iso.refl _) (Iso.refl _) _ _
[GOAL]
case refine'_1.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (parallelPair (G.map f) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ (Cocones.precompose
          (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
              (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
              (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
              (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
      (G.mapCocone c) ≅
    map c G
[PROOFSTEP]
exact Cocones.ext (Iso.refl _) (by rintro (_ | _) <;> aesop_cat)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app
          ((Cocones.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
              (G.mapCocone c)).ι
          j ≫
        (Iso.refl
            ((Cocones.precompose
                    (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                        (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                        (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                        (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
                (G.mapCocone c)).pt).hom =
      NatTrans.app (map c G).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
        ((Cocones.precompose
                (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                    (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                    (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
            (G.mapCocone c)).ι
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocones.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
              (G.mapCocone c)).pt).hom =
    NatTrans.app (map c G).ι WalkingParallelPair.zero
[PROOFSTEP]
aesop_cat
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
⊢ NatTrans.app
        ((Cocones.precompose
                (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                    (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                    (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
            (G.mapCocone c)).ι
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocones.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one))
                      (_ : G.map f ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map f)
                      (_ : 0 ≫ 𝟙 (G.obj Y) = 𝟙 (G.obj X) ≫ G.map 0)).hom).obj
              (G.mapCocone c)).pt).hom =
    NatTrans.app (map c G).ι WalkingParallelPair.one
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasZeroMorphisms C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms D
G : C ⥤ D
inst✝¹ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝ : PreservesColimit (parallelPair f 0) G
l : IsColimit (CokernelCofork.ofπ h w)
⊢ G.map f ≫ G.map h = 0
[PROOFSTEP]
simp only [← G.map_comp, w, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ G.map f ≫ G.map (cokernel.π f) = 0 ≫ G.map (cokernel.π f)
[PROOFSTEP]
simp only [← G.map_comp, cokernel.condition, zero_comp, Functor.map_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ PreservesColimit (parallelPair f 0) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (cokernelIsCokernel f)
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0 ≫ cokernel.π f)))
[PROOFSTEP]
apply (isColimitMapCoconeCoforkEquiv' G (cokernel.condition f)).symm _
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (CokernelCofork.ofπ (G.map (cokernel.π f)) (_ : G.map f ≫ G.map (cokernel.π f) = 0))
[PROOFSTEP]
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (cokernelIsCokernel (G.map f)) i
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G
[PROOFSTEP]
rw [← cancel_epi (cokernel.π _)]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G
[PROOFSTEP]
simp [PreservesCokernel.iso]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ IsIso (cokernelComparison f G)
[PROOFSTEP]
rw [← PreservesCokernel.iso_inv]
[GOAL]
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ IsIso (PreservesCokernel.iso G f).inv
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
[PROOFSTEP]
rw [← G.map_comp, hpq, G.map_comp]
[GOAL]
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesCokernel.iso G f).hom ≫
      cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (_ : G.map f ≫ G.map q = G.map p ≫ G.map g) =
    G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom
[PROOFSTEP]
rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
  cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)
[PROOFSTEP]
have := KernelFork.IsLimit.isIso_ι c hc rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (G.mapCone c)
[PROOFSTEP]
refine' (KernelFork.isLimitMapConeEquiv c G).symm _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (KernelFork.map c G)
[PROOFSTEP]
refine' IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ KernelFork.ofι (𝟙 (G.obj X)) (_ : 𝟙 (G.obj X) ≫ G.map 0 = 0) ≅ KernelFork.map c G
[PROOFSTEP]
exact (Fork.ext (G.mapIso (asIso (Fork.ι c))).symm (by simp))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ (G.mapIso (asIso (Fork.ι c))).symm.hom ≫ Fork.ι (KernelFork.map c G) =
    Fork.ι (KernelFork.ofι (𝟙 (G.obj X)) (_ : 𝟙 (G.obj X) ≫ G.map 0 = 0))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)
[PROOFSTEP]
have := CokernelCofork.IsColimit.isIso_π c hc rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ IsColimit (G.mapCocone c)
[PROOFSTEP]
refine' (CokernelCofork.isColimitMapCoconeEquiv c G).symm _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ IsColimit (CokernelCofork.map c G)
[PROOFSTEP]
refine' IsColimit.ofIsoColimit (CokernelCofork.IsColimit.ofId _ (G.map_zero _ _)) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ CokernelCofork.ofπ (𝟙 (G.obj Y)) (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 0) ≅ CokernelCofork.map c G
[PROOFSTEP]
exact (Cofork.ext (G.mapIso (asIso (Cofork.π c))) (by simp))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
c : Cocone (parallelPair 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ Cofork.π (CokernelCofork.ofπ (𝟙 (G.obj Y)) (_ : G.map 0 ≫ 𝟙 (G.obj Y) = 0)) ≫ (G.mapIso (asIso (Cofork.π c))).hom =
    Cofork.π (CokernelCofork.map c G)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair f 0) G
[PROOFSTEP]
rw [hf]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair 0 0) G
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair f 0) G
[PROOFSTEP]
rw [hf]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms G
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair 0 0) G
[PROOFSTEP]
infer_instance