awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
rw : Eq.{v_1 + 1} (α := s.pt ⟶ P) 0 (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)
⊢ Eq (α := s.pt ⟶ P) (s.fst ≫ 0) (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)
have rw₁ : Eq.{v_1 + 1} (α := s.pt ⟶ P) 0 0
Tactic: rw [comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ s.snd ≫ b ≫ g = s.snd ≫ 0
have rw : Eq (α := s.pt ⟶ Q) (s.snd ≫ 0) (s.snd ≫ 0)
Tactic: rw [hbg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ Eq (α := s.pt ⟶ Q) (s.snd ≫ 0) (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
have rw : Eq.{v_1 + 1} (α := s.pt ⟶ Q) 0 (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
Tactic: rw [comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
rw : Eq.{v_1 + 1} (α := s.pt ⟶ Q) 0 (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
⊢ Eq (α := s.pt ⟶ Q) (s.snd ≫ 0) (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
have rw₁ : Eq.{v_1 + 1} (α := s.pt ⟶ Q) 0 0
Tactic: rw [comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ ((fun (s : PullbackCone a b) ↦
            (kernel.lift (prod.lift f g) (s.snd ≫ b) ⋯ :
              s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
          s ≫
        a') ≫
      a =
    s.fst ≫ a
have rw : ∀ (ha' : a' ≫ a = kernel.ι (prod.lift f g))
  (b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt)
  (hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)) (s : PullbackCone a b),
  ((fun (s : PullbackCone a b) ↦
            (kernel.lift (prod.lift f g) (s.snd ≫ b) sorry :
              s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
          s ≫
        a') ≫
      a =
    s.fst ≫ a
Tactic: rw [KernelFork.ι_ofι] at ha'
Cleared hypotheses: ha', b', hb', s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ ((fun (s : PullbackCone a b) ↦
            (kernel.lift (prod.lift f g) (s.snd ≫ b) ⋯ :
              s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
          s ≫
        b') ≫
      b =
    s.snd ≫ b
have rw : ∀ (hb' : b' ≫ b = kernel.ι (prod.lift f g)) (s : PullbackCone a b),
  ((fun (s : PullbackCone a b) ↦
            (kernel.lift (prod.lift f g) (s.snd ≫ b) sorry :
              s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
          s ≫
        b') ≫
      b =
    s.snd ≫ b
Tactic: rw [KernelFork.ι_ofι] at hb'
Cleared hypotheses: hb', s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)
h₁ : m ≫ a' = s.fst
h : m ≫ b' = s.snd
⊢ m ≫ kernel.ι (prod.lift f g) = m ≫ a' ≫ a
have e_a : kernel.ι (prod.lift f g) = a' ≫ a
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)
h₁ : m ≫ a' = s.fst
h : m ≫ b' = s.snd
⊢ m ≫ a' ≫ a = s.fst ≫ a
have rw : (m ≫ a') ≫ a = s.fst ≫ a
Tactic: rw [← Category.assoc, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)
h₁ : m ≫ a' = s.fst
h : m ≫ b' = s.snd
rw : (m ≫ a') ≫ a = s.fst ≫ a
⊢ m ≫ a' ≫ a = s.fst ≫ a
have rw₁ : s.fst ≫ a = s.fst ≫ a
Tactic: rw [← Category.assoc, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst_5 : Mono a
inst_6 : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)
h₁ : m ≫ a' = s.fst
h : m ≫ b' = s.snd
⊢ s.snd ≫ b =
    CategoryStruct.comp (Y := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g))
      (kernel.lift (prod.lift f g) (s.snd ≫ b) ⋯) (kernel.ι (prod.lift f g))
have rw : s.snd ≫ b = s.snd ≫ b
Tactic: rw [kernel.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) prod.fst)
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
  (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X)
  (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X)
Tactic: rw [prod.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) prod.fst)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.fst)
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
    CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.fst)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
    CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.fst)
Tactic: rw [pullback.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.fst)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
Tactic: rw [prod.lift_fst, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
rw :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.fst)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
have rw₁ : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
Tactic: rw [prod.lift_fst, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) prod.snd)
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
  (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f) (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f)
Tactic: rw [prod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) prod.snd)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.snd)
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
    CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.snd)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
    CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.snd)
Tactic: rw [pullback.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫
      CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) g) prod.snd)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
Tactic: rw [prod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
hvu :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
have rw : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
  (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g) (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
Tactic: rw [hvu, ← huv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ X)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
hvu :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
rw :
  Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
⊢ Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f)
    (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
have rw₁ : Eq (α := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ⟶ Y)
  (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g) (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g)
Tactic: rw [hvu, ← huv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
⊢ u = v
have obtain : ∀ (W : C) (w : Y ⟶ W) (hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0)
  (hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)), u = v
Tactic: obtain ⟨W, w, hw, hl⟩ := normalMonoOfMono (equalizer.ι u v)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
⊢ u = v
have obtain : ∀ (m : X ⟶ equalizer u v) (hm : m ≫ equalizer.ι u v = f), u = v
Tactic: obtain ⟨m, hm⟩ := equalizer.lift' f huv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ f ≫ w = 0
have rw : (m ≫ equalizer.ι u v) ≫ w = 0
Tactic: rw [← hm, Category.assoc, hw, comp_zero]