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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
rw₁ : x ≫ S.f ≫ S.g = 0
rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
⊢ k ≫ S.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
Tactic: rw [hx, assoc, S.zero, 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ ≫ h.π = 0
have rw : h.liftK k sorry ≫ h.π = (x ≫ h.f') ≫ h.π
Tactic: rw [show 0 = (x ≫ h.f') ≫ h.π by simp]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ ≫ h.π = (x ≫ h.f') ≫ h.π
have e_a : h.liftK k sorry = x ≫ h.f'
Tactic: congr 1
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0
have rw : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) (𝟙 S.X₂ ≫ 0) 0
Tactic: rw [hg, id_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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hg : S.g = 0
rw : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) (𝟙 S.X₂ ≫ 0) 0
⊢ 𝟙 S.X₂ ≫ S.g = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [hg, id_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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
⊢ h.f' ≫ 𝟙 h.K = 0
have rw : (h.f' ≫ 𝟙 h.K) ≫ h.i = 0 ≫ h.i
Tactic: rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
rw : (h.f' ≫ 𝟙 h.K) ≫ h.i = 0 ≫ h.i
⊢ h.f' ≫ 𝟙 h.K = 0
have rw₁ : h.f' ≫ h.i = 0 ≫ h.i
Tactic: rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
rw : (h.f' ≫ 𝟙 h.K) ≫ h.i = 0 ≫ h.i
rw₁ : h.f' ≫ h.i = 0 ≫ h.i
⊢ h.f' ≫ 𝟙 h.K = 0
have rw₂ : S.f = 0 ≫ h.i
Tactic: rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
rw : (h.f' ≫ 𝟙 h.K) ≫ h.i = 0 ≫ h.i
rw₁ : h.f' ≫ h.i = 0 ≫ h.i
rw₂ : S.f = 0 ≫ h.i
rw₃ : S.f = 0
⊢ h.f' ≫ 𝟙 h.K = 0
have rw₄ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
⊢ IsIso h.π
have have : ∀ (φ : (CokernelCofork.ofπ h.π sorry).pt ⟶ h.K) (hφ : Cofork.π (CokernelCofork.ofπ h.π sorry) ≫ φ = 𝟙 h.K), IsIso h.π
Tactic: have ⟨φ, hφ⟩ := CokernelCofork.IsColimit.desc' h.hπ' (𝟙 _)
    (by rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf])
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
⊢ φ ≫ h.π = 𝟙 h.H
have rw : h.π ≫ φ ≫ h.π = h.π ≫ 𝟙 h.H
Tactic: rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
rw : h.π ≫ φ ≫ h.π = h.π ≫ 𝟙 h.H
⊢ φ ≫ h.π = 𝟙 h.H
have rw₁ : h.π = h.π ≫ 𝟙 h.H
Tactic: rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]
-- 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
rw : h.π ≫ φ ≫ h.π = h.π ≫ 𝟙 h.H
rw₁ : h.π = h.π ≫ 𝟙 h.H
⊢ φ ≫ h.π = 𝟙 h.H
have rw₂ : h.π = h.π
Tactic: rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]
-- 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
h : S.LeftHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
rw : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [id_comp, hg]
-- 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 : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
T : C
φ : T ⟶ S.X₂
⊢ (ofIsColimitCokernelCofork S hg c hc).liftK φ ⋯ = φ
have rw : φ = φ ≫ (ofIsColimitCokernelCofork S hg c hc).i
Tactic: rw [← cancel_mono (ofIsColimitCokernelCofork S hg c hc).i, liftK_i]
-- 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
h : S.LeftHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ S.X₂)
    (((hc.ofIsoLimit (Fork.ext (Iso.refl c.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ Fork.ι c) (0 ≫ Fork.ι c)
have dsimp : Eq (α := S.X₁ ⟶ S.X₂) (((hc.lift (KernelFork.ofι S.f sorry) ≫ 𝟙 c.pt) ≫ 𝟙 c.pt) ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
  (0 ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
Tactic: dsimp
-- 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
h : S.LeftHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ S.X₂)
    ((hc.ofIsoLimit (Fork.ext (Iso.refl c.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ Fork.ι c) (0 ≫ Fork.ι c)
have dsimp : Eq (α := S.X₁ ⟶ S.X₂) ((hc.lift (KernelFork.ofι S.f sorry) ≫ 𝟙 c.pt) ≫ Fork.ι c : S.X₁ ⟶ S.X₂) (0 ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
Tactic: dsimp
-- 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0
have rw : (ofIsLimitKernelFork S hf c hc).f' ≫ (ofIsLimitKernelFork S hf c hc).i = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
Tactic: rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).f' ≫ (ofIsLimitKernelFork S hf c hc).i = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0
have rw₁ : S.f = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
Tactic: rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).f' ≫ (ofIsLimitKernelFork S hf c hc).i = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
rw₁ : S.f = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0
have rw₂ : Eq (α := S.X₁ ⟶ S.X₂) 0 (0 ≫ (ofIsLimitKernelFork S hf c hc).i)
Tactic: rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).f' ≫ (ofIsLimitKernelFork S hf c hc).i = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
rw₁ : S.f = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
rw₂ : Eq (α := S.X₁ ⟶ S.X₂) 0 (0 ≫ (ofIsLimitKernelFork S hf c hc).i)
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, 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
h : S.LeftHomologyData
A : C
hf : S.f = 0
hg rw : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [id_comp, hg]
-- 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
h : S.LeftHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ S.X₂) ((KernelFork.IsLimit.ofId S.g hg).lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 S.X₂) 0
have change : S.f ≫ 𝟙 S.X₂ = 0
Tactic: change S.f ≫ 𝟙 _ = 0
-- 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
hg : S.g = 0
⊢ (ofZeros S hf hg).f' = 0
have rw : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0 ≫ (ofZeros S hf hg).i
Tactic: rw [← cancel_mono ((ofZeros S hf hg).i), zero_comp, f'_i, hf]
-- 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
hg : S.g = 0
rw : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0 ≫ (ofZeros S hf hg).i
⊢ (ofZeros S hf hg).f' = 0
have rw₁ : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0
Tactic: rw [← cancel_mono ((ofZeros S hf hg).i), zero_comp, f'_i, hf]
-- 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 : ShortComplex.{v_1, u_1} C
hf : S.f = 0
hg : S.g = 0
rw : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0 ≫ (ofZeros S hf hg).i
rw₁ : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0
rw₂ : S.f = 0
⊢ (ofZeros S hf hg).f' = 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [← cancel_mono ((ofZeros S hf hg).i), zero_comp, f'_i, hf]
-- 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
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (eK.hom ≫ h.i) ≫ S.g = 0
have rw : eK.hom ≫ h.i ≫ S.g = 0
Tactic: rw [assoc, h.wi, 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
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
rw : eK.hom ≫ h.i ≫ S.g = 0
⊢ (eK.hom ≫ h.i) ≫ S.g = 0
have rw₁ : Eq (α := K' ⟶ S.X₃) (eK.hom ≫ 0) 0
Tactic: rw [assoc, h.wi, 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
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
rw : eK.hom ≫ h.i ≫ S.g = 0
rw₁ : Eq (α := K' ⟶ S.X₃) (eK.hom ≫ 0) 0
⊢ (eK.hom ≫ h.i) ≫ S.g = 0
have rw₂ : Eq.{v_1 + 1} (α := K' ⟶ S.X₃) 0 0
Tactic: rw [assoc, h.wi, 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ ψ₁.φK = ψ₂.φK
have rw : ψ₁.φK ≫ h₂.i = ψ₂.φK ≫ h₂.i
Tactic: rw [← cancel_mono h₂.i, commi, commi]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
rw : ψ₁.φK ≫ h₂.i = ψ₂.φK ≫ h₂.i
⊢ ψ₁.φK = ψ₂.φK
have rw₁ : h₁.i ≫ φ.τ₂ = ψ₂.φK ≫ h₂.i
Tactic: rw [← cancel_mono h₂.i, commi, commi]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
rw : ψ₁.φK ≫ h₂.i = ψ₂.φK ≫ h₂.i
rw₁ : h₁.i ≫ φ.τ₂ = ψ₂.φK ≫ h₂.i
⊢ ψ₁.φK = ψ₂.φK
have rw₂ : h₁.i ≫ φ.τ₂ = h₁.i ≫ φ.τ₂
Tactic: rw [← cancel_mono h₂.i, commi, commi]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ ψ₁ = ψ₂
have hK : ψ₁.φK = ψ₂.φK
Tactic: have hK : ψ₁.φK = ψ₂.φK := by rw [← cancel_mono h₂.i, commi, commi]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ ψ₁.φH = ψ₂.φH
have rw : h₁.π ≫ ψ₁.φH = h₁.π ≫ ψ₂.φH
Tactic: rw [← cancel_epi h₁.π, commπ, commπ, hK]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
rw : h₁.π ≫ ψ₁.φH = h₁.π ≫ ψ₂.φH
⊢ ψ₁.φH = ψ₂.φH
have rw₁ : ψ₁.φK ≫ h₂.π = h₁.π ≫ ψ₂.φH
Tactic: rw [← cancel_epi h₁.π, commπ, commπ, hK]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
rw : h₁.π ≫ ψ₁.φH = h₁.π ≫ ψ₂.φH
rw₁ : ψ₁.φK ≫ h₂.π = h₁.π ≫ ψ₂.φH
⊢ ψ₁.φH = ψ₂.φH
have rw₂ : ψ₁.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π
Tactic: rw [← cancel_epi h₁.π, commπ, commπ, hK]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
rw : h₁.π ≫ ψ₁.φH = h₁.π ≫ ψ₂.φH
rw₁ : ψ₁.φK ≫ h₂.π = h₁.π ≫ ψ₂.φH
rw₂ : ψ₁.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π
⊢ ψ₁.φH = ψ₂.φH
have rw₃ : ψ₂.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π
Tactic: rw [← cancel_epi h₁.π, commπ, commπ, hK]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ ψ₁ = ψ₂
have hH : ψ₁.φH = ψ₂.φH
Tactic: have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_epi h₁.π, commπ, commπ, hK]
-- 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
hH : ψ₁.φH = ψ₂.φH
⊢ ψ₁ = ψ₂
have mk : ∀ (φK : h₁.K ⟶ h₂.K) (φH : h₁.H ⟶ h₂.H) (commi : φK ≫ h₂.i = h₁.i ≫ φ.τ₂) (commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f')
  (commπ : h₁.π ≫ φH = φK ≫ h₂.π)
  (hK :
    { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φK = ψ₂.φK)
  (hH :
    { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φH = ψ₂.φH),
  { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } = ψ₂
Tactic: cases ψ₁
Cleared hypotheses: ψ₁, hK, hH
-- 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
h₂ : S₂.LeftHomologyData
ψ₂ : LeftHomologyMapData φ h₁ h₂
φK : h₁.K ⟶ h₂.K
φH : h₁.H ⟶ h₂.H
commi : φK ≫ h₂.i = h₁.i ≫ φ.τ₂
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
commπ : h₁.π ≫ φH = φK ≫ h₂.π
hK : { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φK = ψ₂.φK
hH : { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φH = ψ₂.φH
⊢ { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } = ψ₂
have mk : ∀ (φK_1 : h₁.K ⟶ h₂.K) (φH_1 : h₁.H ⟶ h₂.H) (commi_1 : φK_1 ≫ h₂.i = h₁.i ≫ φ.τ₂)
  (commf'_1 : h₁.f' ≫ φK_1 = φ.τ₁ ≫ h₂.f') (commπ_1 : h₁.π ≫ φH_1 = φK_1 ≫ h₂.π)
  (hK :
    { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φK =
      { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 :
          LeftHomologyMapData φ h₁ h₂ }.φK)
  (hH :
    { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φH =
      { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 :
          LeftHomologyMapData φ h₁ h₂ }.φH),
  { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } =
    { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 }
Tactic: cases ψ₂
Cleared hypotheses: ψ₂, hK, hH
-- 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
h₂ : S₂.LeftHomologyData
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0
have rw : h₁.i ≫ φ.τ₂ ≫ S₂.g = 0
Tactic: rw [assoc, φ.comm₂₃, h₁.wi_assoc, 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
h₂ : S₂.LeftHomologyData
rw : h₁.i ≫ φ.τ₂ ≫ S₂.g = 0
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0
have rw₁ : h₁.i ≫ S₁.g ≫ φ.τ₃ = 0
Tactic: rw [assoc, φ.comm₂₃, h₁.wi_assoc, 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
h₂ : S₂.LeftHomologyData
rw : h₁.i ≫ φ.τ₂ ≫ S₂.g = 0
rw₁ : h₁.i ≫ S₁.g ≫ φ.τ₃ = 0
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0
have rw₂ : Eq (α := h₁.K ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [assoc, φ.comm₂₃, h₁.wi_assoc, 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
h₂ : S₂.LeftHomologyData
rw : h₁.i ≫ φ.τ₂ ≫ S₂.g = 0
rw₁ : h₁.i ≫ S₁.g ≫ φ.τ₃ = 0
rw₂ : Eq (α := h₁.K ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0
have rw₃ : Eq.{v_1 + 1} (α := h₁.K ⟶ S₂.X₃) 0 0
Tactic: rw [assoc, φ.comm₂₃, h₁.wi_assoc, 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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw : (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
Tactic: rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
rw : (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw₁ : h₁.f' ≫ φK ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
Tactic: rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
rw : (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
rw₁ : h₁.f' ≫ φK ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw₂ : h₁.f' ≫ φK ≫ h₂.i = φ.τ₁ ≫ h₂.f' ≫ h₂.i
Tactic: rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
rw : (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
rw₁ : h₁.f' ≫ φK ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
rw₂ : h₁.f' ≫ φK ≫ h₂.i = φ.τ₁ ≫ h₂.f' ≫ h₂.i
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw₃ : h₁.f' ≫ h₁.i ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
Tactic: rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i, φ.comm₁₂]