-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma r_mul_max_le {x : Fin 2 → ℤ} (hx : x ≠ 0) : r z * ‖x‖ ≤ ‖x 0 * (z : ℂ) + x 1‖

Proof state:
case h.inl
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 ≤ (↑(x 0) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖

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

Result:
no goals

Proof state:
case h.inr
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 ≤ (↑(x 1) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖

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

Result:
no goals

Proof state:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

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)]

Result:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Proof state:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ 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]

Result:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑((x 0).natAbs ⊔ (x 1).natAbs) ≤
    ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖ *
      ↑((x 0).natAbs ⊔ (x 1).natAbs)

Proof state:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Tactic:
have hn0 : ‖x‖ ≠ 0 := by rwa [norm_ne_zero_iff]

Result:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Proof state:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
rwa [norm_ne_zero_iff]

Result:
no goals

Proof state:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑((x 0).natAbs ⊔ (x 1).natAbs) ≤
    ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖ *
      ↑((x 0).natAbs ⊔ (x 1).natAbs)

Tactic:
gcongr

Result:
case h
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z ≤ ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖

Proof state:
case h
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z ≤ ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖

Tactic:
rcases div_max_sq_ge_one x hx with H1 | H2

Result:
case h.inl
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 ≤ (↑(x 0) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖

case h.inr
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 ≤ (↑(x 1) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑((x 0).natAbs ⊔ (x 1).natAbs)‖

Proof state:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ ↑(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)]

Result:
no goals