awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
this :
  (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)
rw :
  1 -
        HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
          ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ) -
      1 =
    β * ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)

Tactic:
rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]

Premises used: tsum_pnat_eq_tsum_succ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
this :
  (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)
⊢ 1 -
        HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
          ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ) -
      1 =
    β * ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)

Tactic:
have hval : E hk τ - 1 = β * ∑' n : ℕ, (σ (k - 1) (n + 1)) * cexp (2 * π * I * τ) ^ (n + 1) := by
    have := q_expansion_bernoulli hk hk2 τ
    simp_rw [zpow_natCast] at this
    rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]
    ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
rw :
  HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))
⊢ HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ))

Tactic:
rw [hval]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
⊢ HasSum (α := ℂ)
    (fun (i : ℕ) ↦ β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (i + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (i + 1)))
    (∑' (b : ℕ), β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (b + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1)))

Tactic:
(hS.mul_left β).hasSum

Premises used: Summable.mul_left, Summable.hasSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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))
h₁ :
  β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1) =
    ∑' (b : ℕ), β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (b + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1))
⊢ HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))

Tactic:
convert! (hS.mul_left β).hasSum using 1

Premises used: Summable.mul_left, Summable.hasSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1)) fun (i : ℕ) ↦
    β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (i + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (i + 1))

Tactic:
grind [Periodic.qParam, ofReal_one, div_one]

Premises used: Function.Periodic.qParam, Complex.ofReal_one, div_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
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 h₁ :
  β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1) =
    β * ∑' (x : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (x + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (x + 1)
⊢ β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1) =
    ∑' (b : ℕ), β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (b + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1))

Tactic:
rw [tsum_mul_left]

Premises used: tsum_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)

Tactic:
simpa using E_qExpansion_coeff hk hk2 0

Premises used: EisensteinSeries.E_qExpansion_coeff, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : E hk = 0
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)

Tactic:
simp [h, qExpansion_zero]

Premises used: UpperHalfPlane.qExpansion_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
rw : ‖x‖₊ = max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal)
⊢ ‖x‖ = (↑(max (x 0).natAbs (x 1).natAbs) : ℝ)

Tactic:
rw [← coe_nnnorm, ← NNReal.coe_natCast, NNReal.coe_inj, Nat.cast_max]

Premises used: Nat.cast_max, NNReal.coe_natCast, coe_nnnorm, NNReal.coe_inj
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
⊢ ‖x‖₊ = max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal)

Tactic:
eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
refine : ∀ (c : NNReal), ‖x‖₊ ≤ c ↔ max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal) ≤ c
⊢ ‖x‖₊ = max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal)

Tactic:
refine eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x : Fin 2 → ℤ
c : NNReal
⊢ ‖x‖₊ ≤ c ↔ max (↑(x 0).natAbs : NNReal) (↑(x 1).natAbs : NNReal) ≤ c

Tactic:
simp only [pi_nnnorm_le_iff, Fin.forall_fin_two, max_le_iff, NNReal.natCast_natAbs]

Premises used: Fin.forall_fin_two, pi_nnnorm_le_iff, NNReal.natCast_natAbs, max_le_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
x y : ℤ
⊢ ‖![x, y]‖ = ‖![y, x]‖

Tactic:
simp [EisensteinSeries.norm_eq_max_natAbs, max_comm]

Premises used: EisensteinSeries.norm_eq_max_natAbs, max_comm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
simp : LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|n| : ℝ) (↑m.natAbs : ℝ)
⊢ (↑|n| : ℝ) ≤ ‖![n, m]‖

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]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, Nat.cast_max, EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_fin_one, Fin.isValue, le_sup_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
h : LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ)
⊢ LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|n| : ℝ) (↑m.natAbs : ℝ)

Tactic:
left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
h : LE.le (α := ℝ) (↑(↑n.natAbs : ℤ) : ℝ) (↑n.natAbs : ℝ)
⊢ LE.le (α := ℝ) (↑|n| : ℝ) (↑n.natAbs : ℝ)

Tactic:
rw [Int.abs_eq_natAbs]

