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 : ShortComplex.{v_1, u_1} C
⊢ S.HasLeftHomology ↔ S.op.HasRightHomology

Tactic:
⟨fun _ => inferInstance, fun _ => HasLeftHomology.mk' S.op.rightHomologyData.unop⟩

Premises used: inferInstance, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.RightHomologyData.unop, CategoryTheory.ShortComplex.op, Iff.intro, CategoryTheory.ShortComplex.HasLeftHomology.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 : ShortComplex.{v_1, u_1} C
⊢ S.HasRightHomology ↔ S.op.HasLeftHomology

Tactic:
⟨fun _ => inferInstance, fun _ => HasRightHomology.mk' S.op.leftHomologyData.unop⟩

Premises used: CategoryTheory.ShortComplex.leftHomologyData, inferInstance, CategoryTheory.ShortComplex.LeftHomologyData.unop, CategoryTheory.ShortComplex.HasRightHomology.mk', CategoryTheory.ShortComplex.op, Iff.intro
-- 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ᵒᵖ
⊢ S.HasLeftHomology ↔ S.unop.HasRightHomology

Tactic:
S.unop.hasRightHomology_iff_op.symm

Premises used: CategoryTheory.ShortComplex.hasRightHomology_iff_op, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.unop, Iff.symm
-- 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ᵒᵖ
⊢ S.HasRightHomology ↔ S.unop.HasLeftHomology

Tactic:
S.unop.hasLeftHomology_iff_op.symm

Premises used: CategoryTheory.ShortComplex.hasLeftHomology_iff_op, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.unop, Iff.symm
-- 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
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
rw : h₁.p ≫ ψ₁.φQ = h₁.p ≫ ψ₂.φQ
rw₁ : φ.τ₂ ≫ h₂.p = h₁.p ≫ ψ₂.φQ
rw₂ rw₃ : φ.τ₂ ≫ h₂.p = φ.τ₂ ≫ h₂.p
⊢ ψ₁.φQ = ψ₂.φQ

Tactic:
rw [← cancel_epi h₁.p, commp, commp]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyMapData.commp
-- 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
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
⊢ ψ₁.φQ = ψ₂.φQ

Tactic:
have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp]
-- 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
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
rw : ψ₁.φH ≫ h₂.ι = ψ₂.φH ≫ h₂.ι
rw₁ : h₁.ι ≫ ψ₁.φQ = ψ₂.φH ≫ h₂.ι
rw₂ : h₁.ι ≫ ψ₁.φQ = h₁.ι ≫ ψ₂.φQ
rw₃ rw₄ : h₁.ι ≫ ψ₂.φQ = h₁.ι ≫ ψ₂.φQ
⊢ ψ₁.φH = ψ₂.φH

Tactic:
rw [← cancel_mono h₂.ι, commι, commι, hQ]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.RightHomologyMapData.commι, CategoryTheory.ShortComplex.RightHomologyData.ι
-- 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
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁.φH = ψ₂.φH

