awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.rightHomology ⟶ S₂.opcycles) (rightHomologyMap φ ≫ S₂.rightHomologyι) (S₁.rightHomologyι ≫ opcyclesMap φ)

Tactic:
rightHomologyι_naturality' _ _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.rightHomologyι_naturality', CategoryTheory.ShortComplex.rightHomologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' φ h₁ h₂ = γ.φH

Tactic:
RightHomologyMapData.congr_φH (Subsingleton.elim _ _)

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.congr_φH, CategoryTheory.ShortComplex.rightHomologyMap', Subsingleton.elim
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' φ h₁ h₂ = γ.φQ

Tactic:
RightHomologyMapData.congr_φQ (Subsingleton.elim _ _)

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ, CategoryTheory.ShortComplex.opcyclesMap', Subsingleton.elim
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
⊢ rightHomologyMap' (𝟙 S) h h = 𝟙 h.H

Tactic:
(RightHomologyMapData.id h).rightHomologyMap'_eq

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.id, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
⊢ opcyclesMap' (𝟙 S) h h = 𝟙 h.Q

Tactic:
(RightHomologyMapData.id h).opcyclesMap'_eq

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
⊢ rightHomologyMap (𝟙 S) = 𝟙 S.rightHomology

Tactic:
rightHomologyMap'_id _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap'_id, CategoryTheory.ShortComplex.rightHomologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.HasRightHomology
⊢ opcyclesMap (𝟙 S) = 𝟙 S.opcycles

Tactic:
opcyclesMap'_id _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap'_id, CategoryTheory.ShortComplex.opcyclesMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' 0 h₁ h₂ = 0

Tactic:
(RightHomologyMapData.zero h₁ h₂).rightHomologyMap'_eq

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' 0 h₁ h₂ = 0

Tactic:
(RightHomologyMapData.zero h₁ h₂).opcyclesMap'_eq

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq.{v_1 + 1} (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap 0) 0

Tactic:
rightHomologyMap'_zero _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap'_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq.{v_1 + 1} (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap 0) 0

Tactic:
opcyclesMap'_zero _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesMap'_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ rightHomologyMap' φ₂ h₂ h₃
rw₁ : rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH
rw₂ : (γ₁.comp γ₂).φH = γ₁.φH ≫ γ₂.φH
rw₃ rw₄ : γ₁.φH ≫ γ₂.φH = γ₁.φH ≫ γ₂.φH
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

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

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.comp, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.comp_φH
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
rw : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ opcyclesMap' φ₂ h₂ h₃
rw₁ : opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φQ ≫ γ₂.φQ
rw₂ : (γ₁.comp γ₂).φQ = γ₁.φQ ≫ γ₂.φQ
rw₃ rw₄ : γ₁.φQ ≫ γ₂.φQ = γ₁.φQ ≫ γ₂.φQ
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
    RightHomologyMapData.comp_φQ]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.comp, CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.HasRightHomology
inst_3 : S₂.HasRightHomology
inst_4 : S₃.HasRightHomology
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
⊢ Eq (α := S₁.rightHomology ⟶ S₃.rightHomology) (rightHomologyMap (φ₁ ≫ φ₂))
    (CategoryStruct.comp (Y := S₂.rightHomology) (rightHomologyMap φ₁) (rightHomologyMap φ₂))

Tactic:
rightHomologyMap'_comp _ _ _ _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap'_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.HasRightHomology
inst_3 : S₂.HasRightHomology
inst_4 : S₃.HasRightHomology
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
⊢ Eq (α := S₁.opcycles ⟶ S₃.opcycles) (opcyclesMap (φ₁ ≫ φ₂))
    (CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ₁) (opcyclesMap φ₂))

Tactic:
opcyclesMap'_comp _ _ _ _ _

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
rw [← rightHomologyMap_comp, e.hom_inv_id, rightHomologyMap_id]

Premises used: CategoryTheory.ShortComplex.rightHomologyMap_id, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.rightHomologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : rightHomologyMap (e.inv ≫ e.hom) = 𝟙 S₂.rightHomology
rw₁ : rightHomologyMap (𝟙 S₂) = 𝟙 S₂.rightHomology
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₂.rightHomology ⟶ S₂.rightHomology) (𝟙 S₂.rightHomology) (𝟙 S₂.rightHomology)
⊢ CategoryStruct.comp (Y := S₁.rightHomology) (rightHomologyMap e.inv) (rightHomologyMap e.hom) = 𝟙 S₂.rightHomology

