awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : PreservesColimit (parallelPair f g) G
l : IsColimit (Cofork.ofπ h w)
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : ReflectsColimit (parallelPair f g) G
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : HasCoequalizer f g
inst_3 : PreservesColimit (parallelPair f g) G
simp : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map f ≫ G.map (coequalizer.π f g))
    (G.map g ≫ G.map (coequalizer.π f g))

Tactic:
simp only [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : HasCoequalizer f g
inst_3 : PreservesColimit (parallelPair f g) G
rw rw₁ : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (g ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))

Tactic:
rw [coequalizer.condition]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
i : IsIso (X := coequalizer (G.map f) (G.map g)) (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
apply : IsColimit (G.mapCocone (Cofork.ofπ (P := coequalizer f g) (coequalizer.π f g) ⋯))
⊢ PreservesColimit (parallelPair f g) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coequalizerIsCoequalizer f g)

Premises used: CategoryTheory.Limits.coequalizerIsCoequalizer, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
i : IsIso (X := coequalizer (G.map f) (G.map g)) (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
apply : IsColimit (Cofork.ofπ (P := G.obj (coequalizer f g)) (G.map (coequalizer.π f g)) ⋯)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (P := coequalizer f g) (coequalizer.π f g) ⋯))

Tactic:
apply (isColimitMapCoconeCoforkEquiv _ _).symm _

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
i : IsIso (X := coequalizer (G.map f) (G.map g)) (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
⊢ IsColimit (Cofork.ofπ (P := G.obj (coequalizer f g)) (G.map (coequalizer.π f g)) ⋯)

Tactic:
exact
    @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (parallelPair (G.map f) (G.map g))) i

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Functor.map, CategoryTheory.Limits.IsColimit.ofPointIso, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
⊢ Eq (α := coequalizer (G.map f) (G.map g) ⟶ G.obj (coequalizer f g)) (Iso.hom (iso G f g))
    (coequalizerComparison f g G)

Tactic:
rfl

Premises used: CategoryTheory.Limits.coequalizerComparison, CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
⊢ IsIso (X := coequalizer (G.map f) (G.map g)) (Y := G.obj (coequalizer f g)) (Iso.hom (PreservesCoequalizer.iso G f g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h_1 : Y ⟶ Z
w : f ≫ h_1 = g ≫ h_1
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
rw :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
          (coequalizerComparison f g G) ≫
        h =
      CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
          (coequalizerComparison f g G) ≫
        k →
    h = k
⊢ G.map (coequalizer.π f g) ≫ h = G.map (coequalizer.π f g) ≫ k → h = k

Tactic:
rw [← ι_comp_coequalizerComparison]

Premises used: CategoryTheory.Limits.ι_comp_coequalizerComparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h_1 : Y ⟶ Z
w : f ≫ h_1 = g ≫ h_1
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ Epi (Y := G.obj (coequalizer f g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizerComparison f g G))

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h_1 : Y ⟶ Z
w : f ≫ h_1 = g ≫ h_1
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
⊢ Epi (Y := G.obj (coequalizer f g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizerComparison f g G))

Tactic:
haveI : Epi (coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G) := by
      apply epi_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f g : X ⟶ Y
h_1 : Y ⟶ Z
w : f ≫ h_1 = g ≫ h_1
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
h k : G.obj (coequalizer f g) ⟶ W
this :
  Epi (Y := G.obj (coequalizer f g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizerComparison f g G))
⊢ CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
          (coequalizerComparison f g G) ≫
        h =
      CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
          (coequalizerComparison f g G) ≫
        k →
    h = k

Tactic:
apply (cancel_epi _).1

Premises used: Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
rw :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G)
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
rw₁ :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (Iso.hom (PreservesCoequalizer.iso G f g))
        (Iso.inv (PreservesCoequalizer.iso G f g))))
    (coequalizer.π (G.map f) (G.map g))
rw₂ : coequalizer.π (G.map f) (G.map g) ≫ 𝟙 (coequalizer (G.map f) (G.map g)) = coequalizer.π (G.map f) (G.map g)
rw₃ rw₄ :
  Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
    (coequalizer.π (G.map f) (G.map g))
⊢ Eq (α := G.obj Y ⟶ coequalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (Iso.inv (PreservesCoequalizer.iso G f g)))
    (coequalizer.π (G.map f) (G.map g))

Tactic:
rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Limits.ι_comp_coequalizerComparison_assoc, CategoryTheory.Limits.PreservesCoequalizer.iso_hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
rw :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
        (Iso.inv (PreservesCoequalizer.iso G f g)))
      (coequalizer.desc k wk) =
    k
rw₁ :
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (coequalizer.desc k wk) =
    k
rw₂ rw₃ : k = k
⊢ CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (coequalizer.desc k wk)) =
    k

