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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
⊢ h.f' ≫ h.i = S.f

Tactic:
liftK_i _ _ _

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
⊢ h.f' ≫ h.π = 0

Tactic:
h.wπ

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.LeftHomologyData.wπ
-- 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₂
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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ 0 = (x ≫ h.f') ≫ h.π

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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : h.liftK k ⋯ ≫ h.π = (x ≫ h.f') ≫ h.π
⊢ h.liftK k ⋯ ≫ h.π = 0

Tactic:
rw [show 0 = (x ≫ h.f') ≫ h.π by 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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
e_a : h.liftK k ⋯ = x ≫ h.f'
⊢ h.liftK k ⋯ ≫ h.π = (x ≫ h.f') ≫ h.π

Tactic:
congr 1
-- 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₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ = x ≫ h.f'

Tactic:
simp only [← cancel_mono h.i, hx, liftK_i, assoc, f'_i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, 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 : h.K ⟶ A
hk : h.f' ≫ k = 0
⊢ h.π ≫ h.descH k hk = k

Tactic:
h.hπ.fac (CokernelCofork.ofπ k hk) WalkingParallelPair.one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.ShortComplex.LeftHomologyData.hπ, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Limits.CokernelCofork.ofπ
-- 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
hg : S.g = 0
rw : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) (𝟙 S.X₂ ≫ 0) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
rw [hg, 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hg : S.g = 0
⊢ h.i ≫ h.liftK (𝟙 S.X₂) ⋯ = 𝟙 h.K

Tactic:
simp only [← cancel_mono h.i, id_comp, assoc, liftK_i, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
rw : (h.f' ≫ 𝟙 h.K) ≫ h.i = 0 ≫ h.i
rw₁ : h.f' ≫ h.i = 0 ≫ h.i
rw₂ : S.f = 0 ≫ h.i
rw₃ : S.f = 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ h.f' ≫ 𝟙 h.K = 0

Tactic:
rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Limits.zero_comp, 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
hf : S.f = 0
have : ∀ (φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K) (hφ : Cofork.π (CokernelCofork.ofπ h.π ⋯) ≫ φ = 𝟙 h.K), IsIso h.π
⊢ IsIso h.π

Tactic:
have ⟨φ, hφ⟩ := CokernelCofork.IsColimit.desc' h.hπ' (𝟙 _)
    (by rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
rw : h.π ≫ φ ≫ h.π = h.π ≫ 𝟙 h.H
rw₁ : h.π = h.π ≫ 𝟙 h.H
rw₂ rw₃ : h.π = h.π
⊢ φ ≫ h.π = 𝟙 h.H

Tactic:
rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]

Premises used: CategoryTheory.Category.comp_id, 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 : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
hf : S.f = 0
φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K
hφ : h.π ≫ φ = 𝟙 h.K
⊢ IsIso h.π

Tactic:
exact ⟨φ, hφ, by rw [← cancel_epi h.π, reassoc_of% hφ, 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
h : S.LeftHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
rw : S.g = 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
rw [id_comp, hg]

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 : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ (ofIsColimitCokernelCofork S hg c hc).f' = S.f

Tactic:
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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
T : C
φ : T ⟶ S.X₂
⊢ φ ≫ S.g = 0

Tactic:
simp [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 : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
T : C
φ : T ⟶ S.X₂
rw : φ = φ ≫ (ofIsColimitCokernelCofork S hg c hc).i
⊢ (ofIsColimitCokernelCofork S hg c hc).liftK φ ⋯ = φ

Tactic:
rw [← cancel_mono (ofIsColimitCokernelCofork S hg c hc).i, liftK_i]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork, 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
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
T : C
φ : T ⟶ S.X₂
⊢ φ = φ ≫ (ofIsColimitCokernelCofork S hg c hc).i

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
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
dsimp :
  Eq (α := S.X₁ ⟶ S.X₂) (((hc.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ 𝟙 c.pt) ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
    (0 ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ S.X₂)
    (((hc.ofIsoLimit (Fork.ext (Iso.refl c.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ Fork.ι c) (0 ≫ Fork.ι c)

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
h : S.LeftHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ Eq (α := S.X₁ ⟶ S.X₂) (((hc.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ 𝟙 c.pt) ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
    (0 ≫ Fork.ι c : S.X₁ ⟶ S.X₂)

Tactic:
simp only [comp_id, zero_comp, Fork.IsLimit.lift_ι, Fork.ι_ofι, hf]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.Fork.ι_ofι
-- 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
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
dsimp :
  Eq (α := S.X₁ ⟶ S.X₂) ((hc.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
    (0 ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ S.X₂)
    ((hc.ofIsoLimit (Fork.ext (Iso.refl c.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ Fork.ι c) (0 ≫ Fork.ι c)

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
h : S.LeftHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ Eq (α := S.X₁ ⟶ S.X₂) ((hc.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ Fork.ι c : S.X₁ ⟶ S.X₂)
    (0 ≫ Fork.ι c : S.X₁ ⟶ S.X₂)

Tactic:
simp only [comp_id, zero_comp, Fork.IsLimit.lift_ι, Fork.ι_ofι, hf]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.Fork.ι_ofι
-- 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
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).f' ≫ (ofIsLimitKernelFork S hf c hc).i = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
rw₁ : S.f = 0 ≫ (ofIsLimitKernelFork S hf c hc).i
rw₂ : Eq (α := S.X₁ ⟶ S.X₂) 0 (0 ≫ (ofIsLimitKernelFork S hf c hc).i)
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0

Tactic:
rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, zero_comp]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, 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
h : S.LeftHomologyData
A : C
hf : S.f = 0
hg rw : S.g = 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
rw [id_comp, hg]

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
hf : S.f = 0
hg : S.g = 0
change : S.f ≫ 𝟙 S.X₂ = 0
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ S.X₂) ((KernelFork.IsLimit.ofId S.g hg).lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 S.X₂) 0

Tactic:
change S.f ≫ 𝟙 _ = 0

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.ShortComplex.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
h : S.LeftHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
simp only [hf, zero_comp]

Premises used: 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
hf : S.f = 0
hg : S.g = 0
rw : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0 ≫ (ofZeros S hf hg).i
rw₁ : (ofZeros S hf hg).f' ≫ (ofZeros S hf hg).i = 0
rw₂ : S.f = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ (ofZeros S hf hg).f' = 0

Tactic:
rw [← cancel_mono ((ofZeros S hf hg).i), zero_comp, f'_i, hf]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.ofZeros, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, 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
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
rw : eK.hom ≫ h.i ≫ S.g = 0
rw₁ : Eq (α := K' ⟶ S.X₃) (eK.hom ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K' ⟶ S.X₃) 0 0
⊢ (eK.hom ≫ h.i) ≫ S.g = 0

Tactic:
rw [assoc, h.wi, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.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
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ eK.hom ≫ Fork.ι (KernelFork.ofι h.i ⋯) = eK.hom ≫ h.i

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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ H')
    (IsLimit.lift (IsKernel.isoKernel S.g (eK.hom ≫ h.i) h.hi eK ⋯) (KernelFork.ofι S.f ⋯) ≫ eK.hom ≫ h.π ≫ eH.inv) 0

Tactic:
simp [IsKernel.isoKernel]

Premises used: CategoryTheory.Limits.IsKernel.isoKernel
-- 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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (parallelPair (X := (KernelFork.ofι S.f ⋯).pt) (h.hi.lift (KernelFork.ofι S.f ⋯)) 0).map WalkingParallelPairHom.left ≫
      eK.symm.hom =
    Iso.hom (Iso.refl S.X₁) ≫
      (parallelPair (X := (KernelFork.ofι S.f ⋯).pt) (Y := K')
            (IsLimit.lift (IsKernel.isoKernel S.g (eK.hom ≫ h.i) h.hi eK ⋯) (KernelFork.ofι S.f ⋯) :
              (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι (eK.hom ≫ h.i) ⋯).pt)
            (0 : (KernelFork.ofι S.f ⋯).pt ⟶ K')).map
        WalkingParallelPairHom.left

Tactic:
simp [IsKernel.isoKernel]

Premises used: CategoryTheory.Limits.IsKernel.isoKernel
-- 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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (parallelPair (X := (KernelFork.ofι S.f ⋯).pt) (h.hi.lift (KernelFork.ofι S.f ⋯)) 0).map
        WalkingParallelPairHom.right ≫
      eK.symm.hom =
    Iso.hom (Iso.refl S.X₁) ≫
      (parallelPair (X := (KernelFork.ofι S.f ⋯).pt) (Y := K')
            (IsLimit.lift (IsKernel.isoKernel S.g (eK.hom ≫ h.i) h.hi eK ⋯) (KernelFork.ofι S.f ⋯) :
              (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι (eK.hom ≫ h.i) ⋯).pt)
            (0 : (KernelFork.ofι S.f ⋯).pt ⟶ K')).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 S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ Cocone.pt (F :=
      parallelPair (X := (KernelFork.ofι S.f ⋯).pt) (Y := K')
        (IsLimit.lift (IsKernel.isoKernel S.g (eK.hom ≫ h.i) h.hi eK ⋯) (KernelFork.ofι S.f ⋯) :
          (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι (eK.hom ≫ h.i) ⋯).pt)
        (0 : (KernelFork.ofι S.f ⋯).pt ⟶ K'))
      (Functor.obj (Cocone.precompose (Iso.inv (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯)))
        (CokernelCofork.ofπ h.π ⋯)) ≅
    (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).pt

Tactic:
exact eH.symm

Premises used: CategoryTheory.Iso.symm
-- 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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ NatTrans.app
        (Cocone.ι
          (Functor.obj (Cocone.precompose (Iso.inv (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯)))
            (CokernelCofork.ofπ h.π ⋯)))
        WalkingParallelPair.zero ≫
      eH.symm.hom =
    (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).ι.app WalkingParallelPair.zero

Tactic:
simp [IsKernel.isoKernel]

Premises used: CategoryTheory.Limits.IsKernel.isoKernel
-- 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 K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ NatTrans.app
        (Cocone.ι
          (Functor.obj (Cocone.precompose (Iso.inv (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯)))
            (CokernelCofork.ofπ h.π ⋯)))
        WalkingParallelPair.one ≫
      eH.symm.hom =
    (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).ι.app WalkingParallelPair.one

Tactic:
simp [IsKernel.isoKernel]

Premises used: CategoryTheory.Limits.IsKernel.isoKernel
-- 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
⊢ S.HasLeftHomology

Tactic:
⟨Nonempty.intro h⟩

Premises used: Nonempty.intro, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
inst_2 : HasKernel S.g
inst_3 : HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ S.HasLeftHomology

Tactic:
HasLeftHomology.mk' (LeftHomologyData.ofHasKernelOfHasCokernel S)

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
inst_2 : HasCokernel f
⊢ HasLeftHomology (ShortComplex.mk (X₃ := Z) f 0 ⋯)

Tactic:
HasLeftHomology.mk' (LeftHomologyData.ofHasCokernel _ rfl)

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel, rfl, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
Y Z : C
g : Y ⟶ Z
X : C
inst_2 : HasKernel g
⊢ HasLeftHomology (ShortComplex.mk (X₁ := X) 0 g ⋯)

Tactic:
HasLeftHomology.mk' (LeftHomologyData.ofHasKernel _ rfl)

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel, rfl, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
X Y Z : C
⊢ HasLeftHomology.{v_1, u_1} (C := C) (ShortComplex.mk (X₁ := X) (X₂ := Y) (X₃ := Z) 0 0 ⋯)

Tactic:
HasLeftHomology.mk' (LeftHomologyData.ofZeros _ rfl rfl)

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.ofZeros, rfl, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
rw : ψ₁.φK ≫ h₂.i = ψ₂.φK ≫ h₂.i
rw₁ : h₁.i ≫ φ.τ₂ = ψ₂.φK ≫ h₂.i
rw₂ rw₃ : h₁.i ≫ φ.τ₂ = h₁.i ≫ φ.τ₂
⊢ ψ₁.φK = ψ₂.φK

Tactic:
rw [← cancel_mono h₂.i, commi, commi]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.LeftHomologyMapData.commi, 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
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ ψ₁.φK = ψ₂.φK

Tactic:
have hK : ψ₁.φK = ψ₂.φK := by rw [← cancel_mono h₂.i, commi, 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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
rw : h₁.π ≫ ψ₁.φH = h₁.π ≫ ψ₂.φH
rw₁ : ψ₁.φK ≫ h₂.π = h₁.π ≫ ψ₂.φH
rw₂ : ψ₁.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π
rw₃ rw₄ : ψ₂.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π
⊢ ψ₁.φH = ψ₂.φH

Tactic:
rw [← cancel_epi h₁.π, commπ, commπ, hK]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.commπ, 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
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ ψ₁.φH = ψ₂.φH

Tactic:
have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_epi h₁.π, commπ, commπ, hK]
-- 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₂
hK : ψ₁.φK = ψ₂.φK
hH : ψ₁.φH = ψ₂.φH
mk :
  ∀ (φ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),
    { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ : LeftHomologyMapData φ h₁ h₂ } = ψ₂
⊢ ψ₁ = ψ₂

Tactic:
cases ψ₁