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 : 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
rw : (m ≫ equalizer.ι u v) ≫ w = 0
⊢ f ≫ w = 0
have rw₁ : m ≫ equalizer.ι u v ≫ w = 0
Tactic: rw [← hm, Category.assoc, hw, comp_zero]
-- 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
rw : (m ≫ equalizer.ι u v) ≫ w = 0
rw₁ : m ≫ equalizer.ι u v ≫ w = 0
⊢ f ≫ w = 0
have rw₂ : Eq (α := X ⟶ W) (m ≫ 0) 0
Tactic: rw [← hm, Category.assoc, hw, comp_zero]
-- 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
rw : (m ≫ equalizer.ι u v) ≫ w = 0
rw₁ : m ≫ equalizer.ι u v ≫ w = 0
rw₂ : Eq (α := X ⟶ W) (m ≫ 0) 0
⊢ f ≫ w = 0
have rw₃ : Eq.{v_1 + 1} (α := X ⟶ W) 0 0
Tactic: rw [← hm, Category.assoc, hw, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
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
⊢ u = v
have hwf : f ≫ w = 0
Tactic: have hwf : f ≫ w = 0 := by rw [← hm, Category.assoc, hw, comp_zero]
-- 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
hwf : f ≫ w = 0
⊢ u = v
have obtain : ∀ (n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 sorry) ⟶ W)
  (hn : Cofork.π (CokernelCofork.ofπ (Z := Z) 0 sorry) ≫ n = w), u = v
Tactic: obtain ⟨n, hn⟩ := CokernelCofork.IsColimit.desc' l _ hwf
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
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
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : Cofork.π (CokernelCofork.ofπ (Z := Z) 0 ⋯) ≫ n = w
⊢ u = v
have hn₁ : 0 = w
Tactic: rw [Cofork.π_ofπ, zero_comp] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
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
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
⊢ u = v
have this : IsIso (X := equalizer u v) (equalizer.ι u v)
Tactic: have : IsIso (equalizer.ι u v) := by apply isIso_limit_cone_parallelPair_of_eq hn.symm hl
-- 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
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
this : IsIso (X := equalizer u v) (equalizer.ι u v)
⊢ u = v
have apply : Eq (α := equalizer u v ⟶ Z_1) (equalizer.ι u v ≫ u) (equalizer.ι u v ≫ v)
Tactic: apply (cancel_epi (equalizer.ι u v)).1
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
⊢ Eq (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (f ≫ cokernel.π (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))
have rw : Eq (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (f ≫ cokernel.π (coprod.desc f g))
  (f ≫ cokernel.π (coprod.desc f g))
Tactic: rw [coprod.inl_desc_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
⊢ Eq (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
have rw : Eq.{v_1 + 1} (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
  (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
  (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
Tactic: rw [cokernel.condition]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
⊢ Eq (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (g ≫ cokernel.π (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))
have rw : Eq (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (g ≫ cokernel.π (coprod.desc f g))
  (g ≫ cokernel.π (coprod.desc f g))
Tactic: rw [coprod.inr_desc_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
⊢ Eq (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
have rw : Eq.{v_1 + 1} (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
  (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
  (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
Tactic: rw [cokernel.condition]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : a ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
⊢ a ≫ a' = b ≫ b'
have rw : cokernel.π (coprod.desc f g) = b ≫ b'
Tactic: rw [ha', 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : a ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
rw : cokernel.π (coprod.desc f g) = b ≫ b'
⊢ a ≫ a' = b ≫ b'
have rw₁ : Eq (α := X ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (cokernel.π (coprod.desc f g))
  (cokernel.π (coprod.desc f g))
Tactic: rw [ha', 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl (coprod.desc f g ≫ b ≫ s.inr) = f ≫ b ≫ s.inr
have rw : f ≫ b ≫ s.inr = f ≫ b ≫ s.inr
Tactic: rw [coprod.inl_desc_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ f ≫ b ≫ s.inr = f ≫ a ≫ s.inl
have rw : f ≫ b ≫ s.inr = f ≫ b ≫ s.inr
Tactic: rw [PushoutCocone.condition]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ f ≫ a ≫ s.inl = 0 ≫ s.inl
have rw : (f ≫ a) ≫ s.inl = 0 ≫ s.inl
Tactic: rw [← Category.assoc, eq_whisker hfa]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : (f ≫ a) ≫ s.inl = 0 ≫ s.inl
⊢ f ≫ a ≫ s.inl = 0 ≫ s.inl
have rw₁ : Eq (α := P ⟶ s.pt) (0 ≫ s.inl) (0 ≫ s.inl)
Tactic: rw [← Category.assoc, eq_whisker hfa]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ Eq (α := P ⟶ s.pt) (0 ≫ s.inl) (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
have rw : Eq (α := P ⟶ s.pt) (0 ≫ s.inl) 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : Eq (α := P ⟶ s.pt) (0 ≫ s.inl) 0
⊢ Eq (α := P ⟶ s.pt) (0 ≫ s.inl) (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
have rw₁ : Eq.{v_1 + 1} (α := P ⟶ s.pt) 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr (coprod.desc f g ≫ b ≫ s.inr) = g ≫ b ≫ s.inr
have rw : g ≫ b ≫ s.inr = g ≫ b ≫ s.inr
Tactic: rw [coprod.inr_desc_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ g ≫ b ≫ s.inr = 0 ≫ s.inr
have rw : (g ≫ b) ≫ s.inr = 0 ≫ s.inr
Tactic: rw [← Category.assoc, eq_whisker hgb]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : (g ≫ b) ≫ s.inr = 0 ≫ s.inr
⊢ g ≫ b ≫ s.inr = 0 ≫ s.inr
have rw₁ : Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) (0 ≫ s.inr)
Tactic: rw [← Category.assoc, eq_whisker hgb]
-- 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
have rw : Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) 0
⊢ Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
have rw₁ : Eq.{v_1 + 1} (α := Q ⟶ s.pt) 0 0
Tactic: rw [comp_zero, zero_comp]