awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
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
have eq : Cochain.v (δ (-1) 0 α) n n sorry = (Cochain.ofHom f).v n n sorry
Tactic: have eq := hα n n (add_zero n) (by rfl)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
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 ⋯
⊢ K.d n (n + 1) ≫ u = 0
have eq₁ : α.v n (n - 1) sorry ≫ L.d (n - 1) n + K.d n (n + 1) ≫ α.v (n + 1) n sorry = 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
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
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) ⋯
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)
have hu : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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 ℤ).next (n + 1) = n + 2
have simp : n + 1 + 1 = n + 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
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
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)
have hK₁ : (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
Cleared hypotheses: hK, inst_2, u, hu
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ ∃ (h : K.X (n + 2) ⟶ L.X (n + 1)), Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single h (-1))) (Cochain.ofHom f) (n + 1)
have 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)
Tactic: obtain ⟨β, hβ⟩ : ∃ (β : K.X (n + 2) ⟶ L.X (n + 1)), K.d (n + 1) (n + 2) ≫ β = u :=
    ⟨hK.descToInjective _ hu, hK.comp_descToInjective _ _⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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)
have refine : Cochain.EqUpTo (δ (-1) 0 (α + Cochain.single β (-1))) (Cochain.ofHom f) (n + 1)
Tactic: refine ⟨β, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p q hpq = (Cochain.ofHom f).v p q hpq
have obtain : ∀ (hpq : p + 0 = p), Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq
Tactic: obtain rfl : p = q := by lia
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq
have inl : ∀ (hp : p < n + 1), 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
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq
have 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
Tactic: obtain hp | rfl := hp.lt_or_eq
Cleared hypotheses: p, hp, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) p p hpq = (Cochain.ofHom f).v p p hpq
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
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
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq
have inr : (α.v (n + 1) n sorry + 0) ≫ L.d n (n + 1) +
    HSMul.hSMul (β := K.X (n + 1) ⟶ L.X (n + 1)) (Int.negOnePow 0)
      (K.d (n + 1) (n + 2) ≫ (α + Cochain.single β (-1)).v (n + 2) (n + 1) sorry) =
  (Cochain.ofHom f).v (n + 1) (n + 1) hpq
Tactic: rw [δ_v (-1) 0 (neg_add_cancel 1) _ (n + 1) (n + 1) (by lia) n (n + 2)
      (by lia) (by lia), Cochain.add_v,
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
k : ℕ
x : (↑(X k) : Type v_1)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + (↑k : ℤ)
⊢ (↑(φ k x) : Cochain K L (-1)).v p q hpq = (↑x : Cochain K L (-1)).v p q hpq
have dsimp : (↑x : Cochain K L (-1)).v p q hpq +
    Cochain.v
      (Cochain.single
        (sorry.choose (p := fun (h : K.X ((↑k : ℤ) + d - 1 + 2) ⟶ L.X ((↑k : ℤ) + d - 1 + 1)) ↦
          Cochain.EqUpTo (δ (-1) 0 ((↑x : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
            (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + d - 1)))
        (-1))
      p q hpq =
  (↑x : Cochain K L (-1)).v p q hpq
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
k : ℕ
x : (↑(X k) : Type v_1)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + (↑k : ℤ)
⊢ (↑x : Cochain K L (-1)).v p q hpq +
      Cochain.v
        (Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑k : ℤ) + d - 1 + 2) ⟶ L.X ((↑k : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑x : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + d - 1)))
          (-1))
        p q hpq =
    (↑x : Cochain K L (-1)).v p q hpq
have rw : Cochain.v
    (Cochain.single
      (sorry.choose (p := fun (h : K.X ((↑k : ℤ) + d - 1 + 2) ⟶ L.X ((↑k : ℤ) + d - 1 + 1)) ↦
        Cochain.EqUpTo (δ (-1) 0 ((↑x : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
          (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + d - 1)))
      (-1))
    p q hpq =
  0
Tactic: rw [add_eq_left, Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
k : ℕ
x : (↑(X k) : Type v_1)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + (↑k : ℤ)
rw :
  Cochain.v
      (Cochain.single
        (⋯.choose (p := fun (h : K.X ((↑k : ℤ) + d - 1 + 2) ⟶ L.X ((↑k : ℤ) + d - 1 + 1)) ↦
          Cochain.EqUpTo (δ (-1) 0 ((↑x : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
            (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + d - 1)))
        (-1))
      p q hpq =
    0
⊢ (↑x : Cochain K L (-1)).v p q hpq +
      Cochain.v
        (Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑k : ℤ) + d - 1 + 2) ⟶ L.X ((↑k : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑x : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 + d - 1)))
          (-1))
        p q hpq =
    (↑x : Cochain K L (-1)).v p q hpq
have rw₁ : Eq.{v_1 + 1} (α := K.X p ⟶ L.X q) 0 0
Tactic: rw [add_eq_left, Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
⊢ Nonempty.{v_1 + 1} (Homotopy f 0)
have hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
Tactic: have hφ (k : ℕ) (x : X k) : (φ k x).1.EqUpTo x.1 (d + k) := fun p q hpq hp => by
      dsimp [φ]
      rw [add_eq_left, Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
⊢ Nonempty.{v_1 + 1} (Homotopy f 0)
have refine : Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀) + Cochain.ofHom 0
Tactic: refine ⟨(Cochain.equivHomotopy f 0).symm ⟨limitSequence φ hφ x₀, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
⊢ Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀) + Cochain.ofHom 0
have rw : Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀)
Tactic: rw [Cochain.ofHom_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
⊢ Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀)
have h : ∀ (n : ℤ), (Cochain.ofHom f).v n n sorry = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n sorry
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KInjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : L.IsStrictlyGE d
inst_3 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
K : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : (n : ℕ) → Set (Cochain K L (-1)) :=
  fun (n : ℕ) ↦ {α : Cochain K L (-1) | Cochain.EqUpTo (δ (-1) 0 α) (Cochain.ofHom f) ((↑n : ℤ) + d - 1)}
x₀ : (↑(X 0) : Type v_1) := Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X 0) 0 ⋯
φ : (n : ℕ) → (α : (↑(X n) : Type v_1)) → (↑(X (n + 1)) : Type v_1) :=
  fun (n : ℕ) (α : (↑(X n) : Type v_1)) ↦
    Subtype.mk (p := fun (x : Cochain K L (-1)) ↦ x ∈ X (n + 1))
      ((↑α : Cochain K L (-1)) +
        Cochain.single
          (⋯.choose (p := fun (h : K.X ((↑n : ℤ) + d - 1 + 2) ⟶ L.X ((↑n : ℤ) + d - 1 + 1)) ↦
            Cochain.EqUpTo (δ (-1) 0 ((↑α : Cochain K L (-1)) + Cochain.single h (-1))) (Cochain.ofHom f)
              ((↑(n + 1) : ℤ) + d - 1)))
          (-1))
      ⋯
hφ : ∀ (k : ℕ) (x : (↑(X k) : Type v_1)), (↑(φ k x) : Cochain K L (-1)).EqUpTo (↑x : Cochain K L (-1)) (d + (↑k : ℤ))
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ (Cochain.ofHom f).v n n ⋯ = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
have h : Cochain.v (δ (-1) 0 (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1))) n n sorry =
  Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n sorry
Tactic: rw [← (sequence φ x₀ k₀).2 n n (add_zero n) (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ n (n - 1) (by lia) (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)]