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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
have : (hi : IsLimit (KernelFork.ofι i wi)) → S₂.LeftHomologyData
⊢ S₂.LeftHomologyData

Tactic:
have hi : IsLimit (KernelFork.ofι i wi) := KernelFork.IsLimit.ofι _ _
    (fun x hx => h.liftK (x ≫ inv φ.τ₂) (by rw [assoc, ← cancel_mono φ.τ₃, assoc,
      assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, hx, zero_comp]))
    (fun x hx => by simp [i]) (fun x hx b hb => by
      dsimp
      rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc,
        assoc, IsIso.inv_hom_id, comp_id, hb])
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
⊢ hi.lift (KernelFork.ofι S₂.f ⋯) ≫ Fork.ι (KernelFork.ofι i wi) = Fork.ι (KernelFork.ofι S₂.f ⋯)

Tactic:
have eq := @Fork.IsLimit.lift_ι _ _ _ _ _ _ _ ((KernelFork.ofι S₂.f S₂.zero)) hi
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
rw : (φ.τ₁ ≫ f') ≫ h.i = h.f' ≫ h.i
rw₁ : ((φ.τ₁ ≫ f') ≫ h.i) ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₂ : (φ.τ₁ ≫ f') ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
rw₃ : φ.τ₁ ≫ 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 ≫ φ.τ₂
⊢ φ.τ₁ ≫ f' = h.f'

Tactic:
rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, f'_i, φ.comm₁₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Hom.τ₂, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
⊢ φ.τ₁ ≫ f' = h.f'

Tactic:
have hf' : φ.τ₁ ≫ f' = h.f' := by
    have eq := @Fork.IsLimit.lift_ι _ _ _ _ _ _ _ ((KernelFork.ofι S₂.f S₂.zero)) hi
    simp only [Fork.ι_ofι] at eq
    rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
rw : φ.τ₁ ≫ f' ≫ h.π = φ.τ₁ ≫ 0
rw₁ : φ.τ₁ ≫ f' ≫ h.π = 0
rw₂ : h.f' ≫ h.π = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ h.H) 0 0
⊢ f' ≫ h.π = 0

Tactic:
rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]

Premises used: CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.f'_π, 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
⊢ f' ≫ h.π = 0

Tactic:
have wπ : f' ≫ h.π = 0 := by
    rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : (φ.τ₁ ≫ f') ≫ x = 0
rw₁ : φ.τ₁ ≫ f' ≫ x = 0
rw₂ : Eq (α := S₁.X₁ ⟶ Z') (φ.τ₁ ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ Z') 0 0
⊢ h.f' ≫ x = 0

Tactic:
rw [← hf', assoc, hx, 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
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
⊢ h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx = x

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
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
b : h.H ⟶ Z'
hb : h.π ≫ b = x
rw : h.π ≫ b = h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx
rw₁ : h.π ≫ b = x
rw₂ rw₃ : x = x
⊢ b = (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx

Tactic:
rw [← cancel_epi h.π, π_descH, hb]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_descH, CategoryTheory.ShortComplex.LeftHomologyData.π, 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
have : (hπ : IsColimit (CokernelCofork.ofπ h.π wπ)) → S₂.LeftHomologyData
⊢ S₂.LeftHomologyData

Tactic:
have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) := CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => h.descH x (by rw [← hf', assoc, hx, comp_zero]))
    (fun x hx => by simp) (fun x hx b hb => by rw [← cancel_epi h.π, π_descH, hb])
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
hπ : IsColimit (CokernelCofork.ofπ h.π wπ)
⊢ S₂.LeftHomologyData

Tactic:
exact ⟨h.K, h.H, i, h.π, wi, hi, wπ, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f') ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₁ : φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' ≫ (ofEpiOfIsIsoOfMono φ h).i = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₂ : φ.τ₁ ≫ S₂.f = h.f' ≫ (ofEpiOfIsIsoOfMono φ h).i
rw₃ : φ.τ₁ ≫ S₂.f = h.f' ≫ h.i ≫ φ.τ₂
rw₄ : φ.τ₁ ≫ S₂.f = S₁.f ≫ φ.τ₂
rw₅ rw₆ : S₁.f ≫ φ.τ₂ = S₁.f ≫ φ.τ₂
⊢ φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'

Tactic:
rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i,
    ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]

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.LeftHomologyData.ofEpiOfIsIsoOfMono_i, CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
rw : h.i ≫ inv φ.τ₂ ≫ S₁.g = 0
rw₁ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
rw₂ : (h.i ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₃ : h.i ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0
rw₄ : h.i ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0
rw₅ : h.i ≫ inv φ.τ₂ ≫ φ.τ₂ ≫ S₂.g = 0
rw₆ : h.i ≫ S₂.g = 0
rw₇ rw₈ : Eq.{v_1 + 1} (α := h.K ⟶ S₂.X₃) 0 0
⊢ i ≫ S₁.g = 0

Tactic:
rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
⊢ i ≫ S₁.g = 0

Tactic:
have wi : i ≫ S₁.g = 0 := by
    rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃,
      IsIso.inv_hom_id_assoc, h.wi]
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
rw : x ≫ φ.τ₂ ≫ S₂.g = 0
rw₁ : x ≫ S₁.g ≫ φ.τ₃ = 0
rw₂ : Eq (α := W' ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := W' ⟶ S₂.X₃) 0 0
⊢ (x ≫ φ.τ₂) ≫ S₂.g = 0

Tactic:
rw [assoc, φ.comm₂₃, reassoc_of% hx, 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ i = x

Tactic:
simp [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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W' : C
x : W' ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W' ⟶ h.K
hb : b ≫ i = x
rw : b ≫ h.i = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i
rw₁ :
  (b ≫ h.i) ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₂ :
  b ≫ h.i ≫ inv φ.τ₂ =
    ((fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i) ≫ inv φ.τ₂
rw₃ :
  b ≫ h.i ≫ inv φ.τ₂ = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₄ : x = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx ≫ h.i ≫ inv φ.τ₂
rw₅ : x = (x ≫ φ.τ₂) ≫ inv φ.τ₂
rw₆ : x = x ≫ φ.τ₂ ≫ inv φ.τ₂
rw₇ : x = x ≫ 𝟙 S₁.X₂
rw₈ rw₉ : x = x
⊢ b = (fun {W' : C} (x : W' ⟶ S₁.X₂) (hx : x ≫ S₁.g = 0) ↦ h.liftK (x ≫ φ.τ₂) ⋯) x hx

Tactic:
rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i_assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.inv, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
have : (hi : IsLimit (KernelFork.ofι i wi)) → S₁.LeftHomologyData
⊢ S₁.LeftHomologyData

Tactic:
have hi : IsLimit (KernelFork.ofι i wi) := KernelFork.IsLimit.ofι _ _
    (fun x hx => h.liftK (x ≫ φ.τ₂)
      (by rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]))
    (fun x hx => by simp [i])
    (fun x hx b hb => by rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_id, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
⊢ f' ≫ i = S₁.f

Tactic:
have hf' : f' ≫ i = S₁.f := Fork.IsLimit.lift_ι _
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
rw : f' ≫ h.i = (φ.τ₁ ≫ h.f') ≫ h.i
rw₁ : (f' ≫ h.i) ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₂ : f' ≫ h.i ≫ inv φ.τ₂ = ((φ.τ₁ ≫ h.f') ≫ h.i) ≫ inv φ.τ₂
rw₃ : f' ≫ h.i ≫ inv φ.τ₂ = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₄ : f' ≫ h.i ≫ inv φ.τ₂ = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₅ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₆ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
rw₇ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
rw₈ : S₁.f = S₁.f ≫ 𝟙 S₁.X₂
rw₉ rw₁₀ : S₁.f = S₁.f
⊢ f' = φ.τ₁ ≫ h.f'

Tactic:
rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.inv, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
⊢ f' = φ.τ₁ ≫ h.f'

Tactic:
have hf'' : f' = φ.τ₁ ≫ h.f' := by
    rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc,
      φ.comm₁₂_assoc, IsIso.hom_inv_id, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
⊢ f' ≫ h.π = 0

Tactic:
simp only [hf'', assoc, f'_π, comp_zero]

Premises used: CategoryTheory.Category.assoc, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
⊢ f' ≫ h.π = 0

Tactic:
have wπ : f' ≫ h.π = 0 := by simp only [hf'', assoc, f'_π, 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
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : φ.τ₁ ≫ h.f' ≫ x = φ.τ₁ ≫ 0
rw₁ : f' ≫ x = φ.τ₁ ≫ 0
rw₂ : Eq (α := S₁.X₁ ⟶ Z') 0 (φ.τ₁ ≫ 0)
rw₃ rw₄ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ Z') 0 0
⊢ h.f' ≫ x = 0

Tactic:
rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]

Premises used: CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.Limits.comp_zero, 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx_1 : f' ≫ x = 0
b : h.H ⟶ Z'
hx : h.π ≫ b = x
rw : h.π ≫ b = h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx_1
rw₁ : h.π ≫ b = x
rw₂ rw₃ : x = x
⊢ b = (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx_1

Tactic:
rw [← cancel_epi h.π, π_descH, hx]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_descH, CategoryTheory.ShortComplex.LeftHomologyData.π, 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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
have : (hπ : IsColimit (CokernelCofork.ofπ h.π wπ)) → S₁.LeftHomologyData
⊢ S₁.LeftHomologyData

Tactic:
have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) := CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => h.descH x (by rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]))
    (fun x hx => π_descH _ _ _)
    (fun x hx b hx => by rw [← cancel_epi h.π, π_descH, hx])
-- 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
hπ : IsColimit (CokernelCofork.ofπ h.π wπ)
⊢ S₁.LeftHomologyData

Tactic:
exact ⟨h.K, h.H, i, h.π, wi, hi, wπ, 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
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₃ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₄ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
rw₅ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
rw₆ : S₁.f = S₁.f ≫ 𝟙 S₁.X₂
rw₇ rw₈ : S₁.f = S₁.f
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'

Tactic:
rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_i, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono', 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₂
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'