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
e : S₁ ≅ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw : cyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.cycles
⊢ CategoryStruct.comp (Y := S₁.cycles) (cyclesMap e.inv) (cyclesMap e.hom) = 𝟙 S₂.cycles
have rw₁ : cyclesMap (𝟙 S₂) = 𝟙 S₂.cycles
Tactic: rw [← cyclesMap_comp, e.inv_hom_id, cyclesMap_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
e : S₁ ≅ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
rw : cyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.cycles
rw₁ : cyclesMap (𝟙 S₂) = 𝟙 S₂.cycles
⊢ CategoryStruct.comp (Y := S₁.cycles) (cyclesMap e.inv) (cyclesMap e.hom) = 𝟙 S₂.cycles
have rw₂ : Eq.{v_1 + 1} (α := S₂.cycles ⟶ S₂.cycles) (𝟙 S₂.cycles) (𝟙 S₂.cycles)
Tactic: rw [← cyclesMap_comp, e.inv_hom_id, cyclesMap_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
inst_2 : S.HasLeftHomology
⊢ Eq (α := S.cycles ⟶ S.X₂) (Iso.hom h.cyclesIso ≫ h.i) S.iCycles
have dsimp : cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i
Tactic: dsimp [iCycles, LeftHomologyData.cyclesIso]
-- 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
inst_2 : S.HasLeftHomology
⊢ Eq (α := S.cycles ⟶ h.H) (S.leftHomologyπ ≫ Iso.hom h.leftHomologyIso) (Iso.hom h.cyclesIso ≫ h.π)
have dsimp : S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π
Tactic: dsimp only [leftHomologyπ, leftHomologyIso, cyclesIso, leftHomologyMapIso',
    cyclesMapIso', Iso.refl]
-- 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
inst_2 : S.HasLeftHomology
⊢ S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π
have rw : S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h =
  S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h
Tactic: rw [← leftHomologyπ_naturality']
-- 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
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
    (Iso.hom h₁.leftHomologyIso ≫ γ.φH ≫ Iso.inv h₂.leftHomologyIso)
have dsimp : Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
  (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
Tactic: dsimp [LeftHomologyData.leftHomologyIso, leftHomologyMapIso']
-- 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
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
    (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
have rw : Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
  (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)
Tactic: rw [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp,
    ← leftHomologyMap'_comp, id_comp, 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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ) (Iso.hom h₁.cyclesIso ≫ γ.φK ≫ Iso.inv h₂.cyclesIso)
have dsimp : Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ)
  (cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
Tactic: dsimp [LeftHomologyData.cyclesIso, cyclesMapIso']
-- 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
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ)
    (cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
have rw : Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ) (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)
Tactic: rw [← γ.cyclesMap'_eq, ← cyclesMap'_comp, ← cyclesMap'_comp, id_comp, comp_id]
-- 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 ≫ φ.τ₂
⊢ S₂.LeftHomologyData
have wi : i ≫ S₂.g = 0
Tactic: have wi : i ≫ S₂.g = 0 := by simp only [i, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₂ : x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₃ : x ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0 ≫ φ.τ₃
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₃ : x ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0 ≫ φ.τ₃
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₄ : x ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0 ≫ φ.τ₃
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₃ : x ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₄ : x ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0 ≫ φ.τ₃
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₅ : x ≫ S₂.g = 0 ≫ φ.τ₃
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₃ : x ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₄ : x ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0 ≫ φ.τ₃
rw₅ : x ≫ S₂.g = 0 ≫ φ.τ₃
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₆ : Eq (α := W' ⟶ S₂.X₃) 0 (0 ≫ φ.τ₃)
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
rw : x ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₃ : x ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₄ : x ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0 ≫ φ.τ₃
rw₅ : x ≫ S₂.g = 0 ≫ φ.τ₃
rw₆ : Eq (α := W' ⟶ S₂.X₃) 0 (0 ≫ φ.τ₃)
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0
have rw₇ : Eq.{v_1 + 1} (α := W' ⟶ S₂.X₃) 0 0
Tactic: rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, 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 ≫ φ.τ₂
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 = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) sorry ≫ h.i
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) sorry ≫ h.i) ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₂ : b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) sorry ≫ h.i) ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₂ : b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₃ : b ≫ h.i ≫ φ.τ₂ = h.liftK (x ≫ inv φ.τ₂) sorry ≫ h.i ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₂ : b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₃ : b ≫ h.i ≫ φ.τ₂ = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i ≫ φ.τ₂
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₄ : b ≫ h.i ≫ φ.τ₂ = (x ≫ inv φ.τ₂) ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₂ : b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₃ : b ≫ h.i ≫ φ.τ₂ = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i ≫ φ.τ₂
rw₄ : b ≫ h.i ≫ φ.τ₂ = (x ≫ inv φ.τ₂) ≫ φ.τ₂
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₅ : b ≫ h.i ≫ φ.τ₂ = x ≫ inv φ.τ₂ ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₂ : b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₃ : b ≫ h.i ≫ φ.τ₂ = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i ≫ φ.τ₂
rw₄ : b ≫ h.i ≫ φ.τ₂ = (x ≫ inv φ.τ₂) ≫ φ.τ₂
rw₅ : b ≫ h.i ≫ φ.τ₂ = x ≫ inv φ.τ₂ ≫ φ.τ₂
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₆ : b ≫ h.i ≫ φ.τ₂ = x ≫ 𝟙 S₂.X₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
W' : C
x : W' ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i
rw₁ : (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₂ : b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
rw₃ : b ≫ h.i ≫ φ.τ₂ = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i ≫ φ.τ₂
rw₄ : b ≫ h.i ≫ φ.τ₂ = (x ≫ inv φ.τ₂) ≫ φ.τ₂
rw₅ : b ≫ h.i ≫ φ.τ₂ = x ≫ inv φ.τ₂ ≫ φ.τ₂
rw₆ : b ≫ h.i ≫ φ.τ₂ = x ≫ 𝟙 S₂.X₂
rw₇ : b ≫ h.i ≫ φ.τ₂ = x
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯
have rw₈ : x = x
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, 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
⊢ S₂.LeftHomologyData
have have : (hi : IsLimit (KernelFork.ofι i wi)) → S₂.LeftHomologyData
Tactic: have hi : IsLimit (KernelFork.ofι i wi) := KernelFork.IsLimit.ofι _ _
    (fun x hx => h.liftK (x ≫ inv φ.τ₂) (by rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, hx, zero_comp]))
    (fun x hx => by simp [i]) (fun x hx b hb => by
      dsimp
      rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, hb])
-- 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 ⋯)
⊢ φ.τ₁ ≫ f' = h.f'
have eq : hi.lift (KernelFork.ofι S₂.f sorry) ≫ Fork.ι (KernelFork.ofι i wi) = Fork.ι (KernelFork.ofι S₂.f sorry)
Tactic: have eq := @Fork.IsLimit.lift_ι _ _ _ _ _ _ _ ((KernelFork.ofι S₂.f S₂.zero)) hi
-- 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
⊢ φ.τ₁ ≫ f' = h.f'
have rw : (φ.τ₁ ≫ f') ≫ h.i = h.f' ≫ h.i
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
⊢ φ.τ₁ ≫ f' = h.f'
have rw₁ : ((φ.τ₁ ≫ f') ≫ h.i) ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
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) ≫ φ.τ₂
⊢ φ.τ₁ ≫ f' = h.f'
have rw₂ : (φ.τ₁ ≫ f') ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
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) ≫ φ.τ₂
⊢ φ.τ₁ ≫ f' = h.f'
have rw₃ : φ.τ₁ ≫ f' ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
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) ≫ φ.τ₂
⊢ φ.τ₁ ≫ f' = h.f'
have rw₄ : φ.τ₁ ≫ S₂.f = (h.f' ≫ h.i) ≫ φ.τ₂
Tactic: rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, f'_i, φ.comm₁₂]