awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst_2 : S.HasHomology
dsimp :
  leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData)
        (leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫
      CategoryStruct.comp (Y := S.rightHomology)
        (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData)
        (rightHomologyMap' (𝟙 S) S.rightHomologyData h₂)
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    CategoryStruct.comp (Y := S.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₂.homologyIso)

Tactic:
dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyMapIso', leftHomologyIso,
    RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', rightHomologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.ShortComplex.leftHomologyMapIso', CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.leftHomologyIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst_2 : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData)
        (leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫
      CategoryStruct.comp (Y := S.rightHomology)
        (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData)
        (rightHomologyMap' (𝟙 S) S.rightHomologyData h₂)

Tactic:
simp only [assoc, ← leftHomologyMap'_comp_assoc, id_comp, ← rightHomologyMap'_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.leftHomologyMap'_comp_assoc, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.leftHomology ⟶ S.rightHomology) (S.leftRightHomologyComparison : S.leftHomology ⟶ S.rightHomology)
    (CategoryStruct.comp (Y := S.homology) (Iso.hom S.leftHomologyIso) (Iso.inv S.rightHomologyIso) :
      S.leftHomology ⟶ S.rightHomology)

Tactic:
simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv,
    RightHomologyData.homologyIso_rightHomologyData, Iso.symm_hom] using
      leftRightHomologyComparison'_fac S.leftHomologyData S.rightHomologyData

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac, CategoryTheory.Iso.symm_hom, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.Iso.symm_inv, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData, CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h : S.HomologyData
inst_2 : S.HasHomology
this : h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso
rw :
  Eq (α := S.homology ≅ h.right.H) h.right.homologyIso
    (h.left.homologyIso ≪≫ Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso)
rw₁ rw₂ : Eq (α := S.homology ≅ h.right.H) h.right.homologyIso h.right.homologyIso
⊢ Eq (α := S.homology ≅ h.right.H) h.right.homologyIso (h.left.homologyIso ≪≫ h.iso)

Tactic:
rw [this, Iso.self_symm_id_assoc]

Premises used: CategoryTheory.Iso.self_symm_id_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h : S.HomologyData
inst_2 : S.HasHomology
suffices : h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso
⊢ Eq (α := S.homology ≅ h.right.H) h.right.homologyIso (h.left.homologyIso ≪≫ h.iso)

Tactic:
suffices h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso by
    rw [this, Iso.self_symm_id_assoc]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h : S.HomologyData
inst_2 : S.HasHomology
w : h.iso.hom = (Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso).hom
⊢ h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h : S.HomologyData
inst_2 : S.HasHomology
w : h.iso.hom = CategoryStruct.comp (Y := S.homology) (Iso.inv h.left.homologyIso) (Iso.hom h.right.homologyIso)
⊢ h.iso.hom = (Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso).hom

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h : S.HomologyData
inst_2 : S.HasHomology
w : h.iso.hom = leftRightHomologyComparison' h.left h.right
w₁ w₂ : h.iso.hom = h.iso.hom
⊢ h.iso.hom = CategoryStruct.comp (Y := S.homology) (Iso.inv h.left.homologyIso) (Iso.hom h.right.homologyIso)

Tactic:
rw [← leftRightHomologyComparison'_fac, leftRightHomologyComparison'_eq]

Premises used: CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac, CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h : S.HomologyData
inst_2 : S.HasHomology
rw : Eq (α := S.homology ≅ h.left.H) h.left.homologyIso ((h.left.homologyIso ≪≫ h.iso) ≪≫ h.iso.symm)
⊢ Eq (α := S.homology ≅ h.left.H) h.left.homologyIso (h.right.homologyIso ≪≫ h.iso.symm)

Tactic:
rw [right_homologyIso_eq_left_homologyIso_trans_iso]

Premises used: CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst_2 : IsIso (leftRightHomologyComparison' h₁ h₂)
⊢ S.HasHomology

Tactic:
HasHomology.mk' (HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂)

Premises used: CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison', CategoryTheory.ShortComplex.HasHomology.mk'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasLeftHomology
inst_3 : S.HasRightHomology
h : IsIso (X := S.leftHomology) (Y := S.rightHomology) S.leftRightHomologyComparison
⊢ IsIso (Y := S.rightHomologyData.H) (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)

Tactic:
haveI : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData) := h
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasLeftHomology
inst_3 : S.HasRightHomology
h : IsIso (X := S.leftHomology) (Y := S.rightHomology) S.leftRightHomologyComparison
this : IsIso (Y := S.rightHomologyData.H) (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)
⊢ S.HasHomology

Tactic:
hasHomology_of_isIso_leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.hasHomology_of_isIso_leftRightHomologyComparison'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasLeftHomology
inst_3 : S.HasRightHomology
h : IsIso (X := S.leftHomology) (Y := S.rightHomology) S.leftRightHomologyComparison
this : IsIso (Y := S.rightHomologyData.H) (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)
⊢ S.HasHomology

Tactic:
exact hasHomology_of_isIso_leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.hasHomology_of_isIso_leftRightHomologyComparison'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
dsimp :
  Eq (α := S₁.homology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData)
        (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
      leftHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)
      (CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) S₂.homologyData.left S₂.leftHomologyData)
        (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData h₂)))
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ leftHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))

