awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ f ≫ m') 0
⊢ Eq (α :=
    Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
        (KernelFork.ofι (m'.unop ≫ f.unop) ⋯) ⟶
      Functor.obj.{0, v₁, 0, u₁}
        (parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
        WalkingParallelPair.zero)
    (m'.unop ≫ NatTrans.app (Cone.π (KernelFork.ofι f.unop ⋯)) WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (KernelFork.ofι (m'.unop ≫ f.unop) ⋯)) WalkingParallelPair.zero)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ f ≫ m') 0
⊢ Eq (α :=
    Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
        (KernelFork.ofι (m'.unop ≫ f.unop) ⋯) ⟶
      Functor.obj.{0, v₁, 0, u₁}
        (parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
        WalkingParallelPair.one)
    (m'.unop ≫ NatTrans.app (Cone.π (KernelFork.ofι f.unop ⋯)) WalkingParallelPair.one)
    (NatTrans.app (Cone.π (KernelFork.ofι (m'.unop ≫ f.unop) ⋯)) WalkingParallelPair.one)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : Eq (α := Z' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) ((m' ≫ f) ≫ Quiver.Hom.op NormalEpi.g) 0
a :
  m'.unop =
    Quiver.Hom.unop
      ((fun {W' : Cᵒᵖ} (g' : W' ⟶ Y)
            (w' : Eq (α := W' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) (g' ≫ Quiver.Hom.op NormalEpi.g) 0) ↦
          (Quiver.Hom.op
              (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop ⋯) :
                (CokernelCofork.ofπ f.unop ⋯).pt ⟶ unop W') :
            op (unop W') ⟶
              op
                (Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
                  (CokernelCofork.ofπ f.unop ⋯))))
        (m' ≫ f) w')
⊢ m' =
    (fun {W' : Cᵒᵖ} (g' : W' ⟶ Y)
          (w' : Eq (α := W' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) (g' ≫ Quiver.Hom.op NormalEpi.g) 0) ↦
        (Quiver.Hom.op
            (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop ⋯) :
              (CokernelCofork.ofπ f.unop ⋯).pt ⟶ unop W') :
          op (unop W') ⟶
            op
              (Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
                (CokernelCofork.ofπ f.unop ⋯))))
      (m' ≫ f) w'

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : Eq (α := Z' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) ((m' ≫ f) ≫ Quiver.Hom.op NormalEpi.g) 0
a :
  ∀ (j : WalkingParallelPair),
    Eq (α :=
      Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0) j ⟶
        Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯))
      (NatTrans.app (Cocone.ι (CokernelCofork.ofπ f.unop ⋯)) j ≫ m'.unop :
        Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0) j ⟶
          Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
            (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯))
      (NatTrans.app (Cocone.ι (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯)) j :
        Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0) j ⟶
          Functor.obj.{0, v₁, 0, u₁}
            (Functor.obj (Functor.const WalkingParallelPair)
              (Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
                (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯)))
            j)
⊢ m'.unop =
    Quiver.Hom.unop
      ((fun {W' : Cᵒᵖ} (g' : W' ⟶ Y)
            (w' : Eq (α := W' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) (g' ≫ Quiver.Hom.op NormalEpi.g) 0) ↦
          (Quiver.Hom.op
              (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop ⋯) :
                (CokernelCofork.ofπ f.unop ⋯).pt ⟶ unop W') :
            op (unop W') ⟶
              op
                (Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
                  (CokernelCofork.ofπ f.unop ⋯))))
        (m' ≫ f) w')

Tactic:
apply m.isColimit.uniq (CokernelCofork.ofπ (f.unop ≫ m'.unop) _) m'.unop

Premises used: Quiver.Hom.unop, CategoryTheory.NormalEpi.isColimit, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.CokernelCofork.ofπ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : Eq (α := Z' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) ((m' ≫ f) ≫ Quiver.Hom.op NormalEpi.g) 0
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
        WalkingParallelPair.zero ⟶
      Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
        (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯))
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ f.unop ⋯)) WalkingParallelPair.zero ≫ m'.unop :
      Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          WalkingParallelPair.zero ⟶
        Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯))
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯)) WalkingParallelPair.zero :
      Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          WalkingParallelPair.zero ⟶
        Functor.obj.{0, v₁, 0, u₁}
          (Functor.obj (Functor.const WalkingParallelPair)
            (Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
              (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯)))
          WalkingParallelPair.zero)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : Eq (α := Z' ⟶ op (@NormalEpi.W _ _ _ _ inst_1 f.unop _)) ((m' ≫ f) ≫ Quiver.Hom.op NormalEpi.g) 0
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
        WalkingParallelPair.one ⟶
      Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
        (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯))
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ f.unop ⋯)) WalkingParallelPair.one ≫ m'.unop :
      Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          WalkingParallelPair.one ⟶
        Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯))
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯)) WalkingParallelPair.one :
      Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
          WalkingParallelPair.one ⟶
        Functor.obj.{0, v₁, 0, u₁}
          (Functor.obj (Functor.const WalkingParallelPair)
            (Cocone.pt (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 f.unop _) NormalEpi.g 0)
              (CokernelCofork.ofπ (f.unop ≫ m'.unop) ⋯)))
          WalkingParallelPair.one)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : IsNormalEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
haveI : ∀ (this : NormalEpi f), IsRegularEpi f
⊢ IsRegularEpi f

Tactic:
haveI := normalEpiOfEpi f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : IsNormalEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
this : NormalEpi f
⊢ IsRegularEpi f

Tactic:
infer_instance
-- 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)
rw rw₁ :
  Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ P) (kernel.ι (prod.lift f g) ≫ f)
    (kernel.ι (prod.lift f g) ≫ f)
⊢ Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ P) (kernel.ι (prod.lift f g) ≫ f)
    (kernel.ι (prod.lift f g) ≫ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) 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 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)
