-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ Eq (α := ℂ)
    (iteratedDeriv 6
      (fun (z : ℂ) ↦
        (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) * (℘'[L - 0] z * HPow.hPow (β := ℕ) z 3 - 2) -
              4 *
                ((℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) * (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1) *
                  (℘[L - 0] z * HPow.hPow (β := ℕ) z 2 + 1)) +
            L.g₂ * (℘[L - 0] z * HPow.hPow (β := ℕ) z 6 + HPow.hPow (β := ℕ) z 4) +
          L.g₃ * HPow.hPow (β := ℕ) z 6)
      0)
    0
have simp : HSub.hSub (α := ℂ)
        (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 6 1),
          (↑(Nat.choose 6 x) : ℂ) *
              HSub.hSub (α := ℂ)
                (∑ x_1 ∈ Finset.range (x + 1),
                  (↑(x.choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                    (↑(if x - x_1 = 3 then 3! else 0) : ℂ))
                (if x = 0 then 2 else 0) *
            HSub.hSub (α := ℂ)
              (∑ x_1 ∈ Finset.range (6 - x + 1),
                (↑((6 - x).choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                  (↑(if 6 - x - x_1 = 3 then 3! else 0) : ℂ))
              (if 6 - x = 0 then 2 else 0))
        (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 6 1),
          HMul.hMul (α := ℂ) (↑(Nat.choose 6 x) : ℂ) (if x = 0 then 4 else 0) *
            ∑ x_1 ∈ Finset.range (6 - x + 1),
              HMul.hMul (α := ℂ) (↑((6 - x).choose x_1) : ℂ)
                  (∑ x ∈ Finset.range (x_1 + 1),
                    (↑(x_1.choose x) : ℂ) *
                        HAdd.hAdd (α := ℂ)
                          (∑ x_2 ∈ Finset.range (x + 1),
                            ((↑(x.choose x_2) : ℂ) *
                                if x_2 = 0 then ℘[L - 0] 0 else (↑(x_2 + 1)! : ℂ) * L.sumInvPow 0 (x_2 + 2)) *
                              (↑(if x - x_2 = 2 then 2! else 0) : ℂ))
                          (if x = 0 then 1 else 0) *
                      HAdd.hAdd (α := ℂ)
                        (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                          ((↑((x_1 - x).choose x_2) : ℂ) *
                              if x_2 = 0 then ℘[L - 0] 0 else (↑(x_2 + 1)! : ℂ) * L.sumInvPow 0 (x_2 + 2)) *
                            (↑(if x_1 - x - x_2 = 2 then 2! else 0) : ℂ))
                        (if x_1 - x = 0 then 1 else 0)) *
                HAdd.hAdd (α := ℂ)
                  (∑ x_2 ∈ Finset.range (6 - x - x_1 + 1),
                    ((↑((6 - x - x_1).choose x_2) : ℂ) *
                        if x_2 = 0 then ℘[L - 0] 0 else (↑(x_2 + 1)! : ℂ) * L.sumInvPow 0 (x_2 + 2)) *
                      (↑(if 6 - x - x_1 - x_2 = 2 then 2! else 0) : ℂ))
                  (if 6 - x - x_1 = 0 then 1 else 0)) +
      ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 6 1),
        ((↑(Nat.choose 6 x) : ℂ) * if x = 0 then L.g₂ else 0) *
          HAdd.hAdd (α := ℂ)
            (∑ x_1 ∈ Finset.range (6 - x + 1),
              ((↑((6 - x).choose x_1) : ℂ) *
                  if x_1 = 0 then ℘[L - 0] 0 else (↑(x_1 + 1)! : ℂ) * L.sumInvPow 0 (x_1 + 2)) *
                (↑(if 6 - x - x_1 = 6 then 6! else 0) : ℂ))
            (↑(if 6 - x = 4 then 4! else 0) : ℂ) +
    ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 6 1),
      ((↑(Nat.choose 6 x) : ℂ) * if x = 0 then L.g₃ else 0) * (↑(if 6 - x = 6 then 6! else 0) : ℂ) =
  0
Tactic: simp (discharger := fun_prop) only [iteratedDeriv_fun_add, iteratedDeriv_fun_sub,
    iteratedDeriv_fun_mul, iteratedDeriv_const, iteratedDeriv_fun_pow_zero,
    iteratedDeriv_derivWeierstrassPExcept_self, iteratedDeriv_weierstrassPExcept_self]