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₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
γ' : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    CategoryStruct.comp (Y := S₁.rightHomology)
        (S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData)
        (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
          (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv)

Tactic:
simp only [← γ.rightHomologyMap'_eq, assoc, ← rightHomologyMap'_comp_assoc,
    id_comp, comp_id, γ'.left.leftHomologyMap'_eq, γ'.right.rightHomologyMap'_eq, ← γ'.comm_assoc,
    Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.HomologyMapData.right, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.HomologyMapData.left, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, CategoryTheory.ShortComplex.rightHomologyMap'_comp_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq, 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
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.homology ⟶ h₂.H) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
    (Iso.hom h₁.homologyIso ≫ γ.φH)

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq, CategoryTheory.Iso.inv_hom_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
h : S.HomologyData
⊢ homologyMap' (𝟙 S) h h = 𝟙 h.left.H

Tactic:
(HomologyMapData.id h).homologyMap'_eq

Premises used: CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq, CategoryTheory.ShortComplex.HomologyMapData.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
⊢ homologyMap (𝟙 S) = 𝟙 S.homology

Tactic:
homologyMap'_id _

Premises used: CategoryTheory.ShortComplex.homologyMap'_id, CategoryTheory.ShortComplex.homology, 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
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' 0 h₁ h₂ = 0

Tactic:
(HomologyMapData.zero h₁ h₂).homologyMap'_eq

Premises used: CategoryTheory.ShortComplex.HomologyMapData.zero, CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq
-- 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
⊢ Eq.{v + 1} (α := S₁.homology ⟶ S₂.homology) (homologyMap 0) 0

Tactic:
homologyMap'_zero _ _

Premises used: CategoryTheory.ShortComplex.homologyMap'_zero, CategoryTheory.ShortComplex.homology, 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₂ S₃ : ShortComplex.{v, u} C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h₃ : S₃.HomologyData
⊢ homologyMap' (φ₁ ≫ φ₂) h₁ h₃ = homologyMap' φ₁ h₁ h₂ ≫ homologyMap' φ₂ h₂ h₃

Tactic:
leftHomologyMap'_comp _ _ _ _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, 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₂ S₃ : ShortComplex.{v, u} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
⊢ Eq (α := S₁.homology ⟶ S₃.homology) (homologyMap (φ₁ ≫ φ₂))
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ₁) (homologyMap φ₂))

Tactic:
homologyMap'_comp _ _ _ _ _

Premises used: CategoryTheory.ShortComplex.homologyMap'_comp, CategoryTheory.ShortComplex.homology, 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₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.left.H
rw₁ : homologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.left.H
rw₂ rw₃ : Eq.{v + 1} (α := h₁.left.H ⟶ h₁.left.H) (𝟙 h₁.left.H) (𝟙 h₁.left.H)
⊢ homologyMap' e.hom h₁ h₂ ≫ homologyMap' e.inv h₂ h₁ = 𝟙 h₁.left.H

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