Tactic:
rw [← rightHomologyMap_comp, e.inv_hom_id, rightHomologyMap_id]

Premises used: CategoryTheory.ShortComplex.rightHomologyMap_id, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.rightHomologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.HasRightHomology
inst_4 : S₂.HasRightHomology
⊢ IsIso (X := S₁.rightHomology) (Y := S₂.rightHomology) (rightHomologyMap φ)

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

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

Tactic:
rw [← opcyclesMap_comp, e.hom_inv_id, opcyclesMap_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.opcyclesMap_comp, CategoryTheory.ShortComplex.opcyclesMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw : opcyclesMap (e.inv ≫ e.hom) = 𝟙 S₂.opcycles
rw₁ : opcyclesMap (𝟙 S₂) = 𝟙 S₂.opcycles
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₂.opcycles ⟶ S₂.opcycles) (𝟙 S₂.opcycles) (𝟙 S₂.opcycles)
⊢ CategoryStruct.comp (Y := S₁.opcycles) (opcyclesMap e.inv) (opcyclesMap e.hom) = 𝟙 S₂.opcycles

Tactic:
rw [← opcyclesMap_comp, e.inv_hom_id, opcyclesMap_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.opcyclesMap_comp, CategoryTheory.ShortComplex.opcyclesMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.HasRightHomology
inst_4 : S₂.HasRightHomology
⊢ IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)

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

Premises used: _private.0.CategoryTheory.ShortComplex.isIso_opcyclesMap_of_iso._proof_1
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
inst_2 : S.HasRightHomology
dsimp : h.p ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData = S.rightHomologyData.p
⊢ Eq (α := S.X₂ ⟶ S.opcycles) (h.p ≫ Iso.inv h.opcyclesIso) S.pOpcycles

Tactic:
dsimp [pOpcycles, RightHomologyData.opcyclesIso]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso, CategoryTheory.ShortComplex.pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
inst_2 : S.HasRightHomology
⊢ h.p ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData = S.rightHomologyData.p

Tactic:
simp only [p_opcyclesMap', id_τ₂, id_comp]

Premises used: CategoryTheory.ShortComplex.p_opcyclesMap', CategoryTheory.ShortComplex.id_τ₂, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
inst_2 : S.HasRightHomology
⊢ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (Iso.hom h.opcyclesIso) = h.p

Tactic:
simp only [← h.p_comp_opcyclesIso_inv, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
inst_2 : S.HasRightHomology
dsimp :
  rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData
⊢ Eq (α := h.H ⟶ S.opcycles) (Iso.inv h.rightHomologyIso ≫ S.rightHomologyι) (h.ι ≫ Iso.inv h.opcyclesIso)

Tactic:
dsimp only [rightHomologyι, rightHomologyIso, opcyclesIso, rightHomologyMapIso',
    opcyclesMapIso', Iso.refl]

Premises used: CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.opcyclesMapIso', CategoryTheory.ShortComplex.rightHomologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
inst_2 : S.HasRightHomology
rw rw₁ :
  Eq (α := h.H ⟶ S.opcycles) (h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData)
    (h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData)
⊢ rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData

Tactic:
rw [rightHomologyι_naturality']

Premises used: CategoryTheory.ShortComplex.rightHomologyι_naturality'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.RightHomologyData
inst_2 : S.HasRightHomology
⊢ Eq (α := S.rightHomology ⟶ h.Q) (Iso.hom h.rightHomologyIso ≫ h.ι) (S.rightHomologyι ≫ Iso.hom h.opcyclesIso)

Tactic:
simp only [← cancel_mono h.opcyclesIso.inv, ← cancel_epi h.rightHomologyIso.inv,
    assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id, comp_id, rightHomologyIso_inv_comp_rightHomologyι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
dsimp :
  Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (Iso.hom h₁.rightHomologyIso ≫ γ.φH ≫ Iso.inv h₂.rightHomologyIso)

Tactic:
dsimp [RightHomologyData.rightHomologyIso, rightHomologyMapIso']

Premises used: CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
rw :
  Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData)

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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ)
    (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
dsimp :
  Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ)
    (opcyclesMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ S₂.rightHomologyData)
⊢ Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (Iso.hom h₁.opcyclesIso ≫ γ.φQ ≫ Iso.inv h₂.opcyclesIso)

Tactic:
dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']

Premises used: CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso, CategoryTheory.ShortComplex.cyclesMapIso'