Tactic:
rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.coequalizer.π_desc, CategoryTheory.Limits.map_π_preserves_coequalizer_inv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst_5 : 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'
rw :
  Eq (α := G.obj Y ⟶ colimit (parallelPair f' g'))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
        (Iso.inv (PreservesCoequalizer.iso G f g)))
      (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)))
    (q ≫ coequalizer.π f' g')
rw₁ :
  Eq (α := G.obj Y ⟶ colimit (parallelPair f' g'))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
      (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)))
    (q ≫ coequalizer.π f' g')
rw₂ :
  Eq (α := G.obj Y ⟶ colimit (parallelPair f' g'))
    ((parallelPairHom (G.map f) (G.map g) f' g' p q wf wg).app WalkingParallelPair.one ≫
      colimit.ι (parallelPair f' g') WalkingParallelPair.one)
    (q ≫ coequalizer.π f' g')
rw₃ rw₄ :
  Eq (α := G.obj Y ⟶ colimit (parallelPair f' g')) (q ≫ colimit.ι (parallelPair f' g') WalkingParallelPair.one)
    (q ≫ coequalizer.π f' g')
⊢ Eq (α := G.obj Y ⟶ colimit (parallelPair f' g'))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))))
    (q ≫ coequalizer.π f' g')

Tactic:
rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.parallelPairHom_app_one, CategoryTheory.Limits.map_π_preserves_coequalizer_inv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst_5 : 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
a : q ≫ coequalizer.π f' g'
| CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
    (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
      (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)))

Tactic:
rw [map_π_preserves_coequalizer_inv_colimMap]

Premises used: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst_5 : 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
slice_lhs :
  CategoryStruct.comp (Y := colimit (parallelPair f' g')) (q ≫ coequalizer.π f' g') (coequalizer.desc h wh) = q ≫ h
⊢ CategoryStruct.comp (Y := G.obj (coequalizer f g)) (G.map (coequalizer.π f g))
      (CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (Iso.inv (PreservesCoequalizer.iso G f g))
        (CategoryStruct.comp (Y := colimit (parallelPair f' g'))
          (colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg)) (coequalizer.desc h wh))) =
    q ≫ h

Tactic:
slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]

Premises used: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst_5 : 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
a : h
| CategoryStruct.comp (Y := colimit (parallelPair f' g')) (coequalizer.π f' g') (coequalizer.desc h wh)

Tactic:
rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
inst_4 : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst_5 : 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
slice_lhs :
  CategoryStruct.comp (Y := colimit (parallelPair f' g')) (q ≫ coequalizer.π f' g') (coequalizer.desc h wh) = q ≫ h
slice_lhs₁ : q ≫ h = q ≫ h
⊢ CategoryStruct.comp (Y := colimit (parallelPair f' g')) (q ≫ coequalizer.π f' g') (coequalizer.desc h wh) = q ≫ h

Tactic:
slice_lhs 2 3 => rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 g_1 : X ⟶ Y
h : Y ⟶ Z
w : f_1 ≫ h = g_1 ≫ h
inst_2 : HasCoequalizer f_1 g_1
inst_3 : HasCoequalizer (G.map f_1) (G.map g_1)
inst_4 : PreservesColimit (parallelPair f_1 g_1) G
f g : X ⟶ Y
inst_5 : HasSplitCoequalizer f g
f₁ :
  IsColimit
    (G.mapCocone
      (IsSplitCoequalizer.asCofork (Z := HasSplitCoequalizer.coequalizerOfSplit f g)
        (HasSplitCoequalizer.isSplitCoequalizer f g)))
⊢ PreservesColimit (parallelPair f g) G