Premises used: CategoryTheory.ShortComplex.homologyMap'_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.homologyMap'_id
-- 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
e : S₁ ≅ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.left.H
rw₁ : homologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.left.H
rw₂ rw₃ : Eq.{v + 1} (α := h₂.left.H ⟶ h₂.left.H) (𝟙 h₂.left.H) (𝟙 h₂.left.H)
⊢ homologyMap' e.inv h₂ h₁ ≫ homologyMap' e.hom h₁ h₂ = 𝟙 h₂.left.H

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

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.homologyMap'_comp, CategoryTheory.ShortComplex.homologyMap'_id
-- 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₂
inst_2 : IsIso φ
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ IsIso (homologyMap' φ h₁ h₂)

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

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_homologyMap'_of_isIso._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
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw : homologyMap (e.hom ≫ e.inv) = 𝟙 S₁.homology
rw₁ : homologyMap (𝟙 S₁) = 𝟙 S₁.homology
rw₂ rw₃ : Eq.{v + 1} (α := S₁.homology ⟶ S₁.homology) (𝟙 S₁.homology) (𝟙 S₁.homology)
⊢ CategoryStruct.comp (Y := S₂.homology) (homologyMap e.hom) (homologyMap e.inv) = 𝟙 S₁.homology

Tactic:
rw [← homologyMap_comp, e.hom_inv_id, homologyMap_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.homologyMap_comp, CategoryTheory.ShortComplex.homologyMap_id
-- 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
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
rw : homologyMap (e.inv ≫ e.hom) = 𝟙 S₂.homology
rw₁ : homologyMap (𝟙 S₂) = 𝟙 S₂.homology
rw₂ rw₃ : Eq.{v + 1} (α := S₂.homology ⟶ S₂.homology) (𝟙 S₂.homology) (𝟙 S₂.homology)
⊢ CategoryStruct.comp (Y := S₁.homology) (homologyMap e.inv) (homologyMap e.hom) = 𝟙 S₂.homology

Tactic:
rw [← homologyMap_comp, e.inv_hom_id, homologyMap_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.homologyMap_comp, CategoryTheory.ShortComplex.homologyMap_id
-- 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 : IsIso φ
inst_3 : S₁.HasHomology
inst_4 : S₂.HasHomology
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)

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

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_homologyMap_of_iso._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
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₁.i ≫ h₂.p = 0

Tactic:
simp
-- 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
rw₄ : Eq (α := h₁.K ⟶ S.X₃) 0 (h₁.π ≫ 0)
rw₅ rw₆ : Eq.{v + 1} (α := h₁.K ⟶ S.X₃) 0 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0

Tactic:
rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
      RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_descH_assoc, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.wi, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : h₁.π ≫ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = h₁.π ≫ 0
rw₁ : (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0
rw₂ : h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
rw₃ : h₁.i ≫ S.g = h₁.π ≫ 0
rw₄ : Eq (α := h₁.K ⟶ S.X₃) 0 (h₁.π ≫ 0)
rw₅ rw₆ : Eq.{v + 1} (α := h₁.K ⟶ S.X₃) 0 0
⊢ h₁.descH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.g' = 0

Tactic:
rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc,
          RightHomologyData.p_g', LeftHomologyData.wi, comp_zero]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_descH_assoc, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.wi, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- 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
⊢ leftRightHomologyComparison' h₁ h₂ = h₂.liftH (h₁.descH (h₁.i ≫ h₂.p) ⋯) ⋯

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.leftRightHomologyComparison', rfl
-- 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
⊢ h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p

Tactic:
simp only [leftRightHomologyComparison'_eq_liftH,
    RightHomologyData.liftH_ι, LeftHomologyData.π_descH]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.liftH_ι, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, CategoryTheory.ShortComplex.LeftHomologyData.π_descH
-- 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ (h₁.i ≫ h₂.p) ≫ h₂.g' = 0

Tactic:
simp
-- 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι
rw₁ : h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.ι = 0 ≫ h₂.ι
rw₂ : h₁.f' ≫ h₁.i ≫ h₂.p = 0 ≫ h₂.ι
rw₃ : S.f ≫ h₂.p = 0 ≫ h₂.ι
rw₄ : Eq (α := S.X₁ ⟶ h₂.Q) 0 (0 ≫ h₂.ι)
rw₅ rw₆ : Eq.{v + 1} (α := S.X₁ ⟶ h₂.Q) 0 0
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0

Tactic:
rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.wp, CategoryTheory.ShortComplex.RightHomologyData.liftH_ι, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.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.LeftHomologyData
h₂ : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.descH (h₂.liftH (h₁.i ≫ h₂.p) ⋯) ⋯

Tactic:
simp only [← cancel_mono h₂.ι, ← cancel_epi h₁.π, π_leftRightHomologyComparison'_ι,
    LeftHomologyData.π_descH_assoc, RightHomologyData.liftH_ι]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_descH_assoc, CategoryTheory.ShortComplex.RightHomologyData.liftH_ι, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.cancel_epi
-- 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
⊢ Eq (α := S.cycles ⟶ S.opcycles) (S.leftHomologyπ ≫ S.leftRightHomologyComparison ≫ S.rightHomologyι)
    (S.iCycles ≫ S.pOpcycles)

Tactic:
π_leftRightHomologyComparison'_ι _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.rightHomologyι, CategoryTheory.ShortComplex.leftRightHomologyComparison, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles
-- 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₂
h₁ : S₁.LeftHomologyData
h₂ : S₁.RightHomologyData
h₁' : S₂.LeftHomologyData
h₂' : S₂.RightHomologyData
⊢ leftHomologyMap' φ h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' φ h₂ h₂'

Tactic:
simp only [← cancel_epi h₁.π, ← cancel_mono h₂'.ι, assoc,
    leftHomologyπ_naturality'_assoc, rightHomologyι_naturality',
    π_leftRightHomologyComparison'_ι, π_leftRightHomologyComparison'_ι_assoc,
    cyclesMap'_i_assoc, p_opcyclesMap']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.ShortComplex.p_opcyclesMap', CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc, CategoryTheory.ShortComplex.rightHomologyι_naturality', CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, CategoryTheory.ShortComplex.cyclesMap'_i_assoc, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.cancel_epi
-- 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₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
rw :
  leftRightHomologyComparison' h₁ h₂ =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
rw₁ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S ≫ 𝟙 S) h₂ h₂
rw₂ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂
rw₃ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ 𝟙 h₂.H
rw₄ rw₅ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂

Tactic:
rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, comp_id]

Premises used: CategoryTheory.ShortComplex.rightHomologyMap'_id, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality_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
inst_2 : S.HasLeftHomology
inst_3 : S.HasRightHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ Eq (α := S.leftHomology ⟶ S.rightHomology) S.leftRightHomologyComparison
    (Iso.hom h₁.leftHomologyIso ≫ leftRightHomologyComparison' h₁ h₂ ≫ Iso.inv h₂.rightHomologyIso)

Tactic:
leftRightHomologyComparison'_compatibility _ _ _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.RightHomologyData.liftH, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.rightHomologyMap', CategoryTheory.ShortComplex.leftRightHomologyComparison, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility
-- 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
⊢ leftRightHomologyComparison' h.left h.right = h.iso.hom

Tactic:
simp only [← cancel_epi h.left.π, ← cancel_mono h.right.ι, assoc,
    π_leftRightHomologyComparison'_ι, comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.HomologyData.right
-- 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
h : S.HomologyData
rw : IsIso h.iso.hom
⊢ IsIso (Y := h.right.H) (leftRightHomologyComparison' h.left h.right)

Tactic:
rw [h.leftRightHomologyComparison'_eq]

Premises used: 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 S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : S.HomologyData
⊢ IsIso h.iso.hom

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
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
inst_2 : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw :
  IsIso
    (leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      CategoryStruct.comp (Y := S.homologyData.right.H)
        (leftRightHomologyComparison' S.homologyData.left S.homologyData.right)
        (rightHomologyMap' (𝟙 S) S.homologyData.right h₂))
⊢ IsIso (leftRightHomologyComparison' h₁ h₂)

Tactic:
rw [leftRightHomologyComparison'_compatibility h₁ S.homologyData.left h₂
    S.homologyData.right]

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility, CategoryTheory.ShortComplex.HomologyData.right, 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
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
inst_2 : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ IsIso
    (leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      CategoryStruct.comp (Y := S.homologyData.right.H)
        (leftRightHomologyComparison' S.homologyData.left S.homologyData.right)
        (rightHomologyMap' (𝟙 S) S.homologyData.right h₂))

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
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
inst_2 : S.HasHomology
⊢ IsIso (Y := S.rightHomology) (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)

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
h : S.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ = leftHomologyMap' (𝟙 S) h₁ h.left ≫ h.iso.hom ≫ rightHomologyMap' (𝟙 S) h.right h₂

Tactic:
simpa only [h.leftRightHomologyComparison'_eq] using
    leftRightHomologyComparison'_compatibility h₁ h.left h₂ h.right

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility, CategoryTheory.ShortComplex.HomologyData.right, 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.LeftHomologyData
h₂ : S.RightHomologyData
inst_2 : S.HasHomology
rw :
  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)
⊢ leftRightHomologyComparison' h₁ h₂ =
    CategoryStruct.comp (Y := S.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₂.homologyIso)

Tactic:
rw [leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
    S.homologyData h₁ h₂]

Premises used: CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', CategoryTheory.ShortComplex.homologyData