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
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
rw₃ : h₁.f' ≫ h₁.i ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw₄ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ 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
rw₃ : h₁.f' ≫ h₁.i ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
rw₄ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw₅ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ S₂.f
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
rw₃ : h₁.f' ≫ h₁.i ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
rw₄ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
rw₅ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ S₂.f
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
have rw₆ : S₁.f ≫ φ.τ₂ = S₁.f ≫ φ.τ₂
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 (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
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ LeftHomologyMapData φ h₁ h₂
have commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
Tactic: have commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f' := by
    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 ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
⊢ h₁.f' ≫ φK ≫ h₂.π = 0
have rw : φ.τ₁ ≫ h₂.f' ≫ h₂.π = 0
Tactic: rw [reassoc_of% commf', h₂.f'_π, 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
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
rw : φ.τ₁ ≫ h₂.f' ≫ h₂.π = 0
⊢ h₁.f' ≫ φK ≫ h₂.π = 0
have rw₁ : Eq (α := S₁.X₁ ⟶ h₂.H) (φ.τ₁ ≫ 0) 0
Tactic: rw [reassoc_of% commf', h₂.f'_π, 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
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
rw : φ.τ₁ ≫ h₂.f' ≫ h₂.π = 0
rw₁ : Eq (α := S₁.X₁ ⟶ h₂.H) (φ.τ₁ ≫ 0) 0
⊢ h₁.f' ≫ φK ≫ h₂.π = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ h₂.H) 0 0
Tactic: rw [reassoc_of% commf', h₂.f'_π, 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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φH = γ₂.φH
have rw : γ₂.φH = γ₂.φH
Tactic: rw [eq]
-- 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₂
eq : γ₁ = γ₂
⊢ γ₁.φK = γ₂.φK
have rw : γ₂.φK = γ₂.φK
Tactic: rw [eq]
-- 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
inst_2 : S.HasLeftHomology
A : C
f₁ f₂ : S.leftHomology ⟶ A
⊢ f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂
have rw : f₁ = f₂ ↔ f₁ = f₂
Tactic: rw [cancel_epi]
-- 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
inst_2 : S.HasLeftHomology
A : C
f₁ f₂ : A ⟶ S.cycles
⊢ f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles
have rw : f₁ = f₂ ↔ f₁ = f₂
Tactic: rw [cancel_mono]
-- 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
inst_2 : S.HasLeftHomology
hg : S.g = 0
⊢ S.cycles ≅ S.X₂
have this : IsIso (X := S.cycles) S.iCycles
Tactic: have := S.isIso_iCycles hg
-- 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
inst_2 : S.HasLeftHomology
hf : S.f = 0
⊢ S.cycles ≅ S.leftHomology
have this : IsIso (X := S.cycles) S.leftHomologyπ
Tactic: have := S.isIso_leftHomologyπ 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃
have rw : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ leftHomologyMap' φ₂ h₂ h₃
Tactic: rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
rw : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ leftHomologyMap' φ₂ h₂ h₃
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃
have rw₁ : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
Tactic: rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
rw : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ leftHomologyMap' φ₂ h₂ h₃
rw₁ : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃
have rw₂ : (γ₁.comp γ₂).φH = γ₁.φH ≫ γ₂.φH
Tactic: rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
rw : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ leftHomologyMap' φ₂ h₂ h₃
rw₁ : leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
rw₂ : (γ₁.comp γ₂).φH = γ₁.φH ≫ γ₂.φH
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃
have rw₃ : γ₁.φH ≫ γ₂.φH = γ₁.φH ≫ γ₂.φH
Tactic: rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃
have rw : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ cyclesMap' φ₂ h₂ h₃
Tactic: rw [γ₁.cyclesMap'_eq, γ₂.cyclesMap'_eq, (γ₁.comp γ₂).cyclesMap'_eq,
    LeftHomologyMapData.comp_φK]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
rw : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ cyclesMap' φ₂ h₂ h₃
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃
have rw₁ : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ γ₂.φK
Tactic: rw [γ₁.cyclesMap'_eq, γ₂.cyclesMap'_eq, (γ₁.comp γ₂).cyclesMap'_eq,
    LeftHomologyMapData.comp_φK]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
rw : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ cyclesMap' φ₂ h₂ h₃
rw₁ : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ γ₂.φK
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃
have rw₂ : (γ₁.comp γ₂).φK = γ₁.φK ≫ γ₂.φK
Tactic: rw [γ₁.cyclesMap'_eq, γ₂.cyclesMap'_eq, (γ₁.comp γ₂).cyclesMap'_eq,
    LeftHomologyMapData.comp_φK]
-- 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₃ : ShortComplex.{v_1, u_1} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
rw : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ cyclesMap' φ₂ h₂ h₃
rw₁ : cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φK ≫ γ₂.φK
rw₂ : (γ₁.comp γ₂).φK = γ₁.φK ≫ γ₂.φK
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃
have rw₃ : γ₁.φK ≫ γ₂.φK = γ₁.φK ≫ γ₂.φK
Tactic: rw [γ₁.cyclesMap'_eq, γ₂.cyclesMap'_eq, (γ₁.comp γ₂).cyclesMap'_eq,
    LeftHomologyMapData.comp_φK]
-- 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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' e.hom h₁ h₂ ≫ leftHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
have rw : leftHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
Tactic: rw [← leftHomologyMap'_comp, e.hom_inv_id, leftHomologyMap'_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
⊢ leftHomologyMap' e.hom h₁ h₂ ≫ leftHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
have rw₁ : leftHomologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.H
Tactic: rw [← leftHomologyMap'_comp, e.hom_inv_id, leftHomologyMap'_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
rw₁ : leftHomologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.H
⊢ leftHomologyMap' e.hom h₁ h₂ ≫ leftHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
have rw₂ : Eq.{v_1 + 1} (α := h₁.H ⟶ h₁.H) (𝟙 h₁.H) (𝟙 h₁.H)
Tactic: rw [← leftHomologyMap'_comp, e.hom_inv_id, leftHomologyMap'_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' e.inv h₂ h₁ ≫ leftHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
have rw : leftHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
Tactic: rw [← leftHomologyMap'_comp, e.inv_hom_id, leftHomologyMap'_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
⊢ leftHomologyMap' e.inv h₂ h₁ ≫ leftHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
have rw₁ : leftHomologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.H
Tactic: rw [← leftHomologyMap'_comp, e.inv_hom_id, leftHomologyMap'_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
rw₁ : leftHomologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.H
⊢ leftHomologyMap' e.inv h₂ h₁ ≫ leftHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
have rw₂ : Eq.{v_1 + 1} (α := h₂.H ⟶ h₂.H) (𝟙 h₂.H) (𝟙 h₂.H)
Tactic: rw [← leftHomologyMap'_comp, e.inv_hom_id, leftHomologyMap'_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' e.hom h₁ h₂ ≫ cyclesMap' e.inv h₂ h₁ = 𝟙 h₁.K
have rw : cyclesMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.K
Tactic: rw [← cyclesMap'_comp, e.hom_inv_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : cyclesMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.K
⊢ cyclesMap' e.hom h₁ h₂ ≫ cyclesMap' e.inv h₂ h₁ = 𝟙 h₁.K
have rw₁ : cyclesMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.K
Tactic: rw [← cyclesMap'_comp, e.hom_inv_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : cyclesMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.K
rw₁ : cyclesMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.K
⊢ cyclesMap' e.hom h₁ h₂ ≫ cyclesMap' e.inv h₂ h₁ = 𝟙 h₁.K
have rw₂ : Eq.{v_1 + 1} (α := h₁.K ⟶ h₁.K) (𝟙 h₁.K) (𝟙 h₁.K)
Tactic: rw [← cyclesMap'_comp, e.hom_inv_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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' e.inv h₂ h₁ ≫ cyclesMap' e.hom h₁ h₂ = 𝟙 h₂.K
have rw : cyclesMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.K
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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : cyclesMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.K
⊢ cyclesMap' e.inv h₂ h₁ ≫ cyclesMap' e.hom h₁ h₂ = 𝟙 h₂.K
have rw₁ : cyclesMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.K
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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : cyclesMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.K
rw₁ : cyclesMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.K
⊢ cyclesMap' e.inv h₂ h₁ ≫ cyclesMap' e.hom h₁ h₂ = 𝟙 h₂.K
have rw₂ : Eq.{v_1 + 1} (α := h₂.K ⟶ h₂.K) (𝟙 h₂.K) (𝟙 h₂.K)
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
⊢ CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap e.hom) (leftHomologyMap e.inv) = 𝟙 S₁.leftHomology
have rw : leftHomologyMap (e.hom ≫ e.inv) = 𝟙 S₁.leftHomology
Tactic: rw [← leftHomologyMap_comp, e.hom_inv_id, leftHomologyMap_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 : leftHomologyMap (e.hom ≫ e.inv) = 𝟙 S₁.leftHomology
⊢ CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap e.hom) (leftHomologyMap e.inv) = 𝟙 S₁.leftHomology
have rw₁ : leftHomologyMap (𝟙 S₁) = 𝟙 S₁.leftHomology
Tactic: rw [← leftHomologyMap_comp, e.hom_inv_id, leftHomologyMap_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 : leftHomologyMap (e.hom ≫ e.inv) = 𝟙 S₁.leftHomology
rw₁ : leftHomologyMap (𝟙 S₁) = 𝟙 S₁.leftHomology
⊢ CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap e.hom) (leftHomologyMap e.inv) = 𝟙 S₁.leftHomology
have rw₂ : Eq.{v_1 + 1} (α := S₁.leftHomology ⟶ S₁.leftHomology) (𝟙 S₁.leftHomology) (𝟙 S₁.leftHomology)
Tactic: rw [← leftHomologyMap_comp, e.hom_inv_id, leftHomologyMap_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
⊢ CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap e.inv) (leftHomologyMap e.hom) = 𝟙 S₂.leftHomology
have rw : leftHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.leftHomology
Tactic: rw [← leftHomologyMap_comp, e.inv_hom_id, leftHomologyMap_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 : leftHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.leftHomology
⊢ CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap e.inv) (leftHomologyMap e.hom) = 𝟙 S₂.leftHomology
have rw₁ : leftHomologyMap (𝟙 S₂) = 𝟙 S₂.leftHomology
Tactic: rw [← leftHomologyMap_comp, e.inv_hom_id, leftHomologyMap_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 : leftHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.leftHomology
rw₁ : leftHomologyMap (𝟙 S₂) = 𝟙 S₂.leftHomology
⊢ CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap e.inv) (leftHomologyMap e.hom) = 𝟙 S₂.leftHomology
have rw₂ : Eq.{v_1 + 1} (α := S₂.leftHomology ⟶ S₂.leftHomology) (𝟙 S₂.leftHomology) (𝟙 S₂.leftHomology)
Tactic: rw [← leftHomologyMap_comp, e.inv_hom_id, leftHomologyMap_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
⊢ CategoryStruct.comp (Y := S₂.cycles) (cyclesMap e.hom) (cyclesMap e.inv) = 𝟙 S₁.cycles
have rw : cyclesMap (e.hom ≫ e.inv) = 𝟙 S₁.cycles
Tactic: rw [← cyclesMap_comp, e.hom_inv_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.hom ≫ e.inv) = 𝟙 S₁.cycles
⊢ CategoryStruct.comp (Y := S₂.cycles) (cyclesMap e.hom) (cyclesMap e.inv) = 𝟙 S₁.cycles
have rw₁ : cyclesMap (𝟙 S₁) = 𝟙 S₁.cycles
Tactic: rw [← cyclesMap_comp, e.hom_inv_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.hom ≫ e.inv) = 𝟙 S₁.cycles
rw₁ : cyclesMap (𝟙 S₁) = 𝟙 S₁.cycles
⊢ CategoryStruct.comp (Y := S₂.cycles) (cyclesMap e.hom) (cyclesMap e.inv) = 𝟙 S₁.cycles
have rw₂ : Eq.{v_1 + 1} (α := S₁.cycles ⟶ S₁.cycles) (𝟙 S₁.cycles) (𝟙 S₁.cycles)
Tactic: rw [← cyclesMap_comp, e.hom_inv_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
⊢ CategoryStruct.comp (Y := S₁.cycles) (cyclesMap e.inv) (cyclesMap e.hom) = 𝟙 S₂.cycles
have rw : cyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.cycles
Tactic: rw [← cyclesMap_comp, e.inv_hom_id, cyclesMap_id]