Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
⊢ Summable fun x_1 ↦
    (if
          ↑((Equiv.prodCongrLeft fun x ↦
                    { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                      right_inv := ⋯ })
                  (Prod.map some id x_1)).2 =
            l₀ then
        0
      else
        (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id x_1)).1 +
              1) *
            (↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id x_1)).2 -
                x) ^
              (-(↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id x_1)).1 +
                  2)) -
          Nat.rec
            (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id x_1)).2 ^
              (-2))
            (fun n n_ih ↦ 0)
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id x_1)).1) *
      (z - x) ^
        ((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id x_1)).1

Tactic:
refine (H₁.mul_of_nonneg H₂ (by intro; positivity) (by intro; positivity)).of_norm_bounded ?_

Goal state after:
case h₂
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
⊢ ∀ (i : ℕ × ↥L.lattice),
    ‖(if
              ↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id i)).2 =
                l₀ then
            0
          else
            (↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id i)).1 +
                  1) *
                (↑((Equiv.prodCongrLeft fun x ↦
                            { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                              right_inv := ⋯ })
                          (Prod.map some id i)).2 -
                    x) ^
                  (-(↑((Equiv.prodCongrLeft fun x ↦
                              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                                right_inv := ⋯ })
                            (Prod.map some id i)).1 +
                      2)) -
              Nat.rec
                (↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id i)).2 ^
                  (-2))
                (fun n n_ih ↦ 0)
                ((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id i)).1) *
          (z - x) ^
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id i)).1‖ ≤
      (↑i.1 + 2) * κ ^ (-↑i.1) * (‖↑i.2 - x‖ ^ (-3) * ‖z - x‖)