awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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 :
  ∀ (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) ⋯ :
                s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
            s ≫
          b') ≫
        b =
      s.snd ≫ 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

Tactic:
rw [KernelFork.ι_ofι] at hb'

Premises used: CategoryTheory.Limits.KernelFork.ι_ofι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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' ≫ b = 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

Tactic:
simp [hb']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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
e_a : kernel.ι (prod.lift f g) = a' ≫ a
⊢ m ≫ kernel.ι (prod.lift f g) = m ≫ a' ≫ a

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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
⊢ kernel.ι (prod.lift f g) = a' ≫ a

Tactic:
ha'.symm

Premises used: CategoryTheory.Limits.Fork.ι, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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
⊢ kernel.ι (prod.lift f g) = a' ≫ a

Tactic:
exact ha'.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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
rw₁ rw₂ : s.fst ≫ a = s.fst ≫ a
⊢ m ≫ a' ≫ a = s.fst ≫ a

Tactic:
rw [← Category.assoc, h₁]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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 rw₁ : s.snd ≫ b = s.snd ≫ b
⊢ 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))

Tactic:
rw [kernel.lift_ι]

Premises used: CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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 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)
⊢ 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)

Tactic:
rw [prod.lift_fst]

Premises used: CategoryTheory.Limits.prod.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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 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)
⊢ 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)

Tactic:
rw [pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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))
rw₁ 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))
⊢ 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))

Tactic:
rw [prod.lift_fst, Category.comp_id]

Premises used: CategoryTheory.Limits.prod.lift_fst, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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))
rw 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)
⊢ 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)

Tactic:
rw [prod.lift_snd]

Premises used: CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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))
rw 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)
⊢ 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)

Tactic:
rw [pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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))
rw 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)
⊢ 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)

Tactic:
rw [prod.lift_snd]

Premises used: CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [hvu, ← huv]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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)
huu :
  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)
s : Fork f g
⊢ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (s.ι ≫ prod.lift (𝟙 X) f) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (s.ι ≫ prod.lift (𝟙 X) g) prod.fst

Tactic:
simp only [prod.lift_fst, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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)
huu :
  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)
s : Fork f g
⊢ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (s.ι ≫ prod.lift (𝟙 X) f) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} X Y) (s.ι ≫ prod.lift (𝟙 X) g) prod.snd

Tactic:
simp only [prod.comp_lift, Fork.condition s]

Premises used: CategoryTheory.Limits.Fork.condition, CategoryTheory.Limits.prod.comp_lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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)
huu :
  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)
s : Fork f g
⊢ (fun (s : Fork f g) ↦
          (pullback.lift s.ι s.ι ⋯ :
            s.pt ⟶ pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)))
        s ≫
      (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).ι =
    s.ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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)
huu :
  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)
s : Fork f g
m : s.pt ⟶ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).pt
h : m ≫ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).ι = s.ι
⊢ m ≫ pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) =
    CategoryStruct.comp (Y := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
      ((fun (s : Fork f g) ↦
          (pullback.lift s.ι s.ι ⋯ :
            s.pt ⟶ pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)))
        s)
      (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))

Tactic:
simpa only [pullback.lift_fst] using h

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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)
huu :
  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)
s : Fork f g
m : s.pt ⟶ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).pt
h : m ≫ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).ι = s.ι
⊢ m ≫ pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) =
    CategoryStruct.comp (Y := pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))
      ((fun (s : Fork f g) ↦
          (pullback.lift s.ι s.ι ⋯ :
            s.pt ⟶ pullback (Z := Limits.prod.{v_1, u_1} X Y) (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)))
        s)
      (pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g))

Tactic:
simpa only [huv.symm, pullback.lift_fst] using h

Premises used: Eq.symm, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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
⊢ HasEqualizers.{v_1, u_1} C

Tactic:
hasEqualizers_of_hasLimit_parallelPair _

Premises used: CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
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
⊢ Eq (α := X ⟶ Z) (f ≫ 0) 0

Tactic:
simp