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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ Epi (opMap φ).τ₁

Tactic:
haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
-- 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₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₂) (Y := Opposite.op S₁.X₂) φ.τ₂.op

Tactic:
infer_instance
-- 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₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso (opMap φ).τ₂

Tactic:
haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
-- 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₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this_1 : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₁) (Y := Opposite.op S₁.X₁) φ.τ₁.op

Tactic:
infer_instance
-- 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₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this_1 : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono (opMap φ).τ₃

Tactic:
haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
-- 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₂
h : S₁.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this_1 : Epi (opMap φ).τ₁
this_2 : IsIso (opMap φ).τ₂
this : Mono (opMap φ).τ₃
⊢ S₂.RightHomologyData

Tactic:
exact (LeftHomologyData.ofEpiOfIsIsoOfMono' (opMap φ) h.op).unop

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.unop, CategoryTheory.ShortComplex.opMap, CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono', CategoryTheory.ShortComplex.RightHomologyData.op
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).Q = h.Q

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.unop, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).H = h.H

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.unop, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).p = inv φ.τ₂ ≫ h.p

Tactic:
simp [ofEpiOfIsIsoOfMono, opMap]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono, CategoryTheory.ShortComplex.opMap
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).ι = h.ι

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.ShortComplex.unop, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).g' = h.g' ≫ φ.τ₃

Tactic:
simp [ofEpiOfIsIsoOfMono, opMap]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono, CategoryTheory.ShortComplex.opMap
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ Epi.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₃) (Y := Opposite.op S₁.X₃) φ.τ₃.op

Tactic:
infer_instance
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ Epi (opMap φ).τ₁

Tactic:
haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₂) (Y := Opposite.op S₁.X₂) φ.τ₂.op

Tactic:
infer_instance
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso (opMap φ).τ₂

Tactic:
haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this_1 : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₁) (Y := Opposite.op S₁.X₁) φ.τ₁.op

Tactic:
infer_instance
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this_1 : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono (opMap φ).τ₃

Tactic:
haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
-- 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₂
h : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
this_1 : Epi (opMap φ).τ₁
this_2 : IsIso (opMap φ).τ₂
this : Mono (opMap φ).τ₃
⊢ S₁.RightHomologyData

Tactic:
exact (LeftHomologyData.ofEpiOfIsIsoOfMono (opMap φ) h.op).unop

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.unop, CategoryTheory.ShortComplex.opMap, CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono, CategoryTheory.ShortComplex.RightHomologyData.op
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).Q = h.Q

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.unop, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).H = h.H

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.unop, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).p = φ.τ₂ ≫ h.p

Tactic:
simp [ofEpiOfIsIsoOfMono', opMap]

Premises used: CategoryTheory.ShortComplex.opMap, CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).ι = h.ι

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.ShortComplex.unop, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).p ≫ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₁ : S₁.g ≫ φ.τ₃ = (ofEpiOfIsIsoOfMono' φ h).p ≫ h.g'
rw₂ : S₁.g ≫ φ.τ₃ = (φ.τ₂ ≫ h.p) ≫ h.g'
rw₃ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ h.p ≫ h.g'
rw₄ : S₁.g ≫ φ.τ₃ = φ.τ₂ ≫ S₂.g
rw₅ rw₆ : S₁.g ≫ φ.τ₃ = S₁.g ≫ φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'

Tactic:
rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_p, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono', CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- 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₂
inst_2 : S₁.HasRightHomology
inst_3 : Epi φ.τ₁
inst_4 : IsIso φ.τ₂
inst_5 : Mono φ.τ₃
⊢ S₂.HasRightHomology

Tactic:
HasRightHomology.mk' (RightHomologyData.ofEpiOfIsIsoOfMono φ S₁.rightHomologyData)

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.HasRightHomology.mk'
-- 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₂
inst_2 : S₂.HasRightHomology
inst_3 : Epi φ.τ₁
inst_4 : IsIso φ.τ₂
inst_5 : Mono φ.τ₃
⊢ S₁.HasRightHomology

Tactic:
HasRightHomology.mk' (RightHomologyData.ofEpiOfIsIsoOfMono' φ S₂.rightHomologyData)

Premises used: CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.HasRightHomology.mk', CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'
-- 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
e : S₁ ≅ S₂
inst_2 : S₁.HasRightHomology
⊢ S₂.HasRightHomology

Tactic:
hasRightHomology_of_epi_of_isIso_of_mono e.hom

