awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₂ : LeftHomologyMapData φ h₁ h₂
φK : h₁.K ⟶ h₂.K
φH : h₁.H ⟶ h₂.H
commi : φK ≫ h₂.i = h₁.i ≫ φ.τ₂
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
commπ : h₁.π ≫ φH = φK ≫ h₂.π
hK : { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φK = ψ₂.φK
hH : { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φH = ψ₂.φH
mk :
  ∀ (φK_1 : h₁.K ⟶ h₂.K) (φH_1 : h₁.H ⟶ h₂.H) (commi_1 : φK_1 ≫ h₂.i = h₁.i ≫ φ.τ₂)
    (commf'_1 : h₁.f' ≫ φK_1 = φ.τ₁ ≫ h₂.f') (commπ_1 : h₁.π ≫ φH_1 = φK_1 ≫ h₂.π)
    (hK :
      { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φK =
        { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 :
            LeftHomologyMapData φ h₁ h₂ }.φK)
    (hH :
      { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φH =
        { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 :
            LeftHomologyMapData φ h₁ h₂ }.φH),
    { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } =
      { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 }
⊢ { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } = ψ₂

Tactic:
cases ψ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K
φH : h₁.H ⟶ h₂.H
commi : φK ≫ h₂.i = h₁.i ≫ φ.τ₂
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
commπ : h₁.π ≫ φH = φK ≫ h₂.π
φK_1 : h₁.K ⟶ h₂.K
φH_1 : h₁.H ⟶ h₂.H
commi_1 : φK_1 ≫ h₂.i = h₁.i ≫ φ.τ₂
commf'_1 : h₁.f' ≫ φK_1 = φ.τ₁ ≫ h₂.f'
commπ_1 : h₁.π ≫ φH_1 = φK_1 ≫ h₂.π
hK :
  { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φK =
    { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 : LeftHomologyMapData φ h₁ h₂ }.φK
hH :
  { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ }.φH =
    { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 : LeftHomologyMapData φ h₁ h₂ }.φH
⊢ { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } =
    { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : h₁.i ≫ φ.τ₂ ≫ S₂.g = 0
rw₁ : h₁.i ≫ S₁.g ≫ φ.τ₃ = 0
rw₂ : Eq (α := h₁.K ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := h₁.K ⟶ S₂.X₃) 0 0
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0

Tactic:
rw [assoc, φ.comm₂₃, h₁.wi_assoc, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.LeftHomologyData.wi_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
rw : (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
rw₁ : h₁.f' ≫ φK ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
rw₂ : h₁.f' ≫ φK ≫ h₂.i = φ.τ₁ ≫ h₂.f' ≫ h₂.i
rw₃ : h₁.f' ≫ h₁.i ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
rw₄ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ h₂.f' ≫ h₂.i
rw₅ : S₁.f ≫ φ.τ₂ = φ.τ₁ ≫ S₂.f
rw₆ rw₇ : S₁.f ≫ φ.τ₂ = S₁.f ≫ φ.τ₂
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'

Tactic:
rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i, φ.comm₁₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'

Tactic:
have commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f' := by
    rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i, φ.comm₁₂]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
rw : φ.τ₁ ≫ h₂.f' ≫ h₂.π = 0
rw₁ : Eq (α := S₁.X₁ ⟶ h₂.H) (φ.τ₁ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ h₂.H) 0 0
⊢ h₁.f' ≫ φK ≫ h₂.π = 0

Tactic:
rw [reassoc_of% commf', h₂.f'_π, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.f'_π
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π) ⋯
⊢ φK ≫ h₂.i = h₁.i ≫ φ.τ₂

Tactic:
simp [φK]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π) ⋯
⊢ h₁.π ≫ φH = φK ≫ h₂.π

Tactic:
simp [φH]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π) ⋯
⊢ LeftHomologyMapData φ h₁ h₂

Tactic:
exact ⟨φK, φH, by simp [φK], commf', by simp [φH]⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
rw rw₁ : γ₂.φH = γ₂.φH
⊢ γ₁.φH = γ₂.φH

Tactic:
rw [eq]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
rw rw₁ : γ₂.φK = γ₂.φK
⊢ γ₁.φK = γ₂.φK

Tactic:
rw [eq]
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
c₁ : CokernelCofork S₁.f
hc₁ : IsColimit c₁
hg₂ : S₂.g = 0
c₂ : CokernelCofork S₂.f
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
comm : φ.τ₂ ≫ Cofork.π c₂ = Cofork.π c₁ ≫ f
⊢ (LeftHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁).f' ≫ φ.τ₂ =
    φ.τ₁ ≫ (LeftHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂).f'

Tactic:
simp only [LeftHomologyData.ofIsColimitCokernelCofork_f', φ.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_f'
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ S.leftHomologyData.H = S.leftHomology

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.leftHomology, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ Eq (α := S.cycles ⟶ S.X₃) (S.iCycles ≫ S.g) 0

Tactic:
S.leftHomologyData.wi

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.wi, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles = S.f

Tactic:
S.leftHomologyData.f'_i

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ Mono S.leftHomologyData.i

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ Epi S.leftHomologyData.π

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
A : C
f₁ f₂ : S.leftHomology ⟶ A
rw rw₁ : f₁ = f₂ ↔ f₁ = f₂
⊢ f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂

Tactic:
rw [cancel_epi]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
A : C
f₁ f₂ : S.leftHomology ⟶ A
h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂
⊢ f₁ = f₂

Tactic:
simpa only [leftHomology_ext_iff] using h

Premises used: CategoryTheory.ShortComplex.leftHomology_ext_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
A : C
f₁ f₂ : A ⟶ S.cycles
rw rw₁ : f₁ = f₂ ↔ f₁ = f₂
⊢ f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles

Tactic:
rw [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
A : C
f₁ f₂ : A ⟶ S.cycles
h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles
⊢ f₁ = f₂

Tactic:
simpa only [cycles_ext_iff] using h

Premises used: CategoryTheory.ShortComplex.cycles_ext_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hg : S.g = 0
⊢ IsIso (X := S.cycles) S.iCycles

Tactic:
LeftHomologyData.isIso_i _ hg

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.isIso_i, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hg : S.g = 0
⊢ IsIso (X := S.cycles) S.iCycles

Tactic:
have := S.isIso_iCycles hg
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hg : S.g = 0
this : IsIso (X := S.cycles) S.iCycles
⊢ S.cycles ≅ S.X₂

Tactic:
exact asIso S.iCycles

Premises used: CategoryTheory.ShortComplex.iCycles, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hg : S.g = 0
⊢ S.iCycles ≫ Iso.inv (S.cyclesIsoX₂ hg) = 𝟙 S.cycles

Tactic:
(S.cyclesIsoX₂ hg).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cyclesIsoX₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hg : S.g = 0
⊢ CategoryStruct.comp (Y := S.cycles) (Iso.inv (S.cyclesIsoX₂ hg)) S.iCycles = 𝟙 S.X₂

Tactic:
(S.cyclesIsoX₂ hg).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cyclesIsoX₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hf : S.f = 0
⊢ IsIso (X := S.cycles) S.leftHomologyπ

Tactic:
LeftHomologyData.isIso_π _ hf

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.LeftHomologyData.isIso_π, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hf : S.f = 0
⊢ IsIso (X := S.cycles) S.leftHomologyπ

Tactic:
have := S.isIso_leftHomologyπ hf
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hf : S.f = 0
this : IsIso (X := S.cycles) S.leftHomologyπ
⊢ S.cycles ≅ S.leftHomology

Tactic:
exact asIso S.leftHomologyπ

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hf : S.f = 0
⊢ S.leftHomologyπ ≫ Iso.inv (S.cyclesIsoLeftHomology hf) = 𝟙 S.cycles

Tactic:
(S.cyclesIsoLeftHomology hf).hom_inv_id

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.cyclesIsoLeftHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
hf : S.f = 0
⊢ Iso.inv (S.cyclesIsoLeftHomology hf) ≫ S.leftHomologyπ = 𝟙 S.leftHomology

Tactic:
(S.cyclesIsoLeftHomology hf).inv_hom_id

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.cyclesIsoLeftHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' φ h₁ h₂ ≫ h₂.i = h₁.i ≫ φ.τ₂

Tactic:
LeftHomologyMapData.commi _

Premises used: CategoryTheory.ShortComplex.cyclesMap', CategoryTheory.ShortComplex.LeftHomologyMapData.commi
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.f' ≫ cyclesMap' φ h₁ h₂ = φ.τ₁ ≫ h₂.f'

Tactic:
simp only [← cancel_mono h₂.i, assoc, φ.comm₁₂, cyclesMap'_i,
    LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc, CategoryTheory.ShortComplex.cyclesMap'_i, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.π ≫ leftHomologyMap' φ h₁ h₂ = cyclesMap' φ h₁ h₂ ≫ h₂.π

Tactic:
LeftHomologyMapData.commπ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.cyclesMap', CategoryTheory.ShortComplex.LeftHomologyMapData.commπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.cycles ⟶ S₂.X₂) (CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) S₂.iCycles) (S₁.iCycles ≫ φ.τ₂)

Tactic:
cyclesMap'_i _ _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cyclesMap'_i, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.X₁ ⟶ S₂.cycles) (CategoryStruct.comp (Y := S₁.cycles) S₁.toCycles (cyclesMap φ)) (φ.τ₁ ≫ S₂.toCycles)

Tactic:
f'_cyclesMap' _ _ _

Premises used: CategoryTheory.ShortComplex.f'_cyclesMap', CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cycles, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
φ : S₁ ⟶ S₂
⊢ Eq (α := S₁.cycles ⟶ S₂.leftHomology) (S₁.leftHomologyπ ≫ leftHomologyMap φ) (cyclesMap φ ≫ S₂.leftHomologyπ)

Tactic:
leftHomologyπ_naturality' _ _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.leftHomologyπ_naturality', CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' φ h₁ h₂ = γ.φH

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φH, Subsingleton.elim
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' φ h₁ h₂ = γ.φK

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

Premises used: CategoryTheory.ShortComplex.cyclesMap', CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φK, Subsingleton.elim
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
⊢ leftHomologyMap' (𝟙 S) h h = 𝟙 h.H

Tactic:
(LeftHomologyMapData.id h).leftHomologyMap'_eq

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.id, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
⊢ cyclesMap' (𝟙 S) h h = 𝟙 h.K

Tactic:
(LeftHomologyMapData.id h).cyclesMap'_eq

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.id, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ leftHomologyMap (𝟙 S) = 𝟙 S.leftHomology

Tactic:
leftHomologyMap'_id _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.leftHomologyMap'_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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.HasLeftHomology
⊢ cyclesMap (𝟙 S) = 𝟙 S.cycles

Tactic:
cyclesMap'_id _

Premises used: CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cyclesMap'_id, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' 0 h₁ h₂ = 0

Tactic:
(LeftHomologyMapData.zero h₁ h₂).leftHomologyMap'_eq

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.zero, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' 0 h₁ h₂ = 0

Tactic:
(LeftHomologyMapData.zero h₁ h₂).cyclesMap'_eq

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.zero, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq.{v_1 + 1} (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap 0) 0

Tactic:
leftHomologyMap'_zero _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.leftHomologyMap'_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology
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₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq.{v_1 + 1} (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap 0) 0

Tactic:
cyclesMap'_zero _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap'_zero, CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cycles