rw rw₁ :
  Eq.{v_1 + 1} (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ P)
    (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)
    (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)
⊢ Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ P)
    (kernel.ι (prod.lift f g) ≫ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) prod.fst)
    (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)

Tactic:
rw [kernel.condition_assoc]

Premises used: CategoryTheory.Limits.kernel.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 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)
rw rw₁ :
  Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ Q) (kernel.ι (prod.lift f g) ≫ g)
    (kernel.ι (prod.lift f g) ≫ g)
⊢ Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ Q) (kernel.ι (prod.lift f g) ≫ g)
    (kernel.ι (prod.lift f g) ≫ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) 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 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)
rw rw₁ :
  Eq.{v_1 + 1} (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ Q)
    (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
    (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
⊢ Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ Q)
    (kernel.ι (prod.lift f g) ≫ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) prod.snd)
    (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)

Tactic:
rw [kernel.condition_assoc]

Premises used: CategoryTheory.Limits.kernel.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 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)
rw : kernel.ι (prod.lift f g) = b' ≫ b
rw₁ rw₂ :
  Eq (α := kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g) ⟶ Z) (kernel.ι (prod.lift f g))
    (kernel.ι (prod.lift f g))
⊢ a' ≫ a = b' ≫ b

Tactic:
rw [dsimp% ha', dsimp% 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
⊢ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) ((s.snd ≫ b) ≫ prod.lift f g) prod.fst = s.snd ≫ b ≫ f

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 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 rw₁ : s.snd ≫ b ≫ f = s.snd ≫ b ≫ f
⊢ s.snd ≫ b ≫ f = s.fst ≫ a ≫ f

Tactic:
rw [PullbackCone.condition_assoc]

Premises used: CategoryTheory.Limits.PullbackCone.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 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 rw₁ : Eq (α := s.pt ⟶ P) (s.fst ≫ 0) (s.fst ≫ 0)
⊢ s.fst ≫ a ≫ f = s.fst ≫ 0

Tactic:
rw [haf]
-- 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 : Eq.{v_1 + 1} (α := s.pt ⟶ P) 0 (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)
rw₁ rw₂ : Eq.{v_1 + 1} (α := s.pt ⟶ P) 0 0
⊢ Eq (α := s.pt ⟶ P) (s.fst ≫ 0) (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)

Tactic:
rw [comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- 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
⊢ CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) ((s.snd ≫ b) ≫ prod.lift f g) prod.snd = s.snd ≫ b ≫ g

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

Premises used: CategoryTheory.Category.assoc, 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 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 rw₁ : Eq (α := s.pt ⟶ Q) (s.snd ≫ 0) (s.snd ≫ 0)
⊢ s.snd ≫ b ≫ g = s.snd ≫ 0

Tactic:
rw [hbg]
-- 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 : Eq.{v_1 + 1} (α := s.pt ⟶ Q) 0 (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)
rw₁ rw₂ : Eq.{v_1 + 1} (α := s.pt ⟶ Q) 0 0
⊢ Eq (α := s.pt ⟶ Q) (s.snd ≫ 0) (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.snd)

Tactic:
rw [comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- 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 :
  ∀ (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) ⋯ :
                s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
            s ≫
          a') ≫
        a =
      s.fst ≫ a
⊢ ((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

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

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' ≫ 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) ⋯ :
              s.pt ⟶ kernel (Y := Limits.prod.{v_1, u_1} P Q) (prod.lift f g)))
          s ≫
        a') ≫
      a =
    s.fst ≫ a

Tactic:
simp [ha', PullbackCone.condition s]

Premises used: CategoryTheory.Limits.PullbackCone.condition