Tactic:
dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.leftHomologyIso, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ Eq (α := S₁.homology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData)
        (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
      leftHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)
      (CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) S₂.homologyData.left S₂.leftHomologyData)
        (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData h₂)))

Tactic:
simp only [← leftHomologyMap'_comp, id_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
dsimp :
  Eq (α := h₁.H ⟶ S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology)
      (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData)
        (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left))
      (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left))
    (leftHomologyMap' φ h₁ h₂ ≫
      CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
        (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left))
⊢ Eq (α := h₁.H ⟶ S₂.homology) (CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (homologyMap φ))
    (leftHomologyMap' φ h₁ h₂ ≫ Iso.inv h₂.homologyIso)

Tactic:
dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.leftHomologyIso, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ Eq (α := h₁.H ⟶ S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology)
      (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData)
        (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left))
      (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left))
    (leftHomologyMap' φ h₁ h₂ ≫
      CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
        (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left))

Tactic:
simp only [← leftHomologyMap'_comp, id_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.leftHomology ⟶ S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) (Iso.hom S₁.leftHomologyIso) (homologyMap φ) :
      S₁.leftHomology ⟶ S₂.homology)
    (leftHomologyMap φ ≫ Iso.hom S₂.leftHomologyIso : S₁.leftHomology ⟶ S₂.homology)

Tactic:
simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv] using
    LeftHomologyData.leftHomologyIso_inv_naturality φ S₁.leftHomologyData S₂.leftHomologyData

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.Iso.symm_inv, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_inv_naturality
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.homology ⟶ S₂.leftHomology)
    (Iso.inv S₁.leftHomologyIso ≫ leftHomologyMap φ : S₁.homology ⟶ S₂.leftHomology)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.inv S₂.leftHomologyIso) :
      S₁.homology ⟶ S₂.leftHomology)

Tactic:
simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv] using
    LeftHomologyData.leftHomologyIso_hom_naturality φ S₁.leftHomologyData S₂.leftHomologyData

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.Iso.symm_inv, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_naturality, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_leftHomologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ Eq (α := h₁.H ⟶ S₂.homology) (CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (homologyMap φ))
    (rightHomologyMap' φ h₁ h₂ ≫ Iso.inv h₂.homologyIso)

Tactic:
simp only [← cancel_mono h₂.homologyIso.hom, assoc, Iso.inv_hom_id_assoc, comp_id,
    ← RightHomologyData.rightHomologyIso_hom_naturality φ h₁ h₂, Iso.inv_hom_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.rightHomology ⟶ S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) (Iso.hom S₁.rightHomologyIso) (homologyMap φ) :
      S₁.rightHomology ⟶ S₂.homology)
    (rightHomologyMap φ ≫ Iso.hom S₂.rightHomologyIso : S₁.rightHomology ⟶ S₂.homology)

