awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
hval :
  HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1)) fun (i : ℕ) ↦
    β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (i + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (i + 1))
⊢ HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))
have h₁ : β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1) =
  ∑' (b : ℕ), β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (b + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1))
Tactic: convert! (hS.mul_left β).hasSum using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
hval :
  HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1) =
    ∑' (b : ℕ), β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (b + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1))
have h : β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1) =
  β * ∑' (x : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (x + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (x + 1)
Tactic: rw [tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
x : Fin 2 → ℤ
⊢ ‖x‖ = (↑(max (x 0).natAbs (x 1).natAbs) : ℝ)
have rw : ‖x‖₊ = max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal)
Tactic: rw [← coe_nnnorm, ← NNReal.coe_natCast, NNReal.coe_inj, Nat.cast_max]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
x : Fin 2 → ℤ
⊢ ‖x‖₊ = max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal)
have refine : ∀ (c : NNReal), ‖x‖₊ ≤ c ↔ max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal) ≤ c
Tactic: refine eq_of_forall_ge_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
m n : ℤ
⊢ (↑|n| : ℝ) ≤ ‖![n, m]‖
have simp : LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|n| : ℝ) (↑m.natAbs : ℝ)
Tactic: simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|n| : ℝ) (↑m.natAbs : ℝ)
have h : LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ)
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ)
have h : LE.le (α := ℝ) (↑(↑n.natAbs : ℤ) : ℝ) (↑n.natAbs : ℝ)
Tactic: rw [Int.abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
m n : ℤ
⊢ (↑|m| : ℝ) ≤ ‖![n, m]‖
have simp : LE.le (α := ℝ) (↑|m| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)
Tactic: simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑|m| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)
have h : LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)
have h : LE.le (α := ℝ) (↑(↑m.natAbs : ℤ) : ℝ) (↑m.natAbs : ℝ)
Tactic: rw [Int.abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
n : ℕ
⊢ ‖![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have simp : (↑(max (Int.natAbs 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
n : ℕ
⊢ (↑(max (Int.natAbs 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have norm_cast : max 1 (n + 1) = n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
n : ℕ
⊢ ‖![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have simp : (↑(max (Int.natAbs 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
n : ℕ
⊢ (↑(max (Int.natAbs 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have norm_cast : max 1 (Int.negSucc n).natAbs = n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
⊢ r1 z = 1 / (HPow.hPow (β := ℕ) (z.re / z.im) 2 + 1)
have rw : r1 z = 1 / (HPow.hPow (β := ℕ) z.re 2 / HPow.hPow (β := ℕ) z.im 2 + 1)
Tactic: rw [div_pow, div_add_one (by positivity), one_div_div, r1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
rw : r1 z = 1 / (HPow.hPow (β := ℕ) z.re 2 / HPow.hPow (β := ℕ) z.im 2 + 1)
⊢ r1 z = 1 / (HPow.hPow (β := ℕ) (z.re / z.im) 2 + 1)
have rw₁ : r1 z = 1 / ((HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) / HPow.hPow (β := ℕ) z.im 2)
Tactic: rw [div_pow, div_add_one (by positivity), one_div_div, r1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
rw : r1 z = 1 / (HPow.hPow (β := ℕ) z.re 2 / HPow.hPow (β := ℕ) z.im 2 + 1)
rw₁ : r1 z = 1 / ((HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) / HPow.hPow (β := ℕ) z.im 2)
⊢ r1 z = 1 / (HPow.hPow (β := ℕ) (z.re / z.im) 2 + 1)
have rw₂ : r1 z = HPow.hPow (β := ℕ) z.im 2 / (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
Tactic: rw [div_pow, div_add_one (by positivity), one_div_div, r1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
rw : r1 z = 1 / (HPow.hPow (β := ℕ) z.re 2 / HPow.hPow (β := ℕ) z.im 2 + 1)
rw₁ : r1 z = 1 / ((HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) / HPow.hPow (β := ℕ) z.im 2)
rw₂ : r1 z = HPow.hPow (β := ℕ) z.im 2 / (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
⊢ r1 z = 1 / (HPow.hPow (β := ℕ) (z.re / z.im) 2 + 1)
have rw₃ : HPow.hPow (β := ℕ) z.im 2 / (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) =
  HPow.hPow (β := ℕ) z.im 2 / (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)
Tactic: rw [div_pow, div_add_one (by positivity), one_div_div, r1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
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
have H1 : HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2 =
  HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * 2 * c * z.re +
    HPow.hPow (β := ℕ) d 2
Tactic: have H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 =
    c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2 := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
H1 :
  HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2 =
    HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * 2 * c * z.re +
      HPow.hPow (β := ℕ) d 2
⊢ r1 z ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2
have H2 : (HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * 2 * c * z.re +
        HPow.hPow (β := ℕ) d 2) *
      (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) -
    HPow.hPow (β := ℕ) z.im 2 =
  HPow.hPow (β := ℕ) (c * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * z.re) 2 +
    (HPow.hPow (β := ℕ) d 2 - 1) * HPow.hPow (β := ℕ) z.im 2
Tactic: have H2 : (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2)
    - z.im ^ 2 = (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2 := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
H1 :
  HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2 =
    HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * 2 * c * z.re +
      HPow.hPow (β := ℕ) d 2
H2 :
  (HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * 2 * c * z.re +
          HPow.hPow (β := ℕ) d 2) *
        (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) -
      HPow.hPow (β := ℕ) z.im 2 =
    HPow.hPow (β := ℕ) (c * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * z.re) 2 +
      (HPow.hPow (β := ℕ) d 2 - 1) * HPow.hPow (β := ℕ) z.im 2
⊢ r1 z ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2
have rw : 0 ≤
  HPow.hPow (β := ℕ) (c * (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2) + d * z.re) 2 +
    (HPow.hPow (β := ℕ) d 2 - 1) * HPow.hPow (β := ℕ) z.im 2
Tactic: rw [r1, H1, div_le_iff₀ (by positivity), ← sub_nonneg, H2]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ } ≤ r z
have apply : √(r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }) ≤ √(r1 z)
Tactic: apply min_le_min hz.2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ √(r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }) ≤ √(r1 z)
have a : r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ } ≤ r1 z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ } ≤ r1 z
have a : (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: simp only [r1_eq, div_pow, one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ (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)⁻¹
have 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
Tactic: rw [inv_le_inv₀ (by positivity) (by positivity), add_le_add_iff_right, ← even_two.pow_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 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
have a : |z.re| ≤ { coe := { re := A, im := B }, coe_im_pos := h }.re
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ 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
have a₁ : { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }.im ≤ z.im
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
⊢ r z ≤ ‖(↑c : ℂ) * (↑z : ℂ) + (↑d : ℂ)‖
have rcases : ∀ (z : ℂ) (hz : 0 < z.im),
  r { coe := z, coe_im_pos := hz : ℍ } ≤ ‖(↑c : ℂ) * (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) + (↑d : ℂ)‖
Tactic: rcases z with ⟨z, hz⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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)
have rw : HPow.hPow (β := ℕ) z.im 2 ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) z.im 2
Tactic: rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
c d : ℝ
hc : 1 ≤ HPow.hPow (β := ℕ) c 2
z : ℂ
hz : 0 < z.im
⊢ r { coe := z, coe_im_pos := hz : ℍ } ≤ ‖(↑c : ℂ) * (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) + (↑d : ℂ)‖
have H1 : 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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
⊢ r z ≤ ‖(↑c : ℂ) * (↑z : ℂ) + (↑d : ℂ)‖
have H1 : √(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)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2 ∨ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2
have refine_1 : ∀ (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2
Tactic: refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2 ∨ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2
have refine_2 : ∀ (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2
Tactic: refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0
have rwa : ∀ (hx : ‖x‖ ≠ 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 0 ≠ 0
have 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
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 0 ≠ 0
have rwa₂ : ∀ (hx : Ne (α := ℝ) (↑(x 0).natAbs : ℝ) 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 0 ≠ 0
have rwa₃ : ∀ (hx : (x 0).natAbs ≠ 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 0 ≠ 0
have rwa₄ : ∀ (hx : x 0 ≠ 0) (H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs), x 0 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0
have rwa : ∀ (hx : ‖x‖ ≠ 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 1 ≠ 0
have 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
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 1 ≠ 0
have rwa₂ : ∀ (hx : Ne (α := ℝ) (↑(x 1).natAbs : ℝ) 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 1 ≠ 0
have rwa₃ : ∀ (hx : (x 1).natAbs ≠ 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
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
⊢ x 1 ≠ 0
have rwa₄ : ∀ (hx : x 1 ≠ 0) (H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs), x 1 ≠ 0
Tactic: rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
Cleared hypotheses: hx, H1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ r z * ‖x‖ ≤ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖
have hn0 : ‖x‖ ≠ 0
Tactic: have hn0 : ‖x‖ ≠ 0 := by rwa [norm_ne_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
have rw : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = ((↑(x 0) : ℂ) * (↑z : ℂ) / (↑‖x‖ : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
Tactic: rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]