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
inst_2 : S.HasHomology
dsimp : Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0
⊢ Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.homologyπ) 0

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.X₁ ⟶ S.homology) (S.toCycles ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0

Tactic:
simp only [toCycles_comp_leftHomologyπ_assoc, zero_comp]

Premises used: CategoryTheory.ShortComplex.toCycles_comp_leftHomologyπ_assoc, CategoryTheory.Limits.zero_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
dsimp : Eq (α := S.homology ⟶ S.X₃) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.fromOpcycles) 0
⊢ Eq (α := S.homology ⟶ S.X₃) (S.homologyι ≫ S.fromOpcycles) 0

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.homology ⟶ S.X₃) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.fromOpcycles) 0

Tactic:
simp only [assoc, rightHomologyι_comp_fromOpcycles, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles
-- 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
A : C
inst_2 : S.HasHomology
⊢ Eq (α :=
    Cone.pt (F := parallelPair (X := S.opcycles) S.fromOpcycles 0) (KernelFork.ofι S.rightHomologyι ⋯) ⟶ S.opcycles)
    (CategoryStruct.comp (Y :=
        Cone.pt (F := parallelPair (X := S.opcycles) S.fromOpcycles 0)
          (KernelFork.ofι (Z := S.homology) S.homologyι ⋯ : KernelFork (X := S.opcycles) S.fromOpcycles))
        (Iso.hom S.rightHomologyIso) (Fork.ι (KernelFork.ofι (Z := S.homology) S.homologyι ⋯)) :
      Cone.pt (F := parallelPair (X := S.opcycles) S.fromOpcycles 0) (KernelFork.ofι S.rightHomologyι ⋯) ⟶ S.opcycles)
    (Fork.ι (KernelFork.ofι S.rightHomologyι ⋯) :
      Cone.pt (F := parallelPair (X := S.opcycles) S.fromOpcycles 0) (KernelFork.ofι S.rightHomologyι ⋯) ⟶ S.opcycles)

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₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
⊢ Epi (X := S.cycles) (Y := S.homology) S.homologyπ

Tactic:
Limits.epi_of_isColimit_cofork (S.homologyIsCokernel)

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyIsCokernel, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.epi_of_isColimit_cofork
-- 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
A : C
inst_2 : S.HasHomology
⊢ Mono (X := S.homology) S.homologyι

Tactic:
Limits.mono_of_isLimit_fork (S.homologyIsKernel)

Premises used: CategoryTheory.ShortComplex.homologyIsKernel, CategoryTheory.ShortComplex.homology, CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.Limits.Fork.ι, 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
A : C
inst_2 : S.HasHomology
k : S.cycles ⟶ A
hk : S.toCycles ≫ k = 0
⊢ CategoryStruct.comp (Y := S.homology) S.homologyπ (S.descHomology k hk) = k

Tactic:
Cofork.IsColimit.π_desc S.homologyIsCokernel

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.descHomology, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyIsCokernel, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.Cofork.π
-- 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
A : C
inst_2 : S.HasHomology
k : A ⟶ S.opcycles
hk : k ≫ S.fromOpcycles = 0
⊢ CategoryStruct.comp (Y := S.homology) (S.liftHomology k hk) S.homologyι = k

Tactic:
Fork.IsLimit.lift_ι S.homologyIsKernel

Premises used: CategoryTheory.ShortComplex.homologyIsKernel, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.ShortComplex.homology, CategoryTheory.Limits.Fork.ι, CategoryTheory.ShortComplex.homologyι, CategoryTheory.ShortComplex.liftHomology
-- 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
simp :
  Eq (α := S₁.cycles ⟶ S₂.leftHomology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (Iso.inv S₁.leftHomologyIso ≫ leftHomologyMap φ) :
      S₁.cycles ⟶ S₂.leftHomology)
    (cyclesMap φ ≫ S₂.leftHomologyπ : S₁.cycles ⟶ S₂.leftHomology)
⊢ Eq (α := S₁.cycles ⟶ S₂.homology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology)
    (cyclesMap φ ≫ S₂.homologyπ : S₁.cycles ⟶ S₂.homology)

Tactic:
simp only [← cancel_mono S₂.leftHomologyIso.inv, assoc, ← leftHomologyIso_inv_naturality φ,
    homologyπ_comp_leftHomologyIso_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.leftHomologyIso_inv_naturality, CategoryTheory.ShortComplex.leftHomologyIso, CategoryTheory.Iso.inv
-- 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
⊢ Eq (α := S₁.cycles ⟶ S₂.leftHomology)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (Iso.inv S₁.leftHomologyIso ≫ leftHomologyMap φ) :
      S₁.cycles ⟶ S₂.leftHomology)
    (cyclesMap φ ≫ S₂.leftHomologyπ : S₁.cycles ⟶ S₂.leftHomology)

Tactic:
simp only [homologyπ, assoc, Iso.hom_inv_id_assoc, leftHomologyπ_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.leftHomologyπ_naturality, CategoryTheory.Iso.hom_inv_id_assoc
-- 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
simp :
  Eq (α := S₁.rightHomology ⟶ S₂.opcycles) (S₁.rightHomologyι ≫ opcyclesMap φ : S₁.rightHomology ⟶ S₂.opcycles)
    (CategoryStruct.comp (Y := S₁.homology) (Iso.hom S₁.rightHomologyIso) (S₁.homologyι ≫ opcyclesMap φ) :
      S₁.rightHomology ⟶ S₂.opcycles)
⊢ Eq (α := S₁.homology ⟶ S₂.opcycles)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) S₂.homologyι : S₁.homology ⟶ S₂.opcycles)
    (S₁.homologyι ≫ opcyclesMap φ : S₁.homology ⟶ S₂.opcycles)