Premises used: CategoryTheory.ShortComplex.hasRightHomology_of_epi_of_isIso_of_mono, CategoryTheory.Iso.hom
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
rw : IsIso (Y := h₂'.H) (RightHomologyMapData.φH (RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁))
⊢ IsIso (rightHomologyMap' φ h₁ h₂')

Tactic:
rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
dsimp : IsIso.{v_1, u_1} (𝟙 h₁.H)
⊢ IsIso (Y := h₂'.H) (RightHomologyMapData.φH (RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁))

Tactic:
dsimp
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso.{v_1, u_1} (𝟙 h₁.H)

Tactic:
infer_instance
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (rightHomologyMap' φ h₁ h₂')

Tactic:
haveI : IsIso (rightHomologyMap' φ h₁ h₂') := by
    rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
    dsimp
    infer_instance
-- 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
⊢ rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂

Tactic:
have eq := rightHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' 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₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂

Tactic:
rw [comp_id] at eq

Premises used: 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
rw : IsIso (rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂)
⊢ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
rw [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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.RightHomologyData := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂)

Tactic:
infer_instance
-- 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 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
⊢ IsIso (X := S₁.rightHomology) (Y := S₂.rightHomology) (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
infer_instance
-- 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
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : HasKernels.{v_1, u_1} Cᵒᵖ
inst_5 : HasCokernels.{v_1, u_1} Cᵒᵖ
⊢ ∀ {X Y : (ShortComplex.{v_1, u_1} C)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.op (rightHomologyFunctor C)) X ⟶ Functor.obj (opFunctor C ⋙ leftHomologyFunctor Cᵒᵖ) Y)
      (Functor.map (Functor.op (rightHomologyFunctor C)) f ≫
        Iso.hom
          ((fun (S : (ShortComplex.{v_1, u_1} C)ᵒᵖ) ↦
              (Iso.symm (Opposite.unop S).leftHomologyOpIso :
                Opposite.op (Opposite.unop S).rightHomology ≅ (Opposite.unop S).op.leftHomology))
            Y))
      (Iso.hom
          ((fun (S : (ShortComplex.{v_1, u_1} C)ᵒᵖ) ↦
              (Iso.symm (Opposite.unop S).leftHomologyOpIso :
                Opposite.op (Opposite.unop S).rightHomology ≅ (Opposite.unop S).op.leftHomology))
            X) ≫
        Functor.map (opFunctor C ⋙ leftHomologyFunctor Cᵒᵖ) f)

Tactic:
simp [rightHomologyMap_op]

Premises used: CategoryTheory.ShortComplex.rightHomologyMap_op
-- 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
inst_2 : HasKernels.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : HasKernels.{v_1, u_1} Cᵒᵖ
inst_5 : HasCokernels.{v_1, u_1} Cᵒᵖ
⊢ ∀ {X Y : (ShortComplex.{v_1, u_1} C)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.op (leftHomologyFunctor C)) X ⟶ Functor.obj (opFunctor C ⋙ rightHomologyFunctor Cᵒᵖ) Y)
      (Functor.map (Functor.op (leftHomologyFunctor C)) f ≫
        Iso.hom
          ((fun (S : (ShortComplex.{v_1, u_1} C)ᵒᵖ) ↦
              (Iso.symm (Opposite.unop S).rightHomologyOpIso :
                Opposite.op (Opposite.unop S).leftHomology ≅ (Opposite.unop S).op.rightHomology))
            Y))
      (Iso.hom
          ((fun (S : (ShortComplex.{v_1, u_1} C)ᵒᵖ) ↦
              (Iso.symm (Opposite.unop S).rightHomologyOpIso :
                Opposite.op (Opposite.unop S).leftHomology ≅ (Opposite.unop S).op.rightHomology))
            X) ≫
        Functor.map (opFunctor C ⋙ rightHomologyFunctor Cᵒᵖ) f)

Tactic:
simp [leftHomologyMap_op]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap_op
-- 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
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
⊢ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles k hk) = k

Tactic:
RightHomologyData.p_descQ _ k hk

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.RightHomologyData.p_descQ, CategoryTheory.ShortComplex.descOpcycles
-- 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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
A' : C
α : A ⟶ A'
rw : Eq (α := S.X₁ ⟶ A') (0 ≫ α) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ A') 0 0
⊢ S.f ≫ k ≫ α = 0

Tactic:
rw [reassoc_of% hk, zero_comp]

Premises used: CategoryTheory.Limits.zero_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
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ Eq (α := S.opcycles ⟶ A') (S.descOpcycles k hk ≫ α) (S.descOpcycles (k ≫ α) ⋯)

Tactic:
simp only [← cancel_epi S.pOpcycles, p_descOpcycles_assoc, p_descOpcycles]

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.p_descOpcycles_assoc, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.p_descOpcycles
-- 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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
inst_3 : HasCokernel S.f
⊢ Eq (α := S.X₁ ⟶ cokernel S.f) (S.f ≫ cokernel.π S.f) 0

Tactic:
simp
-- 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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
inst_3 : HasCokernel S.f
⊢ Eq (α := S.X₁ ⟶ S.opcycles) (S.f ≫ S.pOpcycles) 0

Tactic:
simp
-- 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
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ Eq (α := S.X₂ ⟶ S.opcycles) (Cofork.π cc ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.pOpcycles

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Cofork.π
-- 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
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (Iso.inv (S.isoOpcyclesOfIsColimit hcc)) = Cofork.π cc

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ S.opcyclesIsCokernel WalkingParallelPair.one

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.opcyclesIsCokernel, CategoryTheory.Limits.Cofork.π
-- 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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_2 : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ A) 0 0
⊢ S.f ≫ k = 0

Tactic:
rw [hx, S.zero_assoc, zero_comp]

Premises used: CategoryTheory.ShortComplex.zero_assoc, CategoryTheory.Limits.zero_comp