-- 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
h :
  Cochain.v (δ (-1) 0 (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1))) n n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
h₁ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯
h₂ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    (limitSequence (X := X) φ hφ x₀).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (limitSequence (X := X) φ hφ x₀).v (n + 1) n ⋯
h₃ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (limitSequence (X := X) φ hφ x₀).v (n + 1) n ⋯
h₄ h₅ :
  (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯ =
    (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 •
        K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence (X := X) φ x₀ k₀) : Cochain K L (-1)).v (n + 1) n ⋯
⊢ (Cochain.ofHom f).v n n ⋯ = Cochain.v (δ (-1) 0 (limitSequence (X := X) φ hφ x₀)) n n ⋯

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)]

Premises used: CochainComplex.HomComplex.Cochain.InductionUp.limitSequence_eqUpTo, CochainComplex.HomComplex.δ_v, HSub.hSub, neg_add_cancel, HAdd.hAdd, CochainComplex.HomComplex.Cochain.InductionUp.sequence, add_zero, OfNat.ofNat, Neg.neg, rfl, Subtype.property