awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := (K.sc' i j k).opcycles ⟶ K.X k)
    (CategoryStruct.comp (Y := K.opcycles j) (Iso.inv (K.opcyclesIsoSc' i j k hi hk)) (K.fromOpcycles j k) :
      (K.sc' i j k).opcycles ⟶ K.X k)
    ((K.sc' i j k).fromOpcycles : (K.sc' i j k).opcycles ⟶ (K.sc' i j k).X₃)

Tactic:
simp only [← cancel_epi (K.sc' i j k).pOpcycles, pOpcycles_opcyclesIsoSc'_inv_assoc,
    p_fromOpcycles, ShortComplex.p_fromOpcycles, shortComplexFunctor'_obj_g]

Premises used: HomologicalComplex.p_fromOpcycles, HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv_assoc, CategoryTheory.ShortComplex.p_fromOpcycles, CategoryTheory.ShortComplex.pOpcycles, HomologicalComplex.shortComplexFunctor'_obj_g, HomologicalComplex.sc', CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
inst_2 : K.HasHomology j
inst_3 : (K.sc' (c.prev j) j (c.next j)).HasHomology
⊢ (K.sc' (c.prev j) j (c.next j)).homology = K.homology j

Tactic:
rfl

Premises used: HomologicalComplex.homology, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
inst_2 : K.HasHomology j
inst_3 : (K.sc' (c.prev j) j (c.next j)).HasHomology
w : Iso.hom (K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯) = Iso.hom (Iso.refl (K.homology j))
⊢ K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯ = Iso.refl (K.homology j)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
inst_2 : K.HasHomology j
inst_3 : (K.sc' (c.prev j) j (c.next j)).HasHomology
⊢ Iso.hom (K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯) = Iso.hom (Iso.refl (K.homology j))

Tactic:
apply ShortComplex.homologyMap_id

Premises used: CategoryTheory.ShortComplex.homologyMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.cycles j ⟶ (K.sc' i j k).homology) (K.homologyπ j ≫ Iso.hom (K.homologyIsoSc' i j k hi hk))
    (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
      (Iso.hom (K.cyclesIsoSc' i j k hi hk) : K.cycles j ⟶ (K.sc' i j k).cycles)
      ((K.sc' i j k).homologyπ : (K.sc' i j k).cycles ⟶ (K.sc' i j k).homology))

Tactic:
apply ShortComplex.homologyπ_naturality

Premises used: CategoryTheory.ShortComplex.homologyπ_naturality
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := (K.sc' i j k).cycles ⟶ K.homology j)
    (CategoryStruct.comp (Y := (K.sc' i j k).homology) (K.sc' i j k).homologyπ
        (Iso.inv (K.homologyIsoSc' i j k hi hk)) :
      (K.sc' i j k).cycles ⟶ K.homology j)
    (Iso.inv (K.cyclesIsoSc' i j k hi hk) ≫ K.homologyπ j : (K.sc' i j k).cycles ⟶ K.homology j)

Tactic:
apply ShortComplex.homologyπ_naturality

Premises used: CategoryTheory.ShortComplex.homologyπ_naturality
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.homology j ⟶ (K.sc' i j k).opcycles)
    (CategoryStruct.comp (Y := (K.sc' i j k).homology) (Iso.hom (K.homologyIsoSc' i j k hi hk))
        (K.sc' i j k).homologyι :
      K.homology j ⟶ (K.sc' i j k).opcycles)
    (K.homologyι j ≫ Iso.hom (K.opcyclesIsoSc' i j k hi hk) : K.homology j ⟶ (K.sc' i j k).opcycles)

Tactic:
apply ShortComplex.homologyι_naturality

Premises used: CategoryTheory.ShortComplex.homologyι_naturality
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := (K.sc' i j k).homology ⟶ K.opcycles j) (Iso.inv (K.homologyIsoSc' i j k hi hk) ≫ K.homologyι j)
    ((K.sc' i j k).homologyι ≫ Iso.inv (K.opcyclesIsoSc' i j k hi hk))

Tactic:
apply ShortComplex.homologyι_naturality

Premises used: CategoryTheory.ShortComplex.homologyι_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
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : HomologyMapData φ h₁ h₂
⊢ h.left.φH ≫ h₂.iso.hom = h₁.iso.hom ≫ h.right.φH

Tactic:
simp only [← cancel_epi h₁.left.π, ← cancel_mono h₂.right.ι, assoc,
    LeftHomologyMapData.commπ_assoc, HomologyData.comm, LeftHomologyMapData.commi_assoc,
    RightHomologyMapData.commι, HomologyData.comm_assoc, RightHomologyMapData.commp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyMapData.commi_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.commι, CategoryTheory.ShortComplex.LeftHomologyData.π, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ_assoc, CategoryTheory.ShortComplex.HomologyData.right, CategoryTheory.ShortComplex.RightHomologyMapData.commp
-- 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
left₁ : LeftHomologyMapData φ h₁.left h₂.left
right₁ : RightHomologyMapData φ h₁.right h₂.right
left₂ : LeftHomologyMapData φ h₁.left h₂.left
right₂ : RightHomologyMapData φ h₁.right h₂.right
⊢ { left := left₁, right := right₁ : HomologyMapData φ h₁ h₂ } = { left := left₂, right := right₂ }

Tactic:
simp only [mk.injEq, eq_iff_true_of_subsingleton, and_self]

Premises used: and_self, CategoryTheory.ShortComplex.HomologyMapData.mk.injEq, eq_iff_true_of_subsingleton
-- 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₁.HomologyData
h₂ : S₂.HomologyData
γ₁ γ₂ : HomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
rw rw₁ : γ₂.left.φH = γ₂.left.φH
⊢ γ₁.left.φH = γ₂.left.φH

Tactic:
rw [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
⊢ (h.right.op.π ≫ h.iso.op.hom ≫ h.left.op.ι).unop = (h.right.op.i ≫ h.left.op.p).unop

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Homology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S_1 S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
S : ShortComplex.{v, u} Cᵒᵖ
h : S.HomologyData
⊢ (h.right.unop.π ≫ h.iso.unop.hom ≫ h.left.unop.ι).op = (h.right.unop.i ≫ h.left.unop.p).op

Tactic:
simp
-- 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
⊢ S.HasHomology

Tactic:
⟨Nonempty.intro h⟩

Premises used: Nonempty.intro, 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 S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
inst_2 : S.HasHomology
⊢ S.op.HasHomology

Tactic:
HasHomology.mk' S.homologyData.op

Premises used: CategoryTheory.ShortComplex.HomologyData.op, CategoryTheory.ShortComplex.HasHomology.mk', 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_1 S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
S : ShortComplex.{v, u} Cᵒᵖ
inst_2 : S.HasHomology
⊢ S.unop.HasHomology

Tactic:
HasHomology.mk' S.homologyData.unop

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.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
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
inst_2 : S.HasHomology
⊢ S.HasLeftHomology

Tactic:
HasLeftHomology.mk' S.homologyData.left

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.homologyData, CategoryTheory.ShortComplex.HasLeftHomology.mk'
-- 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
⊢ S.HasRightHomology

Tactic:
HasRightHomology.mk' S.homologyData.right

Premises used: CategoryTheory.ShortComplex.HasRightHomology.mk', 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₁ : S₁.HomologyData
h₂ : S₂.HomologyData
X Y : C
f : X ⟶ Y
Z : C
inst_2 : HasCokernel f
⊢ HasHomology (mk (X₃ := Z) f 0 ⋯)

Tactic:
HasHomology.mk' (HomologyData.ofHasCokernel _ rfl)

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.ofHasCokernel, rfl
-- 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
Y Z : C
g : Y ⟶ Z
X : C
inst_2 : HasKernel g
⊢ HasHomology (mk (X₁ := X) 0 g ⋯)

Tactic:
HasHomology.mk' (HomologyData.ofHasKernel _ rfl)

Premises used: CategoryTheory.ShortComplex.HomologyData.ofHasKernel, CategoryTheory.ShortComplex.HasHomology.mk', rfl
-- 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
X Y Z : C
⊢ HasHomology.{v, u} (C := C) (mk (X₁ := X) (X₂ := Y) (X₃ := Z) 0 0 ⋯)

Tactic:
HasHomology.mk' (HomologyData.ofZeros _ rfl rfl)

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.ofZeros, rfl
-- 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 : Epi φ.τ₁
inst_4 : IsIso φ.τ₂
inst_5 : Mono φ.τ₃
⊢ S₂.HasHomology

Tactic:
HasHomology.mk' (HomologyData.ofEpiOfIsIsoOfMono φ S₁.homologyData)

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono, 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₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₂.HasHomology
inst_3 : Epi φ.τ₁
inst_4 : IsIso φ.τ₂
inst_5 : Mono φ.τ₃
⊢ S₁.HasHomology

Tactic:
HasHomology.mk' (HomologyData.ofEpiOfIsIsoOfMono' φ S₂.homologyData)

Premises used: CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono', CategoryTheory.ShortComplex.HasHomology.mk', 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₂ : ShortComplex.{v, u} C
e : S₁ ≅ S₂
inst_2 : S₁.HasHomology
⊢ S₂.HasHomology

Tactic:
HasHomology.mk' (HomologyData.ofIso e S₁.homologyData)

Premises used: CategoryTheory.ShortComplex.HomologyData.ofIso, CategoryTheory.ShortComplex.HasHomology.mk', 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 : ShortComplex.{v, u} C
inst_2 : S.HasHomology
w :
  Eq (α := S.homology ⟶ S.leftHomologyData.H) (Iso.hom S.leftHomologyData.homologyIso)
    (Iso.hom (Iso.symm S.leftHomologyIso))
⊢ Eq (α := S.homology ≅ S.leftHomologyData.H) S.leftHomologyData.homologyIso (Iso.symm S.leftHomologyIso)

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
inst_2 : S.HasHomology
w :
  Eq (α := S.homology ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
      (leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData))
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
⊢ Eq (α := S.homology ⟶ S.leftHomologyData.H) (Iso.hom S.leftHomologyData.homologyIso)
    (Iso.hom (Iso.symm S.leftHomologyIso))

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

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, 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
inst_2 : S.HasHomology
w :
  Eq (α := S.homology ⟶ S.leftHomology) (leftHomologyMap' (𝟙 S ≫ 𝟙 S) S.homologyData.left S.leftHomologyData)
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
w₁ w₂ :
  Eq (α := S.homology ⟶ S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
⊢ Eq (α := S.homology ⟶ S.leftHomology)
    (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)
      (leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData))
    (leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData)

Tactic:
rw [← leftHomologyMap'_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, 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
w :
  Eq (α := S.homology ⟶ S.rightHomologyData.H) (Iso.hom S.rightHomologyData.homologyIso)
    (Iso.hom (Iso.symm S.rightHomologyIso))
⊢ Eq (α := S.homology ≅ S.rightHomologyData.H) S.rightHomologyData.homologyIso (Iso.symm S.rightHomologyIso)

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
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ⟶ S.rightHomologyData.H) (Iso.hom S.rightHomologyData.homologyIso)
    (Iso.hom (Iso.symm S.rightHomologyIso))

Tactic:
simp [homologyIso, rightHomologyIso]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.RightHomologyData.homologyIso
-- 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₁.HomologyData
h₂ : S₂.HomologyData
γ : HomologyMapData φ h₁ h₂
⊢ homologyMap' φ h₁ h₂ = γ.left.φH

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φH, Subsingleton.elim
-- 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₁.HomologyData
h₂ : S₂.HomologyData
γ : HomologyMapData φ h₁ h₂
⊢ cyclesMap' φ h₁.left h₂.left = γ.left.φK

Tactic:
LeftHomologyMapData.congr_φK (Subsingleton.elim _ _)

Premises used: CategoryTheory.ShortComplex.cyclesMap', CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φK, Subsingleton.elim
-- 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₁.HomologyData
h₂ : S₂.HomologyData
γ : HomologyMapData φ h₁ h₂
⊢ opcyclesMap' φ h₁.right h₂.right = γ.right.φQ

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

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ, CategoryTheory.ShortComplex.opcyclesMap', Subsingleton.elim
-- 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₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
dsimp :
  Eq (α := S₁.homology ⟶ 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₁) ≫
      γ.φH ≫
        CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
          (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left))
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap φ) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)

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

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
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.homology ⟶ 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₁) ≫
      γ.φH ≫
        CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
          (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left))

Tactic:
simp only [← γ.leftHomologyMap'_eq, ← 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.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₂.LeftHomologyData
γ : LeftHomologyMapData φ 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.Iso.inv_hom_id, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq, 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₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
dsimp :
  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)
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap φ) (Iso.hom h₁.homologyIso ≫ γ.φH ≫ Iso.inv h₂.homologyIso)

Tactic:
dsimp [homologyMap, homologyMap', RightHomologyData.homologyIso,
    rightHomologyIso, RightHomologyData.rightHomologyIso]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.RightHomologyData.homologyIso, 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
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
have :
  ∀ (γ' : 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)
⊢ 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:
have γ' : HomologyMapData φ S₁.homologyData S₂.homologyData := default