awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₂ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 + -k)
h₃ :
  (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * (HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₄ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₅ :
  HMul.hMul (α := ℝ) (↑8 : ℝ) (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₆ : HMul.hMul (α := ℝ) 8 (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₂ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 + -k)
h₃ :
  (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * (HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₄ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₅ :
  HMul.hMul (α := ℝ) (↑8 : ℝ) (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₆ :
  HMul.hMul (α := ℝ) 8 (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₇ : 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ LT.lt (α := ℝ) 1 (↑k : ℝ)
have norm_cast : 1 < k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c : ℂ) * z + (↑n : ℂ)) ^ k)⁻¹) fun (n : ℤ) ↦
    (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑k : ℝ))⁻¹
have lift : ∀ (k : ℕ) (hk : LE.le (α := ℤ) 2 (↑k : ℤ)),
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑c : ℂ) * z + (↑n : ℂ)) (↑k : ℤ))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹
Tactic: lift k to ℕ using by lia
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ LT.lt (α := ℝ) 1 (↑k : ℝ)
have norm_cast : 1 < k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ Summable (α := ℂ) fun (c : ℤ) ↦ (((↑c : ℂ) * z + (↑d : ℂ)) ^ k)⁻¹
have apply : IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑d : ℂ)) ^ k)⁻¹) fun (n : ℤ) ↦
  (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑k : ℝ))⁻¹
Tactic: apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑d : ℂ)) ^ k)⁻¹) fun (n : ℤ) ↦
    (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑k : ℝ))⁻¹
have lift : ∀ (k : ℕ) (hk : LE.le (α := ℤ) 2 (↑k : ℤ)),
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑n : ℂ) * z + (↑d : ℂ)) (↑k : ℤ))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹
Tactic: lift k to ℕ using (by lia)
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : LE.le (α := ℤ) 2 (↑k : ℤ)
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑n : ℂ) * z + (↑d : ℂ)) (↑k : ℤ))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹
have simp : IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ ((↑n : ℂ) * z + (↑d : ℂ))⁻¹ ^ k) fun (n : ℤ) ↦
  HPow.hPow (α := ℝ) |(↑n : ℝ)⁻¹| k
Tactic: simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
c₁ c₂ : ℤ
⊢ LT.lt (α := ℝ) 1 2
have norm_cast : LT.lt (α := ℕ) 1 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
c₁ c₂ : ℤ
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z - (↑n : ℂ)) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹
have apply : IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z - (↑n : ℂ)) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹)
  fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
Tactic: apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
c₁ c₂ : ℤ
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z + (↑n : ℂ) + 1) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹
have apply : IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z + (↑n : ℂ) + 1) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹)
  fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
Tactic: apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ LT.lt (α := ℝ) 1 2
have norm_cast : LT.lt (α := ℕ) 1 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹
have apply : IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
  fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
Tactic: apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
have simp : IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
  fun (n : ℤ) ↦ (HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ))⁻¹
