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

Tactic:
HasLeftHomology.mk' (LeftHomologyData.ofEpiOfIsIsoOfMono' φ S₂.leftHomologyData)

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

Tactic:
hasLeftHomology_of_epi_of_isIso_of_mono e.hom

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

Tactic:
rw [(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq]

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

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

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

Tactic:
have : IsIso (leftHomologyMap' φ h₁ h₂') := by
    rw [(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq]
    dsimp
    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
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
⊢ leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂

Tactic:
have eq := leftHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
eq : leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
⊢ leftHomologyMap' φ h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂

Tactic:
rw [comp_id] at eq

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

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
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
⊢ IsIso (X := S₁.leftHomology) (Y := S₂.leftHomology) (leftHomologyMap' φ S₁.leftHomologyData 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
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
⊢ CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) S.iCycles = k

Tactic:
LeftHomologyData.liftK_i _ k hk

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.ShortComplex.liftCycles, 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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
A' : C
α : A' ⟶ A
rw : α ≫ k ≫ S.g = 0
rw₁ : Eq (α := A' ⟶ S.X₃) (α ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := A' ⟶ S.X₃) 0 0
⊢ (α ≫ k) ≫ S.g = 0

Tactic:
rw [assoc, hk, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
inst_3 : HasKernel S.g
⊢ Eq (α := S.cycles ⟶ S.X₃) (S.iCycles ≫ S.g) 0

Tactic:
simp
-- 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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
inst_3 : HasKernel S.g
⊢ Eq (α := kernel S.g ⟶ S.X₃) (kernel.ι S.g ≫ S.g) 0

Tactic:
simp
-- 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
kf : KernelFork S.g
hkf : IsLimit kf
⊢ Eq (α := S.cycles ⟶ S.X₂) (Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ Fork.ι kf) S.iCycles

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.Fork.ι, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles, CategoryTheory.Limits.WalkingParallelPair.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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
kf : KernelFork S.g
hkf : IsLimit kf
⊢ CategoryStruct.comp (Y := S.cycles) (Iso.hom (S.isoCyclesOfIsLimit hkf)) S.iCycles = Fork.ι kf

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.Fork.ι, CategoryTheory.ShortComplex.iCycles, CategoryTheory.ShortComplex.cycles, CategoryTheory.Limits.WalkingParallelPair.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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
rw₁ : x ≫ S.f ≫ S.g = 0
rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
⊢ k ≫ S.g = 0

Tactic:
rw [hx, assoc, S.zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.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 : ShortComplex.{v_1, u_1} C
A : C
k : A ⟶ S.X₂
inst_2 : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ Eq (α := A ⟶ S.leftHomology) (S.liftCycles k ⋯ ≫ S.leftHomologyπ) 0

Tactic:
LeftHomologyData.liftK_π_eq_zero_of_boundary _ k x hx

Premises used: CategoryTheory.ShortComplex.leftHomologyπ, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.LeftHomologyData.liftK_π_eq_zero_of_boundary, CategoryTheory.ShortComplex.liftCycles, 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
rw rw₁ : S.f = S.f
⊢ S.f = 𝟙 S.X₁ ≫ S.f

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
φ : S ⟶ S₁
inst_3 : S₁.HasLeftHomology
rw : k ≫ φ.τ₂ ≫ S₁.g = 0
rw₁ : k ≫ S.g ≫ φ.τ₃ = 0
rw₂ : Eq (α := A ⟶ S₁.X₃) (0 ≫ φ.τ₃) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ S₁.X₃) 0 0
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0

Tactic:
rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp
-- 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
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
⊢ CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso) = h.liftK k hk

Tactic:
simp only [← cancel_mono h.i, assoc, LeftHomologyData.cyclesIso_hom_comp_i,
    liftCycles_i, LeftHomologyData.liftK_i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
rw :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso) ≫ Iso.inv h.cyclesIso)
    (S.liftCycles k hk)
rw₁ :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso ≫ Iso.inv h.cyclesIso))
    (S.liftCycles k hk)
