Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ ∑ x ∈ Finset.range (i + 1),
            ↑(i.choose x) *
                (∑ 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) *
              (∑ 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),
            (↑(i.choose x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (i - x + 1),
                (↑((i - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ 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) *
                        (∑ 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)) *
                  (∑ 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) *
            (∑ 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

Goal state after:
case neg.inl
L : PeriodPair
hi₁ : 2 < 7
hi₂ : ¬Odd 2
hi₃ : ¬2 = 0
hi₄ : ¬2 = 6
⊢ ∑ x ∈ Finset.range (2 + 1),
            ↑(Nat.choose 2 x) *
                (∑ 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) *
              (∑ 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 (2 + 1),
            (↑(Nat.choose 2 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (2 - x + 1),
                (↑((2 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ 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) *
                        (∑ 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)) *
                  (∑ 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 (2 + 1),
          (↑(Nat.choose 2 x) * if x = 0 then L.g₂ else 0) *
            (∑ 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 (2 + 1), (↑(Nat.choose 2 x) * if x = 0 then L.g₃ else 0) * ↑(if 2 - x = 6 then 6! else 0) =
    0

case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ ∑ x ∈ Finset.range (4 + 1),
            ↑(Nat.choose 4 x) *
                (∑ 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) *
              (∑ 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 (4 + 1),
            (↑(Nat.choose 4 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ 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) *
                        (∑ 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)) *
                  (∑ 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 (4 + 1),
          (↑(Nat.choose 4 x) * if x = 0 then L.g₂ else 0) *
            (∑ 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 (4 + 1), (↑(Nat.choose 4 x) * if x = 0 then L.g₃ else 0) * ↑(if 4 - x = 6 then 6! else 0) =
    0