Premises used: Int.abs_eq_natAbs
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑(↑n.natAbs : ℤ) : ℝ) (↑n.natAbs : ℝ)

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑(↑n.natAbs : ℤ) : ℝ) (↑n.natAbs : ℝ)

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
simp : LE.le (α := ℝ) (↑|m| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)
⊢ (↑|m| : ℝ) ≤ ‖![n, m]‖

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]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, Nat.cast_max, EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_fin_one, Fin.isValue, le_sup_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
h : LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)
⊢ LE.le (α := ℝ) (↑|m| : ℝ) (↑n.natAbs : ℝ) ∨ LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)

Tactic:
right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
h : LE.le (α := ℝ) (↑(↑m.natAbs : ℤ) : ℝ) (↑m.natAbs : ℝ)
⊢ LE.le (α := ℝ) (↑|m| : ℝ) (↑m.natAbs : ℝ)

Tactic:
rw [Int.abs_eq_natAbs]

Premises used: Int.abs_eq_natAbs
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑(↑m.natAbs : ℤ) : ℝ) (↑m.natAbs : ℝ)

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
m n : ℤ
⊢ LE.le (α := ℝ) (↑(↑m.natAbs : ℤ) : ℝ) (↑m.natAbs : ℝ)

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
n : ℕ
simp : (↑(max (Int.natAbs 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ‖![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ = 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]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_fin_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : max 1 (n + 1) = n + 1
⊢ (↑(max (Int.natAbs 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
n : ℕ
simp : (↑(max (Int.natAbs 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ‖![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ = 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]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_fin_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : max 1 (Int.negSucc n).natAbs = n + 1
⊢ (↑(max (Int.natAbs 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs) : ℝ) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
⊢ HPow.hPow (β := ℕ) z.im 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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)
rw₃ 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)
⊢ r1 z = 1 / (HPow.hPow (β := ℕ) (z.re / z.im) 2 + 1)

Tactic:
rw [div_pow, div_add_one (by positivity), one_div_div, r1]

Premises used: EisensteinSeries.r1, div_add_one, div_pow, one_div_div
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
⊢ 0 < HPow.hPow (β := ℕ) z.im 2 / (HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
⊢ 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:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
c d : ℝ
hd : 1 ≤ HPow.hPow (β := ℕ) d 2
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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
⊢ (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:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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
⊢ (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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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
⊢ 0 < HPow.hPow (β := ℕ) z.re 2 + HPow.hPow (β := ℕ) z.im 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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
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
⊢ r1 z ≤ HPow.hPow (β := ℕ) (c * z.re + d) 2 + HPow.hPow (β := ℕ) (c * z.im) 2

Tactic:
rw [r1, H1, div_le_iff₀ (by positivity), ← sub_nonneg, H2]

Premises used: div_le_iff₀, EisensteinSeries.r1, sub_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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
⊢ 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:
add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hd) (sq_nonneg _))

Premises used: Iff.mpr, mul_nonneg, add_nonneg, sq_nonneg, sub_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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
⊢ 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:
exact add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hd) (sq_nonneg _))

Premises used: Iff.mpr, mul_nonneg, add_nonneg, sq_nonneg, sub_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
⊢ 0 < r z

Tactic:
simp only [r, lt_min_iff, im_pos, Real.sqrt_pos, r1_pos, and_self]

Premises used: UpperHalfPlane.im_pos, and_self, EisensteinSeries.r, EisensteinSeries.r1_pos, Real.sqrt_pos, lt_min_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
apply : √(r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }) ≤ √(r1 z)
⊢ r { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ } ≤ r z

Tactic:
apply min_le_min hz.2

Premises used: And.right, min_le_min
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
a : r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ } ≤ r1 z
⊢ √(r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ }) ≤ √(r1 z)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
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)⁻¹
⊢ r1 { coe := { re := A, im := B : ℂ }, coe_im_pos := h : ℍ } ≤ r1 z

Tactic:
simp only [r1_eq, div_pow, one_div]

Premises used: EisensteinSeries.r1_eq, div_pow, one_div
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 <
    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

Tactic:
positivity