Tactic:
simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using
    RightHomologyData.rightHomologyIso_inv_naturality φ S₁.rightHomologyData S₂.rightHomologyData

Premises used: CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_naturality, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.Iso.symm_inv, CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.homology ⟶ S₂.rightHomology)
    (Iso.inv S₁.rightHomologyIso ≫ rightHomologyMap φ : S₁.homology ⟶ S₂.rightHomology)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.inv S₂.rightHomologyIso) :
      S₁.homology ⟶ S₂.rightHomology)

Tactic:
simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using
    RightHomologyData.rightHomologyIso_hom_naturality φ S₁.rightHomologyData S₂.rightHomologyData

Premises used: CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.Iso.symm_inv, CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
inst_2 : CategoryWithHomology.{v, u} C
⊢ CategoryWithHomology.{v, u} Cᵒᵖ

Tactic:
⟨fun S => HasHomology.mk' S.unop.homologyData.op⟩

Premises used: CategoryTheory.ShortComplex.HomologyData.op, CategoryTheory.CategoryWithHomology.mk, CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.unop, CategoryTheory.ShortComplex.homologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ_1 : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ IsIso (X := h₁.left.H) (Y := h₂.left.H) (leftHomologyMap' φ h₁.left h₂.left)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : Epi φ.τ₁
h₂ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap' φ S₁.homologyData S₂.homologyData)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ_1 : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

Tactic:
isIso_homologyMap_of_epi_of_isIso_of_mono' φ inferInstance inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ_1 : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
φ : S₁ ⟶ S₂
inst_2 : CategoryWithHomology.{v, u} C
inst_3 : Epi φ.τ₁
inst_4 : IsIso φ.τ₂
inst_5 : Mono φ.τ₃
⊢ IsIso (X := Functor.obj (homologyFunctor C) S₁) (Functor.map (homologyFunctor C) φ)

Tactic:
inferInstanceAs <| IsIso (homologyMap φ)

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_homologyFunctor_map_of_epi_of_isIso_of_mono._proof_1
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ_1 : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : IsIso φ
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
dsimp :
  Eq (α := S.cycles ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) (Iso.inv S.leftHomologyIso) :
      S.cycles ⟶ S.leftHomology)
    (S.leftHomologyπ : S.cycles ⟶ S.leftHomology)
⊢ Eq (α := S.cycles ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.homology) S.homologyπ (Iso.inv S.leftHomologyIso) : S.cycles ⟶ S.leftHomology)
    (S.leftHomologyπ : S.cycles ⟶ S.leftHomology)

Tactic:
dsimp only [homologyπ]

Premises used: CategoryTheory.ShortComplex.homologyπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) (Iso.inv S.leftHomologyIso) :
      S.cycles ⟶ S.leftHomology)
    (S.leftHomologyπ : S.cycles ⟶ S.leftHomology)

Tactic:
simp only [assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
dsimp :
  Eq (α := S.rightHomology ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.hom S.rightHomologyIso)
        (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
      S.rightHomology ⟶ S.opcycles)
    (S.rightHomologyι : S.rightHomology ⟶ S.opcycles)
⊢ Eq (α := S.rightHomology ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.hom S.rightHomologyIso) S.homologyι : S.rightHomology ⟶ S.opcycles)
    (S.rightHomologyι : S.rightHomology ⟶ S.opcycles)

Tactic:
dsimp only [homologyι]

Premises used: CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
inst_2 : S.HasHomology
⊢ Eq (α := S.rightHomology ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.hom S.rightHomologyIso)
        (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
      S.rightHomology ⟶ S.opcycles)
    (S.rightHomologyι : S.rightHomology ⟶ S.opcycles)

Tactic:
simp only [Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc