-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
l₀ x : ℂ
i : ℕ
zero :
  FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x
        else
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 *
            (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0))
      0 =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ)
          (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(HAdd.hAdd (α := ℕ) 0 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) 0 (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
succ :
  ∀ (i : ℕ),
    FormalMultilinearSeries.coeff
        (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
          if i = 0 then ℘[L - l₀] x
          else
            HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 *
              (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0))
        (i + 1) =
      ∑' (l : ↥L.lattice),
        if (↑l : ℂ) = l₀ then 0
        else
          HSub.hSub (β := ℂ)
            (HAdd.hAdd (α := ℂ) (↑(i + 1) : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 1 + 2) : ℤ)))
            (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) (i + 1) (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)
⊢ FormalMultilinearSeries.coeff
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        if i = 0 then ℘[L - l₀] x
        else
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 *
            (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0))
      i =
    ∑' (l : ↥L.lattice),
      if (↑l : ℂ) = l₀ then 0
      else
        HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) ((↑l : ℂ) - x) (-(↑(i + 2) : ℤ)))
          (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) (↑l : ℂ) (-2)) 0 : ℂ)

Tactic:
cases i with
  | zero => simp [weierstrassPExcept, sub_sq_comm x, zpow_ofNat]
  | succ i =>
    split_ifs with hl₀
    · trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
      · rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]
        simp [add_assoc, one_add_one_eq_two]
      · rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
        · simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring
        · exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))
    · have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)
      simp [h₁, tsum_mul_left, sumInvPow, add_assoc,
        one_add_one_eq_two, ← zpow_natCast, -neg_add_rev]

Premises used: neg_add_rev, zpow_natCast, sub_self, add_assoc, HSub.hSub, sub_sq_comm, FormalMultilinearSeries.coeff_ofScalars, tsum_mul_left, Set.Finite.subset, one_add_one_eq_two, Nat.cast, zpow_ofNat, MulZeroClass.mul_zero, Subtype.ext_iff, HasSum.summable, summable_of_hasFiniteSupport, HPow.hPow, HAdd.hAdd, tsum, zpow_neg, tsum_ite_eq, PeriodPair.hasSum_sumInvPow, Summable.tsum_sub, OfNat.ofNat, Eq, Set.finite_singleton, Neg.neg, SummationFilter.unconditional, PeriodPair.sumInvPow, PeriodPair.weierstrassPExcept, ite