[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, w]
[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (Iso.refl
          ((Cones.postcompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).hom).obj
              (G.mapCone (Fork.ofι h w))).pt).hom ≫
      Fork.ι (Fork.ofι (G.map h) (_ : G.map h ≫ G.map f = G.map h ≫ G.map g)) =
    Fork.ι ((Cones.postcompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).hom).obj (G.mapCone (Fork.ofι h w)))
[PROOFSTEP]
simp [Fork.ι]
[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝ : PreservesLimit (parallelPair f g) G
l : IsLimit (Fork.ofι h w)
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, w]
[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝ : ReflectsLimit (parallelPair f g) G
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp, w]
[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : PreservesLimit (parallelPair f g) G
⊢ G.map (equalizer.ι f g) ≫ G.map f = G.map (equalizer.ι f g) ≫ G.map g
[PROOFSTEP]
simp only [← G.map_comp]
[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : PreservesLimit (parallelPair f g) G
⊢ G.map (equalizer.ι f g ≫ f) = G.map (equalizer.ι f g ≫ g)
[PROOFSTEP]
rw [equalizer.condition]
[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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ PreservesLimit (parallelPair f g) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (equalizerIsEqualizer 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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsLimit (G.mapCone (Fork.ofι (equalizer.ι f g) (_ : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g)))
[PROOFSTEP]
apply (isLimitMapConeForkEquiv _ _).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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsLimit
    (Fork.ofι (G.map (equalizer.ι f g)) (_ : G.map (equalizer.ι f g) ≫ G.map f = G.map (equalizer.ι f g) ≫ G.map g))
[PROOFSTEP]
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (parallelPair (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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsIso
    (IsLimit.lift (limit.isLimit (parallelPair (G.map f) (G.map g)))
      (Fork.ofι (G.map (equalizer.ι f g)) (_ : G.map (equalizer.ι f g) ≫ G.map f = G.map (equalizer.ι f g) ≫ 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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ IsIso (equalizerComparison f g G)
[PROOFSTEP]
rw [← PreservesEqualizer.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 g : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = h ≫ g
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ IsIso (PreservesEqualizer.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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h
[PROOFSTEP]
simp only [← G.map_comp, w]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ Cofork.π
        ((Cocones.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj (G.mapCocone (Cofork.ofπ h w))) ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj
              (G.mapCocone (Cofork.ofπ h w))).pt).hom =
    Cofork.π (Cofork.ofπ (G.map h) (_ : G.map f ≫ G.map h = G.map g ≫ G.map h))
[PROOFSTEP]
dsimp only [Cofork.π, Cofork.ofπ_ι_app]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj (G.mapCocone (Cofork.ofπ h w))).ι
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj
              (G.mapCocone (Cofork.ofπ h w))).pt).hom =
    G.map h
[PROOFSTEP]
dsimp
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ (𝟙 (G.obj Y) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
[PROOFSTEP]
rw [Category.comp_id, Category.id_comp]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝ : PreservesColimit (parallelPair f g) G
l : IsColimit (Cofork.ofπ h w)
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h
[PROOFSTEP]
simp only [← G.map_comp, w]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝ : ReflectsColimit (parallelPair f g) G
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h
[PROOFSTEP]
simp only [← G.map_comp, w]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝¹ : HasCoequalizer f g
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map f ≫ G.map (coequalizer.π f g) = G.map g ≫ G.map (coequalizer.π f g)
[PROOFSTEP]
simp only [← G.map_comp]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝¹ : HasCoequalizer f g
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map (f ≫ coequalizer.π f g) = G.map (g ≫ coequalizer.π f g)
[PROOFSTEP]
rw [coequalizer.condition]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ PreservesColimit (parallelPair f g) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (coequalizerIsCoequalizer 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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (coequalizer.π f g) (_ : f ≫ coequalizer.π f g = g ≫ coequalizer.π f g)))
[PROOFSTEP]
apply (isColimitMapCoconeCoforkEquiv _ _).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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit
    (Cofork.ofπ (G.map (coequalizer.π f g))
      (_ : G.map f ≫ G.map (coequalizer.π f g) = G.map g ≫ G.map (coequalizer.π f g)))
[PROOFSTEP]
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (parallelPair (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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsIso
    (IsColimit.desc (colimit.isColimit (parallelPair (G.map f) (G.map g)))
      (Cofork.ofπ (G.map (coequalizer.π f g))
        (_ : G.map f ≫ G.map (coequalizer.π f g) = G.map g ≫ G.map (coequalizer.π f 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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ IsIso (coequalizerComparison f g G)
[PROOFSTEP]
rw [← PreservesCoequalizer.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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ IsIso (PreservesCoequalizer.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 g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ G.map (coequalizer.π f g) ≫ h = G.map (coequalizer.π f g) ≫ k → h = k
[PROOFSTEP]
rw [← ι_comp_coequalizerComparison]
[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 g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) ≫ h =
      (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) ≫ k →
    h = k
[PROOFSTEP]
haveI : Epi (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) := by apply epi_comp
[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 g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ Epi (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G)
[PROOFSTEP]
apply epi_comp
[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 g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
this : Epi (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G)
⊢ (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) ≫ h =
      (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) ≫ k →
    h = k
[PROOFSTEP]
apply (cancel_epi _).1
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g)
[PROOFSTEP]
rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id, comp_id]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k
[PROOFSTEP]
rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]
[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 g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) =
    q ≫ coequalizer.π f' g'
[PROOFSTEP]
rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]
[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 g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫
        colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
    q ≫ h
[PROOFSTEP]
slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| G.map (coequalizer.π f g) ≫
    (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| coequalizer.desc h wh
[PROOFSTEP]
rw [map_π_preserves_coequalizer_inv_colimMap]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| G.map (coequalizer.π f g) ≫
    (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| coequalizer.desc h wh
[PROOFSTEP]
rw [map_π_preserves_coequalizer_inv_colimMap]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| G.map (coequalizer.π f g) ≫
    (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| coequalizer.desc h wh
[PROOFSTEP]
rw [map_π_preserves_coequalizer_inv_colimMap]
[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 g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ (q ≫ coequalizer.π f' g') ≫ coequalizer.desc h wh = q ≫ h
[PROOFSTEP]
slice_lhs 2 3 => rw [coequalizer.π_desc]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| coequalizer.π f' g' ≫ coequalizer.desc h wh
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| q
[PROOFSTEP]
rw [coequalizer.π_desc]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| coequalizer.π f' g' ≫ coequalizer.desc h wh
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| q
[PROOFSTEP]
rw [coequalizer.π_desc]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| coequalizer.π f' g' ≫ coequalizer.desc h wh
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h✝ : Y ⟶ Z
w : f ≫ h✝ = g ≫ h✝
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
| q
[PROOFSTEP]
rw [coequalizer.π_desc]
[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✝ g✝ : X ⟶ Y
h : Y ⟶ Z
w : f✝ ≫ h = g✝ ≫ h
inst✝³ : HasCoequalizer f✝ g✝
inst✝² : HasCoequalizer (G.map f✝) (G.map g✝)
inst✝¹ : PreservesColimit (parallelPair f✝ g✝) G
f g : X ⟶ Y
inst✝ : HasSplitCoequalizer f g
⊢ PreservesColimit (parallelPair f g) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer
[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✝ g✝ : X ⟶ Y
h : Y ⟶ Z
w : f✝ ≫ h = g✝ ≫ h
inst✝³ : HasCoequalizer f✝ g✝
inst✝² : HasCoequalizer (G.map f✝) (G.map g✝)
inst✝¹ : PreservesColimit (parallelPair f✝ g✝) G
f g : X ⟶ Y
inst✝ : HasSplitCoequalizer f g
⊢ IsColimit (G.mapCocone (IsSplitCoequalizer.asCofork (HasSplitCoequalizer.isSplitCoequalizer f g)))
[PROOFSTEP]
apply (isColimitMapCoconeCoforkEquiv G _).symm ((HasSplitCoequalizer.isSplitCoequalizer f g).map G).isCoequalizer