-- Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
Goal:
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
neg :
  ∀ (hi₁ : 2 < 7) (hi₂ : ¬Odd (α := ℕ) 2) (hi₃ : ¬Eq (α := ℕ) 2 0) (hi₄ : ¬Eq (α := ℕ) 2 6),
    HSub.hSub (α := ℂ)
            (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
              (↑(Nat.choose 2 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 (2 - x + 1),
                    (↑((2 - x).choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                      (↑(if 2 - x - x_1 = 3 then 3! else 0) : ℂ))
                  (if 2 - x = 0 then 2 else 0))
            (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
              HMul.hMul (α := ℂ) (↑(Nat.choose 2 x) : ℂ) (if x = 0 then 4 else 0) *
                ∑ x_1 ∈ Finset.range (2 - x + 1),
                  HMul.hMul (α := ℂ) (↑((2 - 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 (2 - x - x_1 + 1),
                        ((↑((2 - 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 2 - x - x_1 - x_2 = 2 then 2! else 0) : ℂ))
                      (if 2 - x - x_1 = 0 then 1 else 0)) +
          ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
            ((↑(Nat.choose 2 x) : ℂ) * if x = 0 then L.g₂ else 0) *
              HAdd.hAdd (α := ℂ)
                (∑ x_1 ∈ Finset.range (2 - x + 1),
                  ((↑((2 - x).choose x_1) : ℂ) *
                      if x_1 = 0 then ℘[L - 0] 0 else (↑(x_1 + 1)! : ℂ) * L.sumInvPow 0 (x_1 + 2)) *
                    (↑(if 2 - x - x_1 = 6 then 6! else 0) : ℂ))
                (↑(if 2 - x = 4 then 4! else 0) : ℂ) +
        ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
          ((↑(Nat.choose 2 x) : ℂ) * if x = 0 then L.g₃ else 0) * (↑(if 2 - x = 6 then 6! else 0) : ℂ) =
      0
neg₁ :
  ∀ (hi₁ : 4 < 7) (hi₂ : ¬Odd (α := ℕ) 4) (hi₃ : ¬Eq (α := ℕ) 4 0) (hi₄ : ¬Eq (α := ℕ) 4 6),
    HSub.hSub (α := ℂ)
            (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 4 1),
              (↑(Nat.choose 4 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 (4 - x + 1),
                    (↑((4 - x).choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                      (↑(if 4 - x - x_1 = 3 then 3! else 0) : ℂ))
                  (if 4 - x = 0 then 2 else 0))
            (∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 4 1),
              HMul.hMul (α := ℂ) (↑(Nat.choose 4 x) : ℂ) (if x = 0 then 4 else 0) *
                ∑ x_1 ∈ Finset.range (4 - x + 1),
                  HMul.hMul (α := ℂ) (↑((4 - 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 (4 - x - x_1 + 1),
                        ((↑((4 - 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 4 - x - x_1 - x_2 = 2 then 2! else 0) : ℂ))
                      (if 4 - x - x_1 = 0 then 1 else 0)) +
          ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 4 1),
            ((↑(Nat.choose 4 x) : ℂ) * if x = 0 then L.g₂ else 0) *
              HAdd.hAdd (α := ℂ)
                (∑ x_1 ∈ Finset.range (4 - x + 1),
                  ((↑((4 - x).choose x_1) : ℂ) *
                      if x_1 = 0 then ℘[L - 0] 0 else (↑(x_1 + 1)! : ℂ) * L.sumInvPow 0 (x_1 + 2)) *
                    (↑(if 4 - x - x_1 = 6 then 6! else 0) : ℂ))
                (↑(if 4 - x = 4 then 4! else 0) : ℂ) +
        ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 4 1),
          ((↑(Nat.choose 4 x) : ℂ) * if x = 0 then L.g₃ else 0) * (↑(if 4 - x = 6 then 6! else 0) : ℂ) =
      0
⊢ HSub.hSub (α := ℂ)
          (∑ x ∈ Finset.range (i + 1),
            (↑(i.choose 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 (i - x + 1),
                  (↑((i - x).choose x_1) : ℂ) * ((↑(x_1 + 2)! : ℂ) * L.sumInvPow 0 (x_1 + 3)) *
                    (↑(if i - x - x_1 = 3 then 3! else 0) : ℂ))
                (if i - x = 0 then 2 else 0))
          (∑ x ∈ Finset.range (i + 1),
            HMul.hMul (α := ℂ) (↑(i.choose x) : ℂ) (if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (i - x + 1),
                HMul.hMul (α := ℂ) (↑((i - 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 (i - x - x_1 + 1),
                      ((↑((i - 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 i - x - x_1 - x_2 = 2 then 2! else 0) : ℂ))
                    (if i - x - x_1 = 0 then 1 else 0)) +
        ∑ x ∈ Finset.range (i + 1),
          ((↑(i.choose x) : ℂ) * if x = 0 then L.g₂ else 0) *
            HAdd.hAdd (α := ℂ)
              (∑ x_1 ∈ Finset.range (i - x + 1),
                ((↑((i - x).choose x_1) : ℂ) *
                    if x_1 = 0 then ℘[L - 0] 0 else (↑(x_1 + 1)! : ℂ) * L.sumInvPow 0 (x_1 + 2)) *
                  (↑(if i - x - x_1 = 6 then 6! else 0) : ℂ))
              (↑(if i - x = 4 then 4! else 0) : ℂ) +
      ∑ x ∈ Finset.range (i + 1),
        ((↑(i.choose x) : ℂ) * if x = 0 then L.g₃ else 0) * (↑(if i - x = 6 then 6! else 0) : ℂ) =
    0

Tactic:
obtain rfl | rfl : i = 2 ∨ i = 4 := by grind

Premises used: rfl