awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 < HPow.hPow (β := ℕ) z.re 2 / HPow.hPow (β := ℕ) z.im 2 + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
a :
  HPow.hPow (β := ℕ) |z.re| 2 / HPow.hPow (β := ℕ) z.im 2 ≤
    HPow.hPow (β := ℕ) { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.re 2 /
      HPow.hPow (β := ℕ) { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.im 2
⊢ (HPow.hPow (β := ℕ) { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.re 2 /
          HPow.hPow (β := ℕ) { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.im 2 +
        1)⁻¹ ≤
    (HPow.hPow (β := ℕ) z.re 2 / HPow.hPow (β := ℕ) z.im 2 + 1)⁻¹

Tactic:
rw [inv_le_inv₀ (by positivity) (by positivity), add_le_add_iff_right, ← even_two.pow_abs]

Premises used: even_two, add_le_add_iff_right, Even.pow_abs, inv_le_inv₀
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
a : |z.re| ≤ { coe := { re := A, im := B }, coe_im_pos := h }.re
a₁ : { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.im ≤ z.im
⊢ HPow.hPow (β := ℕ) |z.re| 2 / HPow.hPow (β := ℕ) z.im 2 ≤
    HPow.hPow (β := ℕ) { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.re 2 /
      HPow.hPow (β := ℕ) { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.im 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ≤ { coe := { re := A, im := B }, coe_im_pos := h }.re

Tactic:
hz.1

Premises used: And.left, UpperHalfPlane.re
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.im ≤ z.im

Tactic:
hz.2

Premises used: UpperHalfPlane.im, And.right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ≤ { coe := { re := A, im := B }, coe_im_pos := h }.re

Tactic:
exacts [hz.1, hz.2]

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
rcases :
  ∀ (z : ℂ) (hz : 0 < z.im),
    r { coe := z, coe_im_pos := hz : ℍ } ≤ ‖(↑c : ℂ) * (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) + (↑d : ℂ)‖
⊢ r z ≤ ‖(↑c : ℂ) * (↑z : ℂ) + (↑d : ℂ)‖

Tactic:
rcases z with ⟨z, hz⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
z : ℂ
hz : 0 < z.im
rw :
  HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) z.im 2
⊢ z.im ≤ √(HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) ((↑c : ℂ) * z).im 2)

Tactic:
rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]

Premises used: Real.le_sqrt', Complex.im_ofReal_mul, mul_pow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
z : ℂ
hz : 0 < z.im
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) z.im 2

Tactic:
(le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)

Premises used: le_mul_of_one_le_left, sq_nonneg, LE.le.trans, le_add_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
z : ℂ
hz : 0 < z.im
⊢ HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) z.im 2

Tactic:
exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)

Premises used: le_mul_of_one_le_left, sq_nonneg, LE.le.trans, le_add_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
z : ℂ
hz : 0 < z.im
⊢ z.im ≤ √(HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) ((↑c : ℂ) * z).im 2)

Tactic:
have H1 : z.im ≤ √((c * z.re + d) ^ 2 + (c * z).im ^ 2) := by
    rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]
    exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
z : ℂ
hz : 0 < z.im
H1 : z.im ≤ √(HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) ((↑c : ℂ) * z).im 2)
⊢ r { coe := z, coe_im_pos := hz : ℍ } ≤ ‖(↑c : ℂ) * (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) + (↑d : ℂ)‖

Tactic:
simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ← pow_two, add_im, mul_im,
    coe_im, ofReal_im, zero_mul, add_zero, min_le_iff] using Or.inl H1

Premises used: Complex.mul_im, Complex.add_im, pow_two, EisensteinSeries.r, MulZeroClass.zero_mul, min_le_iff, Complex.add_re, Complex.norm_def, Or.inl, UpperHalfPlane.coe_re, Complex.ofReal_im, Complex.normSq_apply, add_zero, UpperHalfPlane.coe_im, Complex.re_ofReal_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
⊢ 0 ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
⊢ √(r1 z) ≤ √(HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2)

Tactic:
have H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2) :=
    (Real.sqrt_le_sqrt_iff (by positivity)).mpr (r1_aux_bound _ _ hd)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
H1 : √(r1 z) ≤ √(HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2)
⊢ r z ≤ ‖(↑c : ℂ) * (↑z : ℂ) + (↑d : ℂ)‖

Tactic:
simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ofReal_re, ← pow_two,
    add_im, im_ofReal_mul, coe_im, ofReal_im, add_zero, min_le_iff] using Or.inr H1

