awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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')
⊢ 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')
have rw₃ : Eq (α := G.obj Y ⟶ colimit (parallelPair f' g')) (q ≫ colimit.ι (parallelPair f' g') WalkingParallelPair.one)
  (q ≫ coequalizer.π f' g')
Tactic: rw [← Category.assoc, map_π_preserves_coequalizer_inv, ι_colimMap, parallelPairHom_app_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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
| 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)))
have a : q ≫ coequalizer.π f' g'
Tactic: rw [map_π_preserves_coequalizer_inv_colimMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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
⊢ 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
have slice_lhs : CategoryStruct.comp (Y := colimit (parallelPair f' g')) (q ≫ coequalizer.π f' g') (coequalizer.desc h wh) = q ≫ h
Tactic: slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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
| CategoryStruct.comp (Y := colimit (parallelPair f' g')) (coequalizer.π f' g') (coequalizer.desc h wh)
have a : h
Tactic: rw [coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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
⊢ CategoryStruct.comp (Y := colimit (parallelPair f' g')) (q ≫ coequalizer.π f' g') (coequalizer.desc h wh) = q ≫ h
have slice_lhs : 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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 := colimit (parallelPair f' g')) (q ≫ coequalizer.π f' g') (coequalizer.desc h wh) = q ≫ h
have slice_lhs₁ : q ≫ h = q ≫ h
Tactic: slice_lhs 2 3 => rw [coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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
⊢ PreservesColimit (parallelPair f g) G
have f₁ : IsColimit
  (G.mapCocone
    (IsSplitCoequalizer.asCofork (Z := HasSplitCoequalizer.coequalizerOfSplit f g)
      (HasSplitCoequalizer.isSplitCoequalizer f g)))
Tactic: apply
    preservesColimit_of_preserves_colimit_cocone
      (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (goal)
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
⊢ PreservesLimit (parallelPair f g) G
have f₁ : IsLimit
  (G.mapCone
    (IsSplitEqualizer.asFork (W := HasSplitEqualizer.equalizerOfSplit f g) (HasSplitEqualizer.isSplitEqualizer f g)))
Tactic: apply
    preservesLimit_of_preserves_limit_cone
      (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images (goal)
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
⊢ CategoryStruct.comp (Y := L.obj (image f)) (L.map (factorThruImage f)) (L.map (image.ι f)) = L.map f
have rw : L.map (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)) = L.map f
Tactic: rw [← L.map_comp, Limits.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images (goal)
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
⊢ CategoryStruct.comp (Y := L.obj (image f)) (L.map (factorThruImage f)) (L.map (image.ι f)) = L.map f
have rw₁ : L.map f = L.map f
Tactic: rw [← L.map_comp, Limits.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images (goal)
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 (α := 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)
have 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 := sorry,
        e := (L.map (factorThruImage f) : L.obj X ⟶ L.obj (image f)), fac := sorry : MonoFactorisation (L.map f) } ≫
    L.map (image.ι f))
  (image.ι (L.map f))
Tactic: rw [iso_hom, image.lift_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images (goal)
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))
⊢ 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)
have rw₁ : Eq (α := image (L.map f) ⟶ L.obj Y) (image.ι (L.map f)) (image.ι (L.map f))
Tactic: rw [iso_hom, image.lift_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ G.map (Fork.ι c) ≫ G.map f = 0
have rw : G.map (Fork.ι c ≫ f) = 0
Tactic: rw [← G.map_comp, c.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
rw : G.map (Fork.ι c ≫ f) = 0
⊢ G.map (Fork.ι c) ≫ G.map f = 0
have rw₁ : Eq (α := G.obj c.pt ⟶ G.obj Y) (G.map 0) 0
Tactic: rw [← G.map_comp, c.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
rw : G.map (Fork.ι c ≫ f) = 0
rw₁ : Eq (α := G.obj c.pt ⟶ G.obj Y) (G.map 0) 0
⊢ G.map (Fork.ι c) ≫ G.map f = 0
have rw₂ : Eq.{v₂ + 1} (α := G.obj c.pt ⟶ G.obj Y) 0 0
Tactic: rw [← G.map_comp, c.condition, G.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ IsLimit (G.mapCone c) ≃ IsLimit (F := parallelPair (G.map f) 0) (c.map G)
have refine_1 : parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
Tactic: refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
refine_1 : parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
⊢ IsLimit (G.mapCone c) ≃ IsLimit (F := parallelPair (G.map f) 0) (c.map G)
have refine_2 : (Cone.postcompose
        (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
            (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) sorry sorry).hom).obj
    (G.mapCone c) ≅
  c.map G
Tactic: refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
⊢ parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
have refine_1 : (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
  Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
    (parallelPair (G.map f) 0).map WalkingParallelPairHom.left
Tactic: refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
refine_1 :
  (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
      (parallelPair (G.map f) 0).map WalkingParallelPairHom.left
⊢ parallelPair f 0 ⋙ G ≅ parallelPair (G.map f) 0
have refine_1₁ : (parallelPair f 0 ⋙ G).map WalkingParallelPairHom.right ≫
    Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) =
  Iso.hom (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero)) ≫
    (parallelPair (G.map f) 0).map WalkingParallelPairHom.right
Tactic: refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
i : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)
⊢ PreservesLimit (parallelPair f 0) G
have apply : IsLimit (F := parallelPair f 0 ⋙ G) (G.mapCone (Fork.ofι (P := kernel f) (kernel.ι f) sorry))
Tactic: apply preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
i : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)
⊢ IsLimit (F := parallelPair f 0 ⋙ G) (G.mapCone (Fork.ofι (P := kernel f) (kernel.ι f) ⋯))
have apply : IsLimit (F := parallelPair (G.map f) 0) (KernelFork.ofι (Z := G.obj (kernel f)) (G.map (kernel.ι f)) sorry)
Tactic: apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
⊢ Eq (α := G.obj (kernel f) ⟶ kernel (G.map f)) (Iso.hom (iso G f)) (kernelComparison f G)
have rw : Eq (α := G.obj (kernel f) ⟶ G.obj X)
  (CategoryStruct.comp (Y := kernel (G.map f)) (Iso.hom (iso G f)) (kernel.ι (G.map f)))
  (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G) (kernel.ι (G.map f)))
Tactic: rw [← cancel_mono (kernel.ι _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
⊢ IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (kernelComparison f G)
have rw : IsIso (X := G.obj (kernel f)) (Y := kernel (G.map f)) (Iso.hom (PreservesKernel.iso G f))
Tactic: rw [← PreservesKernel.iso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasKernel g
inst_9 : HasKernel (G.map g)
inst_10 : 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
have rw : G.map (f ≫ q) = G.map p ≫ G.map g
Tactic: rw [← G.map_comp, hpq, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
inst_7 : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasKernel g
inst_9 : HasKernel (G.map g)
inst_10 : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : G.map (f ≫ q) = G.map p ≫ G.map g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
have rw₁ : G.map (p ≫ g) = G.map p ≫ G.map g
Tactic: rw [← G.map_comp, hpq, G.map_comp]