awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) ((NormalEpi.g ≫ f) ≫ h) 0
have rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ f ≫ h) 0
Tactic: rw [Category.assoc, comm, reassoc', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ f ≫ h) 0
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) ((NormalEpi.g ≫ f) ≫ h) 0
have rw₁ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ g ≫ k) 0
Tactic: rw [Category.assoc, comm, reassoc', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ f ≫ h) 0
rw₁ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ g ≫ k) 0
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) ((NormalEpi.g ≫ f) ≫ h) 0
have rw₂ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (0 ≫ k) 0
Tactic: rw [Category.assoc, comm, reassoc', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ f ≫ h) 0
rw₁ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (NormalEpi.g ≫ g ≫ k) 0
rw₂ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) (0 ≫ k) 0
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) ((NormalEpi.g ≫ f) ≫ h) 0
have rw₃ : Eq.{v₁ + 1} (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) 0 0
Tactic: rw [Category.assoc, comm, reassoc', zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular (NormalEpi.regularEpi g) comm t
⊢ IsColimit (F := parallelPair (X := @NormalEpi.W _ _ _ _ inst_1 g _) (NormalEpi.g ≫ f) 0) (CokernelCofork.ofπ h ⋯)
have q : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ Q) 0 (0 ≫ f)
Tactic: have q := (@zero_comp _ _ _ gn.W _ _ f).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') ((g ≫ Arrow.Hom.left e.hom) ≫ f') 0
have this : Arrow.Hom.left e.hom ≫ (Arrow.mk f').hom = (Arrow.mk f).hom ≫ Arrow.Hom.right e.hom
Tactic: have := Arrow.w e.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.hom ≫ f' = f ≫ Arrow.Hom.right e.hom
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') ((g ≫ Arrow.Hom.left e.hom) ≫ f') 0
have rw : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ Arrow.Hom.left e.hom ≫ f') 0
Tactic: rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.hom ≫ f' = f ≫ Arrow.Hom.right e.hom
rw : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ Arrow.Hom.left e.hom ≫ f') 0
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') ((g ≫ Arrow.Hom.left e.hom) ≫ f') 0
have rw₁ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ f ≫ Arrow.Hom.right e.hom) 0
Tactic: rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.hom ≫ f' = f ≫ Arrow.Hom.right e.hom
rw : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ Arrow.Hom.left e.hom ≫ f') 0
rw₁ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ f ≫ Arrow.Hom.right e.hom) 0
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') ((g ≫ Arrow.Hom.left e.hom) ≫ f') 0
have rw₂ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (0 ≫ Arrow.Hom.right e.hom) 0
Tactic: rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.hom ≫ f' = f ≫ Arrow.Hom.right e.hom
rw : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ Arrow.Hom.left e.hom ≫ f') 0
rw₁ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (g ≫ f ≫ Arrow.Hom.right e.hom) 0
rw₂ : Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') (0 ≫ Arrow.Hom.right e.hom) 0
⊢ Eq (α := @W _ _ _ _ inst_1 f _ ⟶ Y') ((g ≫ Arrow.Hom.left e.hom) ≫ f') 0
have rw₃ : Eq.{v₁ + 1} (α := @W _ _ _ _ inst_1 f _ ⟶ Y') 0 0
Tactic: rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ IsColimit (CokernelCofork.ofπ f' ⋯)
have refine_1 : parallelPair (X := @W _ _ _ _ inst_1 f _) g 0 ≅ parallelPair (X := @W _ _ _ _ inst_1 f _) (g ≫ Arrow.Hom.left e.hom) 0
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
refine_1 :
  parallelPair (X := @W _ _ _ _ inst_1 f _) g 0 ≅ parallelPair (X := @W _ _ _ _ inst_1 f _) (g ≫ Arrow.Hom.left e.hom) 0
⊢ IsColimit (CokernelCofork.ofπ f' ⋯)
have refine_2 : Functor.obj
    (Cocone.precompose
      (Iso.inv
        (parallelPair.ext
          (Iso.refl
            (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := @W _ _ _ _ inst_1 f _) g 0) WalkingParallelPair.zero))
          (Functor.mapIso Arrow.leftFunc e) sorry sorry)))
    (CokernelCofork.ofπ f sorry) ≅
  CokernelCofork.ofπ f' sorry
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
⊢ m' =
    (fun {Z' : Cᵒᵖ} (g' : X ⟶ Z')
          (w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ g') 0) ↦
        (Quiver.Hom.op
            (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop ⋯) : unop Z' ⟶ (KernelFork.ofι f.unop ⋯).pt) :
          op
              (Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
                (KernelFork.ofι f.unop ⋯)) ⟶
            op (unop Z')))
      (f ≫ m') w'
have a : m'.unop =
  Quiver.Hom.unop
    ((fun {Z' : Cᵒᵖ} (g' : X ⟶ Z')
          (w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ g') 0) ↦
        (Quiver.Hom.op
            (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop sorry) : unop Z' ⟶ (KernelFork.ofι f.unop sorry).pt) :
          op
              (Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
                (KernelFork.ofι f.unop sorry)) ⟶
            op (unop Z')))
      (f ≫ m') w')
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
⊢ m'.unop =
    Quiver.Hom.unop
      ((fun {Z' : Cᵒᵖ} (g' : X ⟶ Z')
            (w' : Eq (α := op (@NormalMono.Z _ _ _ _ inst_1 f.unop _) ⟶ Z') (Quiver.Hom.op NormalMono.g ≫ g') 0) ↦
          (Quiver.Hom.op
              (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop ⋯) : unop Z' ⟶ (KernelFork.ofι f.unop ⋯).pt) :
            op
                (Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
                  (KernelFork.ofι f.unop ⋯)) ⟶
              op (unop Z')))
        (f ≫ m') w')
have a : ∀ (j : WalkingParallelPair),
  Eq (α :=
    Cone.pt (F := parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0)
        (KernelFork.ofι (m'.unop ≫ f.unop) sorry) ⟶
      Functor.obj.{0, v₁, 0, u₁}
        (parallelPair (X := unop X) (Y := @NormalMono.Z _ _ _ _ inst_1 f.unop _) NormalMono.g 0) j)
    (m'.unop ≫ NatTrans.app (Cone.π (KernelFork.ofι f.unop sorry)) j)
    (NatTrans.app (Cone.π (KernelFork.ofι (m'.unop ≫ f.unop) sorry)) j)
Tactic: apply m.isLimit.uniq (KernelFork.ofι (m'.unop ≫ f.unop) _) m'.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
⊢ 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'
have 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 sorry) :
              (CokernelCofork.ofπ f.unop sorry).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 sorry))))
      (m' ≫ f) w')
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
⊢ 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')
have 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) sorry))
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ f.unop sorry)) 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) sorry))
    (NatTrans.app (Cocone.ι (CokernelCofork.ofπ (f.unop ≫ m'.unop) sorry)) 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) sorry)))
          j)
Tactic: apply m.isColimit.uniq (CokernelCofork.ofπ (f.unop ≫ m'.unop) _) m'.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
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
⊢ IsRegularEpi f
have haveI : ∀ (this : NormalEpi f), IsRegularEpi f
Tactic: haveI := normalEpiOfEpi f
-- 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)
⊢ 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)
have 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)
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 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)
⊢ 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)
have 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)
Tactic: rw [kernel.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 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)
⊢ 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)
have 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)
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 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)
⊢ 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)
have 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)
Tactic: rw [kernel.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 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)
⊢ a' ≫ a = b' ≫ b
have rw : kernel.ι (prod.lift f g) = b' ≫ b
Tactic: rw [dsimp% ha', dsimp% hb']
-- 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)
rw : kernel.ι (prod.lift f g) = b' ≫ b
⊢ a' ≫ a = b' ≫ b
have 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))
Tactic: rw [dsimp% ha', dsimp% hb']
-- 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 ≫ f = s.fst ≫ a ≫ f
have rw : s.snd ≫ b ≫ f = s.snd ≫ b ≫ f
Tactic: rw [PullbackCone.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 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.fst ≫ a ≫ f = s.fst ≫ 0
have rw : Eq (α := s.pt ⟶ P) (s.fst ≫ 0) (s.fst ≫ 0)
Tactic: rw [haf]
-- 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 ⟶ 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 (CategoryStruct.comp (Y := Limits.prod.{v_1, u_1} P Q) 0 prod.fst)
Tactic: rw [comp_zero, zero_comp]