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.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
inr :
  (α.v (n + 1) n ⋯ + 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) ⋯) =
    (Cochain.ofHom f).v (n + 1) (n + 1) hpq
⊢ Cochain.v (δ (-1) 0 (α + Cochain.single β (-1))) (n + 1) (n + 1) hpq = (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)]

Premises used: CochainComplex.HomComplex.δ_v, neg_add_cancel, HAdd.hAdd, OfNat.ofNat, CochainComplex.HomComplex.Cochain.add_v, Neg.neg, 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
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (α.v (n + 1) n ⋯ + 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) ⋯) =
    (Cochain.ofHom f).v (n + 1) (n + 1) hpq

Tactic:
simp [hβ, u]
-- 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
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)}
p q : ℤ
hpq : p + 0 = q
hp : p ≤ (↑0 : ℤ) + d - 1
⊢ q < d

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
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)
⊢ (↑n : ℤ) + d - 1 + 1 = (↑(n + 1) : ℤ) + d - 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
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 : ℤ)
dsimp :
  (↑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
⊢ (↑(φ k x) : Cochain K L (-1)).v p q hpq = (↑x : Cochain K L (-1)).v p q hpq

Tactic:
dsimp [φ]
-- 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
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 : ℤ)
⊢ p ≠ (↑k : ℤ) + d - 1 + 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
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
rw₁ rw₂ : Eq.{v_1 + 1} (α := K.X p ⟶ L.X q) 0 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

Tactic:
rw [add_eq_left, Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]

Premises used: add_eq_left, 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
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)), (↑(φ 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)]
-- 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
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)

Tactic:
⟨(Cochain.equivHomotopy f 0).symm ⟨limitSequence φ hφ x₀, ?_⟩⟩

Premises used: CochainComplex.HomComplex.Cochain.InductionUp.limitSequence, Nonempty.intro, CochainComplex.HomComplex.Cochain.equivHomotopy, Subtype.mk, Equiv.symm, OfNat.ofNat, DFunLike.coe
-- 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
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 : ℤ))
refine : Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀) + Cochain.ofHom 0
⊢ Nonempty.{v_1 + 1} (Homotopy f 0)

Tactic:
refine ⟨(Cochain.equivHomotopy f 0).symm ⟨limitSequence φ hφ x₀, ?_⟩⟩
-- 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
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 : ℤ))
rw : Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀)
⊢ Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀) + Cochain.ofHom 0

Tactic:
rw [Cochain.ofHom_zero, add_zero]

Premises used: CochainComplex.HomComplex.Cochain.ofHom_zero, add_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
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 : ℤ))
h : ∀ (n : ℤ), (Cochain.ofHom f).v n n ⋯ = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
⊢ Cochain.ofHom f = δ (-1) 0 (limitSequence (X := X) φ hφ x₀)

Tactic:
ext n
-- 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
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
⊢ n ≤ (↑k₀ : ℤ) + d - 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
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
⊢ n + 0 = 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
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
⊢ 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
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
⊢ 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
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
⊢ n ≤ d + (↑k₀ : ℤ)

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
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
⊢ 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
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
⊢ n + 1 ≤ d + (↑k₀ : ℤ)

Tactic:
lia