Tactic:
have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_mono h₂.ι, commι, commι, hQ]
-- 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
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
hH : ψ₁.φH = ψ₂.φH
mk :
  ∀ (φQ : h₁.Q ⟶ h₂.Q) (φH : h₁.H ⟶ h₂.H) (commp : h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p) (commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃)
    (commι : φH ≫ h₂.ι = h₁.ι ≫ φQ)
    (hQ :
      { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ =
        ψ₂.φQ)
    (hH :
      { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH =
        ψ₂.φH),
    { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } = ψ₂
⊢ ψ₁ = ψ₂

Tactic:
cases ψ₁
-- 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
ψ₂ : RightHomologyMapData φ h₁ h₂
φQ : h₁.Q ⟶ h₂.Q
φH : h₁.H ⟶ h₂.H
commp : h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
commι : φH ≫ h₂.ι = h₁.ι ≫ φQ
hQ : { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ = ψ₂.φQ
hH : { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH = ψ₂.φH
mk :
  ∀ (φQ_1 : h₁.Q ⟶ h₂.Q) (φH_1 : h₁.H ⟶ h₂.H) (commp_1 : h₁.p ≫ φQ_1 = φ.τ₂ ≫ h₂.p)
    (commg'_1 : φQ_1 ≫ h₂.g' = h₁.g' ≫ φ.τ₃) (commι_1 : φH_1 ≫ h₂.ι = h₁.ι ≫ φQ_1)
    (hQ :
      { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ =
        { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 :
            RightHomologyMapData φ h₁ h₂ }.φQ)
    (hH :
      { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH =
        { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 :
            RightHomologyMapData φ h₁ h₂ }.φH),
    { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } =
      { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 }
⊢ { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } = ψ₂

Tactic:
cases ψ₂
-- 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
φQ : h₁.Q ⟶ h₂.Q
φH : h₁.H ⟶ h₂.H
commp : h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
commι : φH ≫ h₂.ι = h₁.ι ≫ φQ
φQ_1 : h₁.Q ⟶ h₂.Q
φH_1 : h₁.H ⟶ h₂.H
commp_1 : h₁.p ≫ φQ_1 = φ.τ₂ ≫ h₂.p
commg'_1 : φQ_1 ≫ h₂.g' = h₁.g' ≫ φ.τ₃
commι_1 : φH_1 ≫ h₂.ι = h₁.ι ≫ φQ_1
hQ :
  { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φQ =
    { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 : RightHomologyMapData φ h₁ h₂ }.φQ
hH :
  { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ }.φH =
    { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 : RightHomologyMapData φ h₁ h₂ }.φH
⊢ { φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι : RightHomologyMapData φ h₁ h₂ } =
    { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 }

Tactic:
congr
-- 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
rw : φ.τ₁ ≫ S₂.f ≫ h₂.p = 0
rw₁ : Eq (α := S₁.X₁ ⟶ h₂.Q) (φ.τ₁ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ h₂.Q) 0 0
⊢ S₁.f ≫ φ.τ₂ ≫ h₂.p = 0

Tactic:
rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.wp, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc
-- 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
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
rw : h₁.p ≫ φQ ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₁ : (φ.τ₂ ≫ h₂.p) ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₂ : φ.τ₂ ≫ h₂.p ≫ h₂.g' = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₃ : φ.τ₂ ≫ S₂.g = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₄ : S₁.g ≫ φ.τ₃ = h₁.p ≫ h₁.g' ≫ φ.τ₃
rw₅ rw₆ : S₁.g ≫ φ.τ₃ = S₁.g ≫ φ.τ₃
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃

Tactic:
rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc, CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
⊢ φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃

Tactic:
have commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by
    rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc,
      RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc]
-- 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
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
rw : h₁.ι ≫ φQ ≫ h₂.g' = 0
rw₁ : h₁.ι ≫ h₁.g' ≫ φ.τ₃ = 0
rw₂ : Eq (α := h₁.H ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := h₁.H ⟶ S₂.X₃) 0 0
⊢ (h₁.ι ≫ φQ) ≫ h₂.g' = 0

Tactic:
rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.ι_g'_assoc, 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) ⋯
⊢ h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p

Tactic:
simp [φ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₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) ⋯
⊢ φH ≫ h₂.ι = h₁.ι ≫ φQ

Tactic:
simp [φ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
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) ⋯
⊢ RightHomologyMapData φ h₁ h₂

Tactic:
exact ⟨φQ, φH, by simp [φQ], commg', by simp [φ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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
rw rw₁ : γ₂.φH = γ₂.φH
⊢ γ₁.φ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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
rw rw₁ : γ₂.φQ = γ₂.φQ
⊢ γ₁.φQ = γ₂.φQ

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
φ_1 : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
c₁ : KernelFork S₁.g
hc₁ : IsLimit c₁
hf₂ : S₂.f = 0
c₂ : KernelFork S₂.g
hc₂ : IsLimit c₂
f : c₁.pt ⟶ c₂.pt
comm : Fork.ι c₁ ≫ φ.τ₂ = f ≫ Fork.ι c₂
⊢ φ.τ₂ ≫ (RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂).g' =
    (RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁).g' ≫ φ.τ₃

Tactic:
simp only [RightHomologyData.ofIsLimitKernelFork_g', φ.comm₂₃]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
⊢ S.rightHomologyData.H = S.rightHomology

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.rightHomology, 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
⊢ Eq (α := S.X₁ ⟶ S.opcycles) (S.f ≫ S.pOpcycles) 0

Tactic:
S.rightHomologyData.wp

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.RightHomologyData.wp, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.rightHomologyData
-- 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
⊢ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles = S.g

Tactic:
S.rightHomologyData.p_g'

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.fromOpcycles, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
⊢ Epi S.rightHomologyData.p

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 : S.HasRightHomology
⊢ Mono 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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
A : C
f₁ f₂ : A ⟶ S.rightHomology
rw rw₁ : f₁ = f₂ ↔ f₁ = f₂
⊢ f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι

Tactic:
rw [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- 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
A : C
f₁ f₂ : A ⟶ S.rightHomology
h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι
⊢ f₁ = f₂

Tactic:
simpa only [rightHomology_ext_iff]

Premises used: CategoryTheory.ShortComplex.rightHomology_ext_iff
-- 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
A : C
f₁ f₂ : S.opcycles ⟶ A
rw rw₁ : f₁ = f₂ ↔ f₁ = f₂
⊢ f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂

Tactic:
rw [cancel_epi]

Premises used: CategoryTheory.cancel_epi
-- 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
A : C
f₁ f₂ : S.opcycles ⟶ A
h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂
⊢ f₁ = f₂

Tactic:
simpa only [opcycles_ext_iff]

Premises used: CategoryTheory.ShortComplex.opcycles_ext_iff
-- 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
hf : S.f = 0
⊢ IsIso (Y := S.opcycles) S.pOpcycles

Tactic:
RightHomologyData.isIso_p _ hf

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.RightHomologyData.isIso_p
-- 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 : S.HasRightHomology
hf : S.f = 0
⊢ IsIso (Y := S.opcycles) S.pOpcycles

Tactic:
have := S.isIso_pOpcycles hf
-- 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 : S.HasRightHomology
hf : S.f = 0
this : IsIso (Y := S.opcycles) S.pOpcycles
⊢ S.opcycles ≅ S.X₂

Tactic:
exact (asIso S.pOpcycles).symm

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- 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
hf : S.f = 0
⊢ CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (Iso.hom (S.opcyclesIsoX₂ hf)) = 𝟙 S.X₂

Tactic:
(S.opcyclesIsoX₂ hf).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.opcyclesIsoX₂
-- 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
hf : S.f = 0
⊢ Iso.hom (S.opcyclesIsoX₂ hf) ≫ S.pOpcycles = 𝟙 S.opcycles

Tactic:
(S.opcyclesIsoX₂ hf).hom_inv_id

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.opcyclesIsoX₂
-- 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
hg : S.g = 0
⊢ IsIso (X := S.rightHomology) S.rightHomologyι

Tactic:
RightHomologyData.isIso_ι _ hg

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.RightHomologyData.isIso_ι, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : S.HasRightHomology
hg : S.g = 0
⊢ IsIso (X := S.rightHomology) S.rightHomologyι

Tactic:
have := S.isIso_rightHomologyι hg
-- 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 : S.HasRightHomology
hg : S.g = 0
this : IsIso (X := S.rightHomology) S.rightHomologyι
⊢ S.opcycles ≅ S.rightHomology

Tactic:
exact (asIso S.rightHomologyι).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.rightHomologyι, CategoryTheory.asIso
-- 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
hg : S.g = 0
⊢ S.rightHomologyι ≫ Iso.hom (S.opcyclesIsoRightHomology hg) = 𝟙 S.rightHomology

Tactic:
(S.opcyclesIsoRightHomology hg).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.rightHomologyι, CategoryTheory.ShortComplex.opcyclesIsoRightHomology
-- 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
hg : S.g = 0
⊢ Iso.hom (S.opcyclesIsoRightHomology hg) ≫ S.rightHomologyι = 𝟙 S.opcycles

Tactic:
(S.opcyclesIsoRightHomology hg).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.rightHomologyι, CategoryTheory.ShortComplex.opcyclesIsoRightHomology
-- 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
⊢ h₁.p ≫ opcyclesMap' φ h₁ h₂ = φ.τ₂ ≫ h₂.p

Tactic:
RightHomologyMapData.commp _

Premises used: CategoryTheory.ShortComplex.opcyclesMap', CategoryTheory.ShortComplex.RightHomologyMapData.commp
-- 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
⊢ opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃

Tactic:
simp only [← cancel_epi h₁.p, φ.comm₂₃, p_opcyclesMap'_assoc,
    RightHomologyData.p_g'_assoc, RightHomologyData.p_g']

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.p_opcyclesMap'_assoc, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, 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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ h₁ h₂ ≫ h₂.ι = h₁.ι ≫ opcyclesMap' φ h₁ h₂

Tactic:
RightHomologyMapData.commι _

Premises used: CategoryTheory.ShortComplex.rightHomologyMap', CategoryTheory.ShortComplex.RightHomologyMapData.commι, 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
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.X₂ ⟶ S₂.opcycles) (CategoryStruct.comp (Y := S₁.opcycles) S₁.pOpcycles (opcyclesMap φ))
    (φ.τ₂ ≫ S₂.pOpcycles)

Tactic:
p_opcyclesMap' _ _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.ShortComplex.p_opcyclesMap', 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
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.opcycles ⟶ S₂.X₃) (CategoryStruct.comp (Y := S₂.opcycles) (opcyclesMap φ) S₂.fromOpcycles)
    (S₁.fromOpcycles ≫ φ.τ₃)

Tactic:
opcyclesMap'_g' _ _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap'_g', CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.fromOpcycles