awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
⊢ n + 1 + -1 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
⊢ n + 2 + -1 = n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
⊢ n ≤ n

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
⊢ Cochain.v (δ (-1) 0 α) n n ⋯ = (Cochain.ofHom f).v n n ⋯

Tactic:
have eq := hα n n (add_zero n) (by rfl)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
eq : Cochain.v (δ (-1) 0 α) n n ⋯ = (Cochain.ofHom f).v n n ⋯
⊢ n - 1 = n - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
eq : Cochain.v (δ (-1) 0 α) n n ⋯ = (Cochain.ofHom f).v n n ⋯
⊢ n + 1 = n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
eq : Cochain.v (δ (-1) 0 α) n n ⋯ = (Cochain.ofHom f).v n n ⋯
⊢ α.v n (n - 1) ⋯ ≫ L.d (n - 1) n + K.d n (n + 1) ≫ α.v (n + 1) n ⋯ = f.f n

Tactic:
simp only [δ_v (-1) 0 (neg_add_cancel 1) α n n (add_zero _) (n - 1) (n + 1)
      (by lia) (by lia), Int.negOnePow_zero, one_smul, Cochain.ofHom_v] at eq

Premises used: CochainComplex.HomComplex.δ_v, HSub.hSub, CochainComplex.HomComplex.Cochain.ofHom_v, one_smul, neg_add_cancel, HAdd.hAdd, Int.negOnePow_zero, add_zero, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
eq : α.v n (n - 1) ⋯ ≫ L.d (n - 1) n + K.d n (n + 1) ≫ α.v (n + 1) n ⋯ = f.f n
⊢ K.d n (n + 1) ≫ u = 0

Tactic:
simp only [u, comp_sub, HomologicalComplex.d_comp_d_assoc, zero_comp,
      ← f.comm, ← eq, add_comp, Category.assoc, L.d_comp_d, comp_zero, zero_add, sub_self]

Premises used: CategoryTheory.Category.assoc, sub_self, HomologicalComplex.d_comp_d_assoc, CategoryTheory.Limits.comp_zero, zero_add, CategoryTheory.Preadditive.add_comp, HomologicalComplex.d_comp_d, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
⊢ K.d n (n + 1) ≫ u = 0

Tactic:
have hu : K.d n (n + 1) ≫ u = 0 := by
    have eq := hα n n (add_zero n) (by rfl)
    simp only [δ_v (-1) 0 (neg_add_cancel 1) α n n (add_zero _) (n - 1) (n + 1)
      (by lia) (by lia), Int.negOnePow_zero, one_smul, Cochain.ofHom_v] at eq
    simp only [u, comp_sub, HomologicalComplex.d_comp_d_assoc, zero_comp,
      ← f.comm, ← eq, add_comp, Category.assoc, L.d_comp_d, comp_zero, zero_add, sub_self]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ (ComplexShape.up ℤ).prev (n + 1) = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
simp : n + 1 + 1 = n + 2
⊢ (ComplexShape.up ℤ).next (n + 1) = n + 2

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ n + 1 + 1 = n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact

Tactic:
rw [K.exactAt_iff' n (n + 1) (n + 2) (by simp) (by simp; lia)] at hK

Premises used: HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
hK₁ : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
⊢ Injective.{v_1, u_1} (L.X (n + 1))

Tactic:
rw [K.exactAt_iff' n (n + 1) (n + 2) (by simp) (by simp; lia)] at hK

Premises used: HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst_3 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
hK₁ : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst : Injective.{v_1, u_1} (L.X (n + 1))
⊢ let u := f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯;
  K.d n (n + 1) ≫ u = 0

Tactic:
rw [K.exactAt_iff' n (n + 1) (n + 2) (by simp) (by simp; lia)] at hK

Premises used: HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ ∃ (β : K.X (n + 2) ⟶ L.X (n + 1)), K.d (n + 1) (n + 2) ≫ β = u

Tactic:
⟨hK.descToInjective _ hu, hK.comp_descToInjective _ _⟩

Premises used: CategoryTheory.ShortComplex.Exact.comp_descToInjective, CategoryTheory.ShortComplex.Exact.descToInjective, Exists.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
obtain :
  ∀ (β : K.X (n + 2) ⟶ L.X (n + 1)) (hβ : K.d (n + 1) (n + 2) ≫ β = u),
    ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)

Tactic:
obtain ⟨β, hβ⟩ : ∃ (β : K.X (n + 2) ⟶ L.X (n + 1)), K.d (n + 1) (n + 2) ≫ β = u :=
    ⟨hK.descToInjective _ hu, hK.comp_descToInjective _ _⟩

Premises used: HAdd.hAdd, HomologicalComplex.X, OfNat.ofNat, HomologicalComplex.d
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)

Tactic:
⟨β, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
refine : Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single β (-1))) (Cochain.ofHom f) (n + 1)
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)

Tactic:
refine ⟨β, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p q : ℤ
hpq : p + 0 = q
hp : p ≤ n + 1
⊢ p = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p q : ℤ
hpq : p + 0 = q
hp : p ≤ n + 1
obtain : ∀ (hpq : p + 0 = p), Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p q hpq = (Cochain.ofHom f).v p q hpq

Tactic:
obtain rfl : p = q := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp : p ≤ n + 1
hpq : p + 0 = p
inl : ∀ (hp : p < n + 1), Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq
inr :
  ∀ (hp : n + 1 ≤ n + 1) (hpq : n + 1 + 0 = n + 1),
    Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq

Tactic:
obtain hp | rfl := hp.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp_1 : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ p + 0 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp_1 : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ p ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp_1 : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ p ≠ n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp_1 : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ p + 1 ≠ n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp_1 : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
inl :
  CategoryStruct.comp (Y := L.X (p - 1)) 0 (L.d (p - 1) p) +
      HSMul.hSMul (β := K.X p ⟶ L.X p) (Int.negOnePow 0) (CategoryStruct.comp (Y := K.X (p + 1)) (K.d p (p + 1)) 0) =
    0
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq

Tactic:
rw [δ_add, Cochain.add_v, hα p p (by lia) (by lia), add_eq_left,
      δ_v (-1) 0 (neg_add_cancel 1) _ p p hpq (p - 1) (p + 1) rfl rfl,
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia),
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]

Premises used: CochainComplex.HomComplex.δ_v, HSub.hSub, CochainComplex.HomComplex.δ_add, neg_add_cancel, add_eq_left, HAdd.hAdd, OfNat.ofNat, CochainComplex.HomComplex.Cochain.add_v, Neg.neg, rfl, CochainComplex.HomComplex.Cochain.single_v_eq_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp_1 : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ CategoryStruct.comp (Y := L.X (p - 1)) 0 (L.d (p - 1) p) +
      HSMul.hSMul (β := K.X p ⟶ L.X p) (Int.negOnePow 0) (CategoryStruct.comp (Y := K.X (p + 1)) (K.d p (p + 1)) 0) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ n + 1 + 0 = n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ n = n + 1 - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ n + 1 + 1 = n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst_2 : Injective.{v_1, u_1} (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ n + 1 ≠ n + 2

Tactic:
lia