awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
rw : (φ.τ₁ ≫ f') ≫ h.i = h.f' ≫ h.i
rw₁ : ((φ.τ₁ ≫ f') ≫ h.i) ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₂ : (φ.τ₁ ≫ f') ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₃ : φ.τ₁ ≫ f' ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₄ : φ.τ₁ ≫ S₂.f = (h.f' ≫ h.i) ≫ φ.τ₂
⊢ φ.τ₁ ≫ f' = h.f'
have rw₅ : φ.τ₁ ≫ S₂.f = S₁.f ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, f'_i, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
rw : (φ.τ₁ ≫ f') ≫ h.i = h.f' ≫ h.i
rw₁ : ((φ.τ₁ ≫ f') ≫ h.i) ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₂ : (φ.τ₁ ≫ f') ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₃ : φ.τ₁ ≫ f' ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₄ : φ.τ₁ ≫ S₂.f = (h.f' ≫ h.i) ≫ φ.τ₂
rw₅ : φ.τ₁ ≫ S₂.f = S₁.f ≫ φ.τ₂
⊢ φ.τ₁ ≫ f' = h.f'
have rw₆ : S₁.f ≫ φ.τ₂ = S₁.f ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, f'_i, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
⊢ S₂.LeftHomologyData
have hf' : φ.τ₁ ≫ f' = h.f'
Tactic: have hf' : φ.τ₁ ≫ f' = h.f' := by
    have eq := @Fork.IsLimit.lift_ι _ _ _ _ _ _ _ ((KernelFork.ofι S₂.f S₂.zero)) hi
    simp only [Fork.ι_ofι] at eq
    rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, f'_i, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
⊢ f' ≫ h.π = 0
have rw : φ.τ₁ ≫ f' ≫ h.π = φ.τ₁ ≫ 0
Tactic: rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
rw : φ.τ₁ ≫ f' ≫ h.π = φ.τ₁ ≫ 0
⊢ f' ≫ h.π = 0
have rw₁ : φ.τ₁ ≫ f' ≫ h.π = 0
Tactic: rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
rw : φ.τ₁ ≫ f' ≫ h.π = φ.τ₁ ≫ 0
rw₁ : φ.τ₁ ≫ f' ≫ h.π = 0
⊢ f' ≫ h.π = 0
have rw₂ : h.f' ≫ h.π = 0
Tactic: rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
rw : φ.τ₁ ≫ f' ≫ h.π = φ.τ₁ ≫ 0
rw₁ : φ.τ₁ ≫ f' ≫ h.π = 0
rw₂ : h.f' ≫ h.π = 0
⊢ f' ≫ h.π = 0
have rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ h.H) 0 0
Tactic: rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
⊢ S₂.LeftHomologyData
have wπ : f' ≫ h.π = 0
Tactic: have wπ : f' ≫ h.π = 0 := by
    rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
⊢ h.f' ≫ x = 0
have rw : (φ.τ₁ ≫ f') ≫ x = 0
Tactic: rw [← hf', assoc, hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : (φ.τ₁ ≫ f') ≫ x = 0
⊢ h.f' ≫ x = 0
have rw₁ : φ.τ₁ ≫ f' ≫ x = 0
Tactic: rw [← hf', assoc, hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : (φ.τ₁ ≫ f') ≫ x = 0
rw₁ : φ.τ₁ ≫ f' ≫ x = 0
⊢ h.f' ≫ x = 0
have rw₂ : Eq (α := S₁.X₁ ⟶ Z') (φ.τ₁ ≫ 0) 0
Tactic: rw [← hf', assoc, hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : (φ.τ₁ ≫ f') ≫ x = 0
rw₁ : φ.τ₁ ≫ f' ≫ x = 0
rw₂ : Eq (α := S₁.X₁ ⟶ Z') (φ.τ₁ ≫ 0) 0
⊢ h.f' ≫ x = 0
have rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ Z') 0 0
Tactic: rw [← hf', assoc, hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
b : h.H ⟶ Z'
hb : h.π ≫ b = x
⊢ b = (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx
have rw : h.π ≫ b = h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x sorry) x hx
Tactic: rw [← cancel_epi h.π, π_descH, hb]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
b : h.H ⟶ Z'
hb : h.π ≫ b = x
rw : h.π ≫ b = h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx
rw₁ : h.π ≫ b = x
⊢ b = (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx
have rw₂ : x = x
Tactic: rw [← cancel_epi h.π, π_descH, hb]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
⊢ S₂.LeftHomologyData
have have : (hπ : IsColimit (CokernelCofork.ofπ h.π wπ)) → S₂.LeftHomologyData
Tactic: have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) := CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => h.descH x (by rw [← hf', assoc, hx, comp_zero]))
    (fun x hx => by simp) (fun x hx b hb => by rw [← cancel_epi h.π, π_descH, hb])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
have rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
have rw₁ : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₁ : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
have rw₂ : φ.τ₁ ≫ S₂.f = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₁ : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₂ : φ.τ₁ ≫ S₂.f = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
have rw₃ : φ.τ₁ ≫ S₂.f = h.f' ≫ h.i ≫ φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₁ : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₂ : φ.τ₁ ≫ S₂.f = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₃ : φ.τ₁ ≫ S₂.f = h.f' ≫ h.i ≫ φ.τ₂
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
have rw₄ : φ.τ₁ ≫ S₂.f = S₁.f ≫ φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₁ : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₂ : φ.τ₁ ≫ S₂.f = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₃ : φ.τ₁ ≫ S₂.f = h.f' ≫ h.i ≫ φ.τ₂
rw₄ : φ.τ₁ ≫ S₂.f = S₁.f ≫ φ.τ₂
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
have rw₅ : S₁.f ≫ φ.τ₂ = S₁.f ≫ φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
⊢ i ≫ S₁.g = 0
have rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
⊢ i ≫ S₁.g = 0
have rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
⊢ i ≫ S₁.g = 0
have rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
⊢ i ≫ S₁.g = 0
have rw₃ : h.i ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₃ : h.i ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
⊢ i ≫ S₁.g = 0
have rw₄ : h.i ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₃ : h.i ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₄ : h.i ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0
⊢ i ≫ S₁.g = 0
have rw₅ : h.i ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₃ : h.i ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₄ : h.i ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0
rw₅ : h.i ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0
⊢ i ≫ S₁.g = 0
have rw₆ : h.i ≫ S₂.g = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₃ : h.i ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₄ : h.i ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0
rw₅ : h.i ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0
rw₆ : h.i ≫ S₂.g = 0
⊢ i ≫ S₁.g = 0
have rw₇ : Eq.{v_1 + 1} (α := h.K ⟶ S₂.X₃) 0 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
⊢ S₁.LeftHomologyData
have wi : i ≫ S₁.g = 0
Tactic: have wi : i ≫ S₁.g = 0 := by
    rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ (x ≫ φ.τ₂) ≫ S₂.g = 0
have rw : x ≫ φ.τ₂ ≫ S₂.g = 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
rw : x ≫ φ.τ₂ ≫ S₂.g = 0
⊢ (x ≫ φ.τ₂) ≫ S₂.g = 0
have rw₁ : x ≫ S₁.g ≫ φ.τ₃ = 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
rw : x ≫ φ.τ₂ ≫ S₂.g = 0
rw₁ : x ≫ S₁.g ≫ φ.τ₃ = 0
⊢ (x ≫ φ.τ₂) ≫ S₂.g = 0
have rw₂ : Eq (α := W' ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
rw : x ≫ φ.τ₂ ≫ S₂.g = 0
rw₁ : x ≫ S₁.g ≫ φ.τ₃ = 0
rw₂ : Eq (α := W' ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ (x ≫ φ.τ₂) ≫ S₂.g = 0
have rw₃ : Eq.{v_1 + 1} (α := W' ⟶ S₂.X₃) 0 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx
have rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) sorry) x hx ≫ h.i
Tactic: rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]