Tactic:
apply
    preservesColimit_of_preserves_colimit_cocone
      (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer

Premises used: CategoryTheory.HasSplitCoequalizer.isSplitCoequalizer, CategoryTheory.IsSplitCoequalizer.isCoequalizer, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 g_1 : X ⟶ Y
h : Y ⟶ Z
w : f_1 ≫ h = g_1 ≫ h
inst_2 : HasCoequalizer f_1 g_1
inst_3 : HasCoequalizer (G.map f_1) (G.map g_1)
inst_4 : PreservesColimit (parallelPair f_1 g_1) G
f g : X ⟶ Y
inst_5 : HasSplitCoequalizer f g
⊢ IsColimit
    (G.mapCocone
      (IsSplitCoequalizer.asCofork (Z := HasSplitCoequalizer.coequalizerOfSplit f g)
        (HasSplitCoequalizer.isSplitCoequalizer f g)))

Tactic:
apply
    (isColimitMapCoconeCoforkEquiv G _).symm
      ((HasSplitCoequalizer.isSplitCoequalizer f g).map G).isCoequalizer

Premises used: CategoryTheory.IsSplitCoequalizer.map, CategoryTheory.HasSplitCoequalizer.isSplitCoequalizer, CategoryTheory.IsSplitCoequalizer.isCoequalizer, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 g_1 : X ⟶ Y
h : Y ⟶ Z
w : f_1 ≫ h = g_1 ≫ h
inst_2 : HasCoequalizer f_1 g_1
inst_3 : HasCoequalizer (G.map f_1) (G.map g_1)
inst_4 : PreservesColimit (parallelPair f_1 g_1) G
f g : X ⟶ Y
inst_5 : HasSplitEqualizer f g
f₁ :
  IsLimit
    (G.mapCone
      (IsSplitEqualizer.asFork (W := HasSplitEqualizer.equalizerOfSplit f g) (HasSplitEqualizer.isSplitEqualizer f g)))
⊢ PreservesLimit (parallelPair f g) G

Tactic:
apply
    preservesLimit_of_preserves_limit_cone
      (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer

Premises used: CategoryTheory.IsSplitEqualizer.isEqualizer, CategoryTheory.HasSplitEqualizer.isSplitEqualizer, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 g_1 : X ⟶ Y
h : Y ⟶ Z
w : f_1 ≫ h = g_1 ≫ h
inst_2 : HasCoequalizer f_1 g_1
inst_3 : HasCoequalizer (G.map f_1) (G.map g_1)
inst_4 : PreservesColimit (parallelPair f_1 g_1) G
f g : X ⟶ Y
inst_5 : HasSplitEqualizer f g
⊢ IsLimit
    (G.mapCone
      (IsSplitEqualizer.asFork (W := HasSplitEqualizer.equalizerOfSplit f g) (HasSplitEqualizer.isSplitEqualizer f g)))

Tactic:
apply
    (isLimitMapConeForkEquiv G _).symm
      ((HasSplitEqualizer.isSplitEqualizer f g).map G).isEqualizer

Premises used: CategoryTheory.IsSplitEqualizer.isEqualizer, CategoryTheory.Limits.isLimitMapConeForkEquiv, CategoryTheory.HasSplitEqualizer.isSplitEqualizer, CategoryTheory.IsSplitEqualizer.map, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : HasEqualizers.{v₁, u₁} A
inst_3 : HasImages.{v₁, u₁} A
inst_4 : StrongEpiCategory.{v₂, u₂} B
inst_5 : HasImages.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_6 : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst_7 : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
rw : L.map (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)) = L.map f
rw₁ rw₂ : L.map f = L.map f
⊢ CategoryStruct.comp (Y := L.obj (image f)) (L.map (factorThruImage f)) (L.map (image.ι f)) = L.map f

Tactic:
rw [← L.map_comp, Limits.image.fac]

Premises used: CategoryTheory.Limits.image.fac, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : HasEqualizers.{v₁, u₁} A
inst_3 : HasImages.{v₁, u₁} A
inst_4 : StrongEpiCategory.{v₂, u₂} B
inst_5 : HasImages.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_6 : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst_7 : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ Eq (α := L.obj X ⟶ L.obj (image f))
    (CategoryStruct.comp (Y := image (L.map f)) (factorThruImage (L.map f) : L.obj X ⟶ image (L.map f))
        (Iso.hom (iso L f) : image (L.map f) ⟶ L.obj (image f)) :
      L.obj X ⟶ L.obj (image f))
    (L.map (factorThruImage f) : L.obj X ⟶ L.obj (image f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : HasEqualizers.{v₁, u₁} A
inst_3 : HasImages.{v₁, u₁} A
inst_4 : StrongEpiCategory.{v₂, u₂} B
inst_5 : HasImages.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_6 : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst_7 : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
rw :
  Eq (α := image (L.map f) ⟶ L.obj Y)
    (image.lift
        { I := L.obj (image f), m := (L.map (image.ι f) : L.obj (image f) ⟶ L.obj Y), m_mono := ⋯,
          e := (L.map (factorThruImage f) : L.obj X ⟶ L.obj (image f)), fac := ⋯ : MonoFactorisation (L.map f) } ≫
      L.map (image.ι f))
    (image.ι (L.map f))
rw₁ rw₂ : Eq (α := image (L.map f) ⟶ L.obj Y) (image.ι (L.map f)) (image.ι (L.map f))
⊢ Eq (α := image (L.map f) ⟶ L.obj Y)
    (CategoryStruct.comp (Y := L.obj (image f)) (Iso.hom (iso L f) : image (L.map f) ⟶ L.obj (image f))
        (L.map (image.ι f) : L.obj (image f) ⟶ L.obj Y) :
      image (L.map f) ⟶ L.obj Y)
    (image.ι (L.map f) : image (L.map f) ⟶ L.obj Y)

Tactic:
rw [iso_hom, image.lift_fac]

Premises used: CategoryTheory.PreservesImage.iso_hom, CategoryTheory.Limits.image.lift_fac