Tactic:
simp only [← cancel_epi S₁.rightHomologyIso.hom, rightHomologyIso_hom_naturality_assoc φ,
    rightHomologyIso_hom_comp_homologyι, rightHomologyι_naturality]

Premises used: CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyIso_hom_comp_homologyι, CategoryTheory.ShortComplex.rightHomologyIso_hom_naturality_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.ShortComplex.rightHomologyι_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₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.rightHomology ⟶ S₂.opcycles) (S₁.rightHomologyι ≫ opcyclesMap φ : S₁.rightHomology ⟶ S₂.opcycles)
    (CategoryStruct.comp (Y := S₁.homology) (Iso.hom S₁.rightHomologyIso) (S₁.homologyι ≫ opcyclesMap φ) :
      S₁.rightHomology ⟶ S₂.opcycles)

Tactic:
simp only [homologyι, assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_assoc, 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
dsimp :
  Eq (α := S.cycles ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
        (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
      S.cycles ⟶ S.opcycles)
    (S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles)
⊢ Eq (α := S.cycles ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) S.homologyπ S.homologyι : S.cycles ⟶ S.opcycles)
    (S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles)

Tactic:
dsimp only [homologyπ, homologyι]

Premises used: CategoryTheory.ShortComplex.homologyπ, 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.opcycles)
    (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
        (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
      S.cycles ⟶ S.opcycles)
    (S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles)

Tactic:
simpa only [assoc, S.leftRightHomologyComparison_fac] using S.π_leftRightHomologyComparison_ι

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison_fac, CategoryTheory.ShortComplex.π_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.HasHomology
h : S.LeftHomologyData
dsimp :
  Eq (α := S.cycles ⟶ h.H)
    (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
        (Iso.hom (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso)) :
      S.cycles ⟶ h.H)
    (Iso.hom h.cyclesIso ≫ h.π : S.cycles ⟶ h.H)
⊢ Eq (α := S.cycles ⟶ h.H) (CategoryStruct.comp (Y := S.homology) S.homologyπ (Iso.hom h.homologyIso) : S.cycles ⟶ h.H)
    (Iso.hom h.cyclesIso ≫ h.π : S.cycles ⟶ h.H)

Tactic:
dsimp only [homologyπ, homologyIso]

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso
-- 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
h : S.LeftHomologyData
⊢ Eq (α := S.cycles ⟶ h.H)
    (CategoryStruct.comp (Y := S.homology) (S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
        (Iso.hom (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso)) :
      S.cycles ⟶ h.H)
    (Iso.hom h.cyclesIso ≫ h.π : S.cycles ⟶ h.H)

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id_assoc,
    leftHomologyπ_comp_leftHomologyIso_hom]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom, CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.Iso.hom_inv_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
inst_2 : S.HasHomology
h : S.LeftHomologyData
dsimp :
  Eq (α := h.K ⟶ S.homology) (h.π ≫ Iso.inv (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso))
    (Iso.inv h.cyclesIso ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)
⊢ Eq (α := h.K ⟶ S.homology) (h.π ≫ Iso.inv h.homologyIso) (Iso.inv h.cyclesIso ≫ S.homologyπ)

Tactic:
dsimp only [homologyπ, homologyIso]

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso
-- 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
h : S.LeftHomologyData
⊢ Eq (α := h.K ⟶ S.homology) (h.π ≫ Iso.inv (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso))
    (Iso.inv h.cyclesIso ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso)

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, π_comp_leftHomologyIso_inv_assoc]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_comp_leftHomologyIso_inv_assoc, CategoryTheory.Iso.symm_inv, CategoryTheory.Iso.trans_inv
-- 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
h : S.RightHomologyData
dsimp :
  Eq (α := h.H ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.inv (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso))
        (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
      h.H ⟶ S.opcycles)
    (h.ι ≫ Iso.inv h.opcyclesIso : h.H ⟶ S.opcycles)
⊢ Eq (α := h.H ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.inv h.homologyIso) S.homologyι : h.H ⟶ S.opcycles)
    (h.ι ≫ Iso.inv h.opcyclesIso : h.H ⟶ S.opcycles)