Tactic: simp only [Real.rpow_two, abs_mul_abs_self, pow_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
a b : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite
    (fun (m : Fin 2 → ℤ) ↦ (HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹)
    fun (m : Fin 2 → ℤ) ↦ ‖![m 0 + a, m 1 + b]‖⁻¹
have rw : ∃ (c : ℝ),
  ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
    ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤ c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
Tactic: rw [Asymptotics.isBigO_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
z : ℍ
a b : ℤ
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
      ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
        c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
have h0 : z ∈ verticalStrip |z.re| z.im
Tactic: have h0 : z ∈ verticalStrip |z.re| (z.im) := by simp [mem_verticalStrip_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
      ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
        c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
have h : ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
  ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
    ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := sorry : ℍ }‖⁻¹ * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
Tactic: use ‖r ⟨⟨|z.re|, z.im⟩, z.2⟩‖⁻¹
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
⊢ ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
    ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
      ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
have h : ∀ (m : Fin 2 → ℤ),
  ‖(HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
    ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := sorry : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
Tactic: filter_upwards with m
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
    ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
have h : (r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := sorry : ℍ })⁻¹ * ‖![m 0 + a, m 1 + b]‖⁻¹ ≤
  ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := sorry : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
Tactic: apply le_trans (by simpa [Real.rpow_neg_one, add_assoc] using
    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
a b : ℤ
⊢ IsTheta (E := ℝ) (F := ℝ) cofinite (fun (m : Fin 2 → ℤ) ↦ ‖![m 0 + a, m 1 + b]‖⁻¹) fun (m : Fin 2 → ℤ) ↦ ‖m‖⁻¹
have this : ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]
Tactic: have (x : Fin 2 → ℤ) : ![x 0 + a, x 1 + b] = x + ![a, b] := List.ofFn_inj.mp rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
a b : ℤ
this : ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]
⊢ IsTheta (E := Fin (Nat.succ 0).succ → ℤ) (F := ℝ) cofinite (fun (x : Fin 2 → ℤ) ↦ x)
    fun (x : Fin (Nat.succ 0).succ → ℤ) ↦ ‖x‖
have rw : IsTheta (E := ℝ) (F := ℝ) cofinite (fun (x : Fin (Nat.succ 0).succ → ℤ) ↦ ‖x‖) fun (x : Fin (Nat.succ 0).succ → ℤ) ↦ ‖x‖
Tactic: rw [← isTheta_norm_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)
have norm_cast : 2 < k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (hypothesis)
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformly (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ eisensteinSeries a k x) Filter.atTop
have hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
Tactic: have hk' : (2 : ℝ) < k := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (hypothesis)
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
⊢ TendstoLocallyUniformly (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ eisensteinSeries a k x) Filter.atTop
have p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
Tactic: have p_sum : Summable fun x : gammaSet N 1 a ↦ ‖x.val‖ ^ (-k) :=
    mod_cast (summable_one_div_norm_rpow hk').subtype (gammaSet N 1 a)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
⊢ TendstoLocallyUniformly (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ eisensteinSeries a k x) Filter.atTop
have simp : ∀ (K : Set ℍ),
  IsCompact K →
    TendstoUniformlyOn (β := ℂ)
      (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
      (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K
Tactic: simp only [tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
⊢ TendstoUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K
have obtain : ∀ (A B : ℝ) (hB : 0 < B) (HABK : K ⊆ verticalStrip A B),
  TendstoUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K
Tactic: obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact hK
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ TendstoUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K
have refine : ∀ (p : (↑(gammaSet N 1 a) : Type)) (z : ℍ) (hz : z ∈ verticalStrip A B),
  ‖eisSummand k (↑p : Fin 2 → ℤ) z‖ ≤
    HPow.hPow (β := ℝ) (r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ }) (-(↑k : ℝ)) *
      ‖(↑p : Fin 2 → ℤ)‖ ^ (-k)
Tactic: refine (tendstoUniformlyOn_tsum (hu := p_sum.mul_left <| r ⟨⟨A, B⟩, hB⟩ ^ (-k : ℝ))
    (fun p z hz ↦ ?_)).mono HABK
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
      (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
    ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop {z : ℂ | 0 < z.im}
have rw : TendstoLocallyUniformlyOn (β := ℂ)
  (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
    (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
  ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop (UpperHalfPlane.coe '' Set.univ)
Tactic: rw [← upperHalfPlaneSet, ← range_coe, ← image_univ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
      (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
    ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop (UpperHalfPlane.coe '' Set.univ)
have apply : TendstoLocallyUniformlyOn (β := ℂ)
  (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
  (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop ⊤
Tactic: apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
apply :
  TendstoLocallyUniformlyOn (β := ℂ)
    (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
    (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop ⊤
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
      (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
    ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop (UpperHalfPlane.coe '' Set.univ)
have apply₁ : MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).symm : ℂ → ℍ)
  (IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).target ⊤
Tactic: apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
    (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop ⊤
have simp : TendstoLocallyUniformly (β := ℂ)
  (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
  (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop
Tactic: simp only [Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)
have rw : Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ)
  (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) (⇑f : (a : ℍ) → ℂ) τ :
    ℂ)
Tactic: rw [← congr_fun (slash_action_eqn f _ <| Γ.mem_strictPeriods_iff.mp hH) τ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this :
  HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
    h +ᵥ τ
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ)
    (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
        ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) (⇑f : (a : ℍ) → ℂ) τ :
      ℂ)
have simp_rw : (f : (a : ℍ) → ℂ) (h +ᵥ τ) =
  HMul.hMul (α := ℂ)
      ((σ ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h) : (a : ℂ) → ℂ)
          ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ) :
        ℂ)
      ((↑|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
                    ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)) :
                ℝ)| :
          ℂ) ^
        (k - 1)) *
    denom ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h) (↑τ : ℂ) ^ (-k)
Tactic: simp_rw [slash_def, this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ)
    (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
        ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) (⇑f : (a : ℍ) → ℂ) τ :
      ℂ)
have suffices : HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
  h +ᵥ τ
Tactic: suffices GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ by
    simp_rw [slash_def, this]
    simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
    h +ᵥ τ
have coe : (↑(HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ) :
    ℂ) =
  (↑(h +ᵥ τ) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) +ᵥ z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
have hH : HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) ∈ Subgroup.strictPeriods (Subgroup.map (mapGL ℝ) Γ(N))
Tactic: apply vAdd_apply_of_mem_strictPeriods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (ModularGroup.T ^ ((↑N : ℤ) * n) • z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
have rw : Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * n) : ℝ) z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: rw [modular_T_zpow_smul z (N * n)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ @SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k ModularGroup.S f z =
    f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (↑z : ℂ) ^ (-k)
have rw : f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ } *
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) ModularGroup.S))
        (↑z : ℂ) ^
      (-k) =
  f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ } * (↑z : ℂ) ^ (-k)
Tactic: rw [SL_slash_apply, modular_S_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
⊢ (∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) ↔
    ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
have mp : (∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) →
  ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
Tactic: constructor