awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₃ rw₄ : γ₁.φH ≫ γ₂.φH = γ₁.φH ≫ γ₂.φH
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.comp, CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₃ rw₄ : γ₁.φK ≫ γ₂.φK = γ₁.φK ≫ γ₂.φK
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.cyclesMap'_eq, γ₂.cyclesMap'_eq, (γ₁.comp γ₂).cyclesMap'_eq,
    LeftHomologyMapData.comp_φK]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.comp, CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
inst_4 : S₃.HasLeftHomology
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
⊢ Eq (α := S₁.leftHomology ⟶ S₃.leftHomology) (leftHomologyMap (φ₁ ≫ φ₂))
    (CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap φ₁) (leftHomologyMap φ₂))

Tactic:
leftHomologyMap'_comp _ _ _ _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
inst_4 : S₃.HasLeftHomology
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
⊢ Eq (α := S₁.cycles ⟶ S₃.cycles) (cyclesMap (φ₁ ≫ φ₂))
    (CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ₁) (cyclesMap φ₂))

Tactic:
cyclesMap'_comp _ _ _ _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := h₁.H ⟶ h₁.H) (𝟙 h₁.H) (𝟙 h₁.H)
⊢ leftHomologyMap' e.hom h₁ h₂ ≫ leftHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H

Tactic:
rw [← leftHomologyMap'_comp, e.hom_inv_id, leftHomologyMap'_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.leftHomologyMap'_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := h₂.H ⟶ h₂.H) (𝟙 h₂.H) (𝟙 h₂.H)
⊢ leftHomologyMap' e.inv h₂ h₁ ≫ leftHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H

Tactic:
rw [← leftHomologyMap'_comp, e.inv_hom_id, leftHomologyMap'_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.leftHomologyMap'_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₂
inst_2 : IsIso φ
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
inferInstanceAs <| IsIso (leftHomologyMapIso' (asIso φ) h₁ h₂).hom

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_leftHomologyMap'_of_isIso._proof_1
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := h₁.K ⟶ h₁.K) (𝟙 h₁.K) (𝟙 h₁.K)
⊢ cyclesMap' e.hom h₁ h₂ ≫ cyclesMap' e.inv h₂ h₁ = 𝟙 h₁.K

Tactic:
rw [← cyclesMap'_comp, e.hom_inv_id, cyclesMap'_id]

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.cyclesMap'_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := h₂.K ⟶ h₂.K) (𝟙 h₂.K) (𝟙 h₂.K)
⊢ cyclesMap' e.inv h₂ h₁ ≫ cyclesMap' e.hom h₁ h₂ = 𝟙 h₂.K

Tactic:
rw [← cyclesMap'_comp, e.inv_hom_id, cyclesMap'_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.cyclesMap'_comp, CategoryTheory.ShortComplex.cyclesMap'_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₂
inst_2 : IsIso φ
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (cyclesMap' φ h₁ h₂)

Tactic:
inferInstanceAs <| IsIso (cyclesMapIso' (asIso φ) h₁ h₂).hom

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso._proof_1
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.leftHomology ⟶ S₁.leftHomology) (𝟙 S₁.leftHomology) (𝟙 S₁.leftHomology)
⊢ CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap e.hom) (leftHomologyMap e.inv) = 𝟙 S₁.leftHomology

Tactic:
rw [← leftHomologyMap_comp, e.hom_inv_id, leftHomologyMap_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.leftHomologyMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₂.leftHomology ⟶ S₂.leftHomology) (𝟙 S₂.leftHomology) (𝟙 S₂.leftHomology)
⊢ CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap e.inv) (leftHomologyMap e.hom) = 𝟙 S₂.leftHomology

Tactic:
rw [← leftHomologyMap_comp, e.inv_hom_id, leftHomologyMap_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap_comp, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.leftHomologyMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₂
inst_2 : IsIso φ
inst_3 : S₁.HasLeftHomology
inst_4 : S₂.HasLeftHomology
⊢ IsIso (X := S₁.leftHomology) (Y := S₂.leftHomology) (leftHomologyMap φ)

Tactic:
inferInstanceAs <| IsIso (leftHomologyMapIso (asIso φ)).hom

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_leftHomologyMap_of_iso._proof_1
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.cycles ⟶ S₁.cycles) (𝟙 S₁.cycles) (𝟙 S₁.cycles)
⊢ CategoryStruct.comp (Y := S₂.cycles) (cyclesMap e.hom) (cyclesMap e.inv) = 𝟙 S₁.cycles

Tactic:
rw [← cyclesMap_comp, e.hom_inv_id, cyclesMap_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.cyclesMap_comp, CategoryTheory.ShortComplex.cyclesMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₂.cycles ⟶ S₂.cycles) (𝟙 S₂.cycles) (𝟙 S₂.cycles)
⊢ CategoryStruct.comp (Y := S₁.cycles) (cyclesMap e.inv) (cyclesMap e.hom) = 𝟙 S₂.cycles

Tactic:
rw [← cyclesMap_comp, e.inv_hom_id, cyclesMap_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.cyclesMap_comp, CategoryTheory.ShortComplex.cyclesMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₂
inst_2 : IsIso φ
inst_3 : S₁.HasLeftHomology
inst_4 : S₂.HasLeftHomology
⊢ IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)

Tactic:
inferInstanceAs <| IsIso (cyclesMapIso (asIso φ)).hom

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_cyclesMap_of_iso._proof_1
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
dsimp : cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i
⊢ Eq (α := S.cycles ⟶ S.X₂) (Iso.hom h.cyclesIso ≫ h.i) S.iCycles

Tactic:
dsimp [iCycles, LeftHomologyData.cyclesIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
⊢ cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i

Tactic:
simp only [cyclesMap'_i, id_τ₂, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.id_τ₂, CategoryTheory.ShortComplex.cyclesMap'_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
⊢ CategoryStruct.comp (Y := S.cycles) (Iso.inv h.cyclesIso) S.iCycles = h.i

Tactic:
simp only [← h.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
dsimp : S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π
⊢ Eq (α := S.cycles ⟶ h.H) (S.leftHomologyπ ≫ Iso.hom h.leftHomologyIso) (Iso.hom h.cyclesIso ≫ h.π)

Tactic:
dsimp only [leftHomologyπ, leftHomologyIso, cyclesIso, leftHomologyMapIso',
    cyclesMapIso', Iso.refl]

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.leftHomologyMapIso', CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, CategoryTheory.ShortComplex.cyclesMapIso'
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw rw₁ :
  S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h =
    S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h
⊢ S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π

Tactic:
rw [← leftHomologyπ_naturality']

Premises used: CategoryTheory.ShortComplex.leftHomologyπ_naturality'
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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 (α := h.K ⟶ S.leftHomology) (h.π ≫ Iso.inv h.leftHomologyIso) (Iso.inv h.cyclesIso ≫ S.leftHomologyπ)

Tactic:
simp only [← cancel_epi h.cyclesIso.hom, ← cancel_mono h.leftHomologyIso.hom, assoc,
    Iso.inv_hom_id, comp_id, Iso.hom_inv_id_assoc,
    LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom, CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
dsimp :
  Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
    (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
    (Iso.hom h₁.leftHomologyIso ≫ γ.φH ≫ Iso.inv h₂.leftHomologyIso)

Tactic:
dsimp [LeftHomologyData.leftHomologyIso, leftHomologyMapIso']

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.leftHomologyMapIso'
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw :
  Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
    (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ)
    (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)

Tactic:
rw [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp,
    ← leftHomologyMap'_comp, id_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.leftHomologyData S₂.leftHomologyData)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
dsimp :
  Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ)
    (cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
⊢ Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ) (Iso.hom h₁.cyclesIso ≫ γ.φK ≫ Iso.inv h₂.cyclesIso)

Tactic:
dsimp [LeftHomologyData.cyclesIso, cyclesMapIso']

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, CategoryTheory.ShortComplex.cyclesMapIso'
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw : Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ) (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)
⊢ Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ)
    (cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData)

Tactic:
rw [← γ.cyclesMap'_eq, ← cyclesMap'_comp, ← cyclesMap'_comp, id_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.leftHomologyData S₂.leftHomologyData)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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 ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap φ) (Iso.hom h₂.leftHomologyIso))
    (Iso.hom h₁.leftHomologyIso ≫ γ.φH)

Tactic:
simp only [γ.leftHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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 ⟶ h₂.K) (CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) (Iso.hom h₂.cyclesIso))
    (Iso.hom h₁.cyclesIso ≫ γ.φK)

Tactic:
simp only [γ.cyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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 ≫ φ.τ₂
⊢ i ≫ S₂.g = 0

Tactic:
simp only [i, assoc, φ.comm₂₃, h.wi_assoc, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.LeftHomologyData.wi_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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 ≫ φ.τ₂
⊢ i ≫ S₂.g = 0

Tactic:
have wi : i ≫ S₂.g = 0 := by simp only [i, assoc, φ.comm₂₃, h.wi_assoc, zero_comp]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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 ≫ φ.τ₃)
rw₇ rw₈ : Eq.{v_1 + 1} (α := W' ⟶ S₂.X₃) 0 0
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0

Tactic:
rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, hx, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.ShortComplex.Hom.τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
⊢ (fun {W' : C} (x : W' ⟶ S₂.X₂) (hx : x ≫ S₂.g = 0) ↦ h.liftK (x ≫ inv φ.τ₂) ⋯) x hx ≫ i = x

Tactic:
simp [i]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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
rw₈ rw₉ : x = x
⊢ b = h.liftK (x ≫ inv φ.τ₂) ⋯

Tactic:
rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, hb]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i_assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.LeftHomologyData.i