Tactic:
dsimp only [homologyι, homologyIso]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.homologyIso, 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
h : S.RightHomologyData
⊢ Eq (α := h.H ⟶ S.opcycles)
    (CategoryStruct.comp (Y := S.homology) (Iso.inv (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso))
        (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) :
      h.H ⟶ S.opcycles)
    (h.ι ≫ Iso.inv h.opcyclesIso : h.H ⟶ S.opcycles)

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, assoc, Iso.hom_inv_id_assoc,
    rightHomologyIso_inv_comp_rightHomologyι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι, CategoryTheory.Iso.trans_inv
-- 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
h : S.RightHomologyData
dsimp :
  Eq (α := S.homology ⟶ h.Q) (Iso.hom (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso) ≫ h.ι)
    ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ Iso.hom h.opcyclesIso)
⊢ Eq (α := S.homology ⟶ h.Q) (Iso.hom h.homologyIso ≫ h.ι) (S.homologyι ≫ Iso.hom h.opcyclesIso)

Tactic:
dsimp only [homologyι, homologyIso]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.homologyIso, 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
h : S.RightHomologyData
⊢ Eq (α := S.homology ⟶ h.Q) (Iso.hom (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso) ≫ h.ι)
    ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ Iso.hom h.opcyclesIso)

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, rightHomologyIso_hom_comp_ι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_ι, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.trans_hom
-- 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
h : S.LeftHomologyData
dsimp :
  Eq (α := S.homology ⟶ S.leftHomology)
    (Iso.hom (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso) ≫ Iso.inv h.leftHomologyIso) (Iso.inv S.leftHomologyIso)
⊢ Eq (α := S.homology ⟶ S.leftHomology) (Iso.hom h.homologyIso ≫ Iso.inv h.leftHomologyIso) (Iso.inv S.leftHomologyIso)

Tactic:
dsimp only [homologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.homologyIso
-- 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
h : S.LeftHomologyData
⊢ Eq (α := S.homology ⟶ S.leftHomology)
    (Iso.hom (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso) ≫ Iso.inv h.leftHomologyIso) (Iso.inv S.leftHomologyIso)

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.trans_hom
-- 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
h : S.LeftHomologyData
dsimp :
  Eq (α := S.leftHomology ⟶ S.homology)
    (Iso.hom h.leftHomologyIso ≫ Iso.inv (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso)) (Iso.hom S.leftHomologyIso)
⊢ Eq (α := S.leftHomology ⟶ S.homology) (Iso.hom h.leftHomologyIso ≫ Iso.inv h.homologyIso) (Iso.hom S.leftHomologyIso)

Tactic:
dsimp only [homologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.homologyIso
-- 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
h : S.LeftHomologyData
⊢ Eq (α := S.leftHomology ⟶ S.homology)
    (Iso.hom h.leftHomologyIso ≫ Iso.inv (Iso.symm S.leftHomologyIso ≪≫ h.leftHomologyIso)) (Iso.hom S.leftHomologyIso)

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.symm_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Iso.trans_inv
-- 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
h : S.RightHomologyData
dsimp :
  Eq (α := S.homology ⟶ S.rightHomology)
    (Iso.hom (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso) ≫ Iso.inv h.rightHomologyIso)
    (Iso.inv S.rightHomologyIso)
⊢ Eq (α := S.homology ⟶ S.rightHomology) (Iso.hom h.homologyIso ≫ Iso.inv h.rightHomologyIso)
    (Iso.inv S.rightHomologyIso)

Tactic:
dsimp only [homologyIso]

Premises used: 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 : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ Eq (α := S.homology ⟶ S.rightHomology)
    (Iso.hom (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso) ≫ Iso.inv h.rightHomologyIso)
    (Iso.inv S.rightHomologyIso)

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.trans_hom
-- 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
h : S.RightHomologyData
dsimp :
  Eq (α := S.rightHomology ⟶ S.homology)
    (Iso.hom h.rightHomologyIso ≫ Iso.inv (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso))
    (Iso.hom S.rightHomologyIso)
⊢ Eq (α := S.rightHomology ⟶ S.homology) (Iso.hom h.rightHomologyIso ≫ Iso.inv h.homologyIso)
    (Iso.hom S.rightHomologyIso)

Tactic:
dsimp only [homologyIso]

Premises used: 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 : ShortComplex.{v, u} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ Eq (α := S.rightHomology ⟶ S.homology)
    (Iso.hom h.rightHomologyIso ≫ Iso.inv (Iso.symm S.rightHomologyIso ≪≫ h.rightHomologyIso))
    (Iso.hom S.rightHomologyIso)

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.symm_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Iso.trans_inv
-- 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₂.RightHomologyData
dsimp :
  h₁.π ≫
      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 ≫
          CategoryStruct.comp (Y := S₂.rightHomology)
              (S₂.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₂) S₂.homologyData.right S₂.rightHomologyData)
              (rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData h₂) ≫
            h₂.ι) =
    h₁.i ≫ φ.τ₂ ≫ h₂.p
⊢ h₁.π ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso ≫ h₂.ι)) =
    h₁.i ≫ φ.τ₂ ≫ h₂.p

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

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso, CategoryTheory.ShortComplex.leftHomologyMapIso', CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.leftHomologyIso, CategoryTheory.ShortComplex.homologyMap