rw₂ : S.liftCycles k hk ≫ 𝟙 S.cycles = S.liftCycles k hk
rw₃ rw₄ : Eq (α := A ⟶ S.cycles) (S.liftCycles k hk) (S.liftCycles k hk)
⊢ Eq (α := A ⟶ S.cycles) (h.liftK k hk ≫ Iso.inv h.cyclesIso) (S.liftCycles k hk)

Tactic:
rw [← h.liftCycles_comp_cyclesIso_hom, assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom
-- 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
⊢ HasKernel S.g

Tactic:
⟨⟨⟨_, S.leftHomologyData.hi⟩⟩⟩

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.hi, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- 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
inst_3 : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
⊢ HasColimit (parallelPair h.f' 0)

Tactic:
haveI : HasColimit (parallelPair h.f' 0) := ⟨⟨⟨_, h.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 : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
inst_3 : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ (parallelPair (Y := kernel S.g) (kernel.lift S.g S.f ⋯) 0).map WalkingParallelPairHom.right ≫
      Iso.hom (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi) =
    Iso.hom (Iso.refl ((parallelPair (Y := kernel S.g) (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair h.f' 0).map WalkingParallelPairHom.right

Tactic:
simp
-- 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
inst_3 : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
e : parallelPair (Y := kernel S.g) (kernel.lift S.g S.f ⋯) 0 ≅ parallelPair h.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (Y := kernel S.g) (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero))
    (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi) ⋯ ⋯
⊢ HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
hasColimit_of_iso e

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- 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
inst_3 : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
e : parallelPair (Y := kernel S.g) (kernel.lift S.g S.f ⋯) 0 ≅ parallelPair h.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (Y := kernel S.g) (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero))
    (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi) ⋯ ⋯
⊢ HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
exact hasColimit_of_iso e

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- 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₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (cyclesMap' φ h₁ h₂)

Tactic:
⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.Hom.τ₂, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.IsIso.mk, 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₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
refine_1 : (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0
refine_2 : cyclesMap' φ h₁ h₂ ≫ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ = 𝟙 h₁.K
refine_3 : h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ ≫ cyclesMap' φ h₁ h₂ = 𝟙 h₂.K
⊢ IsIso (cyclesMap' φ h₁ h₂)

Tactic:
refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩
-- 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₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0

Tactic:
simp only [assoc, ← cancel_mono φ.τ₃, zero_comp, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, h₂.wi]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyData.wi, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.ShortComplex.Hom.τ₃
-- 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₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' φ h₁ h₂ ≫ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ = 𝟙 h₁.K

Tactic:
simp only [← cancel_mono h₁.i, assoc, h₁.liftK_i, cyclesMap'_i_assoc,
      IsIso.hom_inv_id, comp_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.cyclesMap'_i_assoc, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.ShortComplex.LeftHomologyData.i, CategoryTheory.Category.id_comp
-- 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₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ ≫ cyclesMap' φ h₁ h₂ = 𝟙 h₂.K

Tactic:
simp only [← cancel_mono h₂.i, assoc, cyclesMap'_i, h₁.liftK_i_assoc,
      IsIso.inv_hom_id, comp_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i_assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.cyclesMap'_i, CategoryTheory.ShortComplex.LeftHomologyData.i, CategoryTheory.Category.id_comp
-- 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₂ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)

Tactic:
isIso_cyclesMap'_of_isIso_of_mono φ h₂ h₃ _ _

Premises used: CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso_of_mono, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : IsIso φ.τ₂
inst_3 : Mono φ.τ₃
inst_4 : S₁.HasLeftHomology
inst_5 : S₂.HasLeftHomology
⊢ IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)

Tactic:
isIso_cyclesMap_of_isIso_of_mono' φ inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.isIso_cyclesMap_of_isIso_of_mono'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)

Tactic:
have eq₁ := h₁.fac (π₁.mapCone s)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
⊢ ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)

Tactic:
have eq₂ := h₂.fac (π₂.mapCone s)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
⊢ ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) c.pt) j).f ≫ (c.π.app j).τ₂

Tactic:
have eq₁₂ := fun j => (c.π.app j).comm₁₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) c.pt) j).f ≫ (c.π.app j).τ₂
⊢ ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) s.pt) j).f ≫ (s.π.app j).τ₂

Tactic:
have eq₁₂' := fun j => (s.π.app j).comm₁₂