Premises used: Complex.add_im, pow_two, EisensteinSeries.r, min_le_iff, Complex.add_re, Complex.norm_def, Complex.im_ofReal_mul, Complex.ofReal_re, UpperHalfPlane.coe_re, Complex.ofReal_im, Complex.normSq_apply, add_zero, UpperHalfPlane.coe_im, Or.inr, Complex.re_ofReal_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2 ∨ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2

Tactic:
(max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)

Premises used: max_choice, Int.natAbs, Or.imp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
refine_1 : ∀ (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2
refine_2 : ∀ (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2 ∨ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2

Tactic:
refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)

Premises used: max_choice, Int.natAbs, Or.imp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
rwa : ∀ (hx : ‖x‖ ≠ 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
rwa₁ :
  ∀ (hx : Ne (α := ℝ) (↑(max (x 0).natAbs (x 1).natAbs) : ℝ) 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs),
    x 0 ≠ 0
rwa₂ : ∀ (hx : Ne (α := ℝ) (↑(x 0).natAbs : ℝ) 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
rwa₃ : ∀ (hx : (x 0).natAbs ≠ 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hx : x 0 ≠ 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
⊢ x 0 ≠ 0

Tactic:
rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Premises used: EisensteinSeries.norm_eq_max_natAbs, norm_ne_zero_iff, Int.natAbs_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0

Tactic:
have : x 0 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
this : x 0 ≠ 0
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2

Tactic:
simp only [norm_eq_max_natAbs, H0, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

Premises used: le_refl, Int.cast_abs, OfNat.ofNat_ne_zero, pow_eq_zero_iff, Nat.cast_natAbs, EisensteinSeries.norm_eq_max_natAbs, ne_eq, div_pow, Int.cast_eq_zero, sq_abs, not_false_eq_true, div_self
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
rwa : ∀ (hx : ‖x‖ ≠ 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
rwa₁ :
  ∀ (hx : Ne (α := ℝ) (↑(max (x 0).natAbs (x 1).natAbs) : ℝ) 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs),
    x 1 ≠ 0
rwa₂ : ∀ (hx : Ne (α := ℝ) (↑(x 1).natAbs : ℝ) 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
rwa₃ : ∀ (hx : (x 1).natAbs ≠ 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hx : x 1 ≠ 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
⊢ x 1 ≠ 0

Tactic:
rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Premises used: EisensteinSeries.norm_eq_max_natAbs, norm_ne_zero_iff, Int.natAbs_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0

Tactic:
have : x 1 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
this : x 1 ≠ 0
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2

Tactic:
simp only [norm_eq_max_natAbs, H1, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

Premises used: le_refl, Int.cast_abs, OfNat.ofNat_ne_zero, pow_eq_zero_iff, Nat.cast_natAbs, EisensteinSeries.norm_eq_max_natAbs, ne_eq, div_pow, Int.cast_eq_zero, sq_abs, not_false_eq_true, div_self
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
rwa rwa₁ rwa₂ rwa₃ : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
rwa [norm_ne_zero_iff]

Premises used: norm_ne_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
have hn0 : ‖x‖ ≠ 0 := by rwa [norm_ne_zero_iff]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
rw :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) * (↑z : ℂ) / (↑‖x‖ : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
rw₁ : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) / (↑‖x‖ : ℂ) * (↑‖x‖ : ℂ)
rw₂ rw₃ : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
⊢ (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)

Tactic:
rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]

Premises used: div_mul_cancel₀, div_mul_eq_mul_div, add_div
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)

Tactic:
have h11 : x 0 * (z : ℂ) + x 1 = (x 0 / ‖x‖ * z + x 1 / ‖x‖) * ‖x‖ := by
    rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
rw :
  r z * (↑(max (x 0).natAbs (x 1).natAbs) : ℝ) ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
          (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖ *
      (↑(max (x 0).natAbs (x 1).natAbs) : ℝ)
⊢ r z * ‖x‖ ≤ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖

Tactic:
rw [norm_eq_max_natAbs, h11, norm_mul, norm_real, norm_norm, norm_eq_max_natAbs]

Premises used: EisensteinSeries.norm_eq_max_natAbs, norm_mul, Complex.norm_real, norm_norm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
hbc :
  r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
⊢ r z * (↑(max (x 0).natAbs (x 1).natAbs) : ℝ) ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
          (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖ *
      (↑(max (x 0).natAbs (x 1).natAbs) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
hbc :
  ∀ (H1 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2),
    r z ≤
      ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
          (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
hbc₁ :
  ∀ (H2 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2),
    r z ≤
      ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
          (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
⊢ r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖

Tactic:
rcases div_max_sq_ge_one x hx with H1 | H2

Premises used: EisensteinSeries.div_max_sq_ge_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
H1 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2
⊢ r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖

Tactic:
simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1

Premises used: Norm.norm, Int.cast, Complex.ofReal_intCast, HDiv.hDiv, EisensteinSeries.norm_eq_max_natAbs, EisensteinSeries.auxbound1, Complex.ofReal_div, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
H2 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2
⊢ r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖

Tactic:
simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound2 z (x 0 / ‖x‖) H2

Premises used: Norm.norm, Int.cast, Complex.ofReal_intCast, HDiv.hDiv, EisensteinSeries.norm_eq_max_natAbs, EisensteinSeries.auxbound2, Complex.ofReal_div, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
pos : ∀ (hx : x = 0), ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
neg : ∀ (hx : ¬x = 0), ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
pos : HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]

Premises used: Int.cast_zero, MulZeroClass.zero_mul, norm_zero, Pi.zero_apply, add_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
pos : ∀ (h : -k = 0), HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
neg : ∀ (h : ¬-k = 0), HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)

Tactic:
by_cases h : -k = 0
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
pos : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (β := ℝ) (r z) 0 * HPow.hPow (α := ℝ) (β := ℝ) 0 0
pos₁ : 1 ≤ HPow.hPow (β := ℝ) (r z) 0 * 1
pos₂ : 1 ≤ HMul.hMul (α := ℝ) 1 1
pos₃ pos₄ : LE.le (α := ℝ) 1 1
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)

Tactic:
rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]

Premises used: Real.rpow_zero, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
neg : 0 ≤ r z ^ (-k) * 0
neg₁ neg₂ : LE.le (α := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)

Tactic:
rw [Real.zero_rpow h, mul_zero]

Premises used: Real.zero_rpow, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
neg : ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
rw [← Real.mul_rpow (r_pos _).le (norm_nonneg _)]

Premises used: EisensteinSeries.r_pos, Real.mul_rpow, LT.lt.le, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)

Tactic:
Real.rpow_le_rpow_of_nonpos (mul_pos (r_pos _) (norm_pos_iff.mpr hx)) (r_mul_max_le z hx)
      (neg_nonpos.mpr hk)

Premises used: Iff.mpr, norm_pos_iff, EisensteinSeries.r_pos, Real.rpow_le_rpow_of_nonpos, neg_nonpos, EisensteinSeries.r_mul_max_le, mul_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)

Tactic:
exact Real.rpow_le_rpow_of_nonpos (mul_pos (r_pos _) (norm_pos_iff.mpr hx)) (r_mul_max_le z hx)
      (neg_nonpos.mpr hk)

Premises used: Iff.mpr, norm_pos_iff, EisensteinSeries.r_pos, Real.rpow_le_rpow_of_nonpos, neg_nonpos, EisensteinSeries.r_mul_max_le, mul_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 ≤ ‖x‖ ^ (-k)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
refine : r z ^ (-k) ≤ r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-k)
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
refine (summand_bound z hk x).trans (mul_le_mul_of_nonneg_right ?_ (by positivity))

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, EisensteinSeries.summand_bound
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ r z ^ (-k) ≤ r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-k)

Tactic:
Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz)
    (neg_nonpos.mpr hk)

Premises used: Iff.mpr, EisensteinSeries.r_lower_bound_on_verticalStrip, EisensteinSeries.r_pos, Real.rpow_le_rpow_of_nonpos, neg_nonpos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ r z ^ (-k) ≤ r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-k)

Tactic:
exact Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz)
    (neg_nonpos.mpr hk)

Premises used: Iff.mpr, EisensteinSeries.r_lower_bound_on_verticalStrip, EisensteinSeries.r_pos, Real.rpow_le_rpow_of_nonpos, neg_nonpos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
ho : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
apply IsTheta.add_isLittleO

Premises used: Asymptotics.IsTheta.add_isLittleO
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real)

Premises used: Int.cast_complex_isTheta_cast_real, Asymptotics.IsLittleO.add_isTheta
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
hΘ : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real)

Premises used: Int.cast_complex_isTheta_cast_real, Asymptotics.IsLittleO.add_isTheta
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
hΘ : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
ho : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
apply IsTheta.add_isLittleO <;>
  [refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real); skip]

Premises used: Int.cast_complex_isTheta_cast_real, Asymptotics.IsLittleO.add_isTheta, Asymptotics.IsTheta.add_isLittleO
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
⊢ IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
simpa [-Int.cofinite_eq] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real

Premises used: Int.cofinite_eq, Int.isClosedEmbedding_coe_real, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
⊢ IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
simpa [-Int.cofinite_eq] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real

Premises used: Int.cofinite_eq, Int.isClosedEmbedding_coe_real, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding