awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
⊢ Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
have this : ∀ (h_sum : Summable (α := ℝ) fun (n : ℕ) ↦ (1 / 2) ^ (n + 1))
  (hab : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℂ) ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 (0 k)))
  (h_bound : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖-n ^ (k + 1)‖ ≤ (1 / 2) ^ (k + 1)),
  Tendsto (β := ℂ) (fun (n : ℂ) ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 (∏' (k : ℕ), HAdd.hAdd (α := ℂ) 1 (0 k)))
Tactic: have := tendsto_tprod_one_add_of_dominated_convergence (𝓕 := 𝓝 0) (g := 0)
      (f := fun (q : ℂ) (n : ℕ) ↦ -q ^ (n + 1)) (bound := fun n ↦ (1 / 2 : ℝ) ^ (n + 1))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
this :
  ∀ (h_sum : Summable (α := ℝ) fun (n : ℕ) ↦ (1 / 2) ^ (n + 1))
    (hab : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℂ) ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 (0 k)))
    (h_bound : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖-n ^ (k + 1)‖ ≤ (1 / 2) ^ (k + 1)),
    Tendsto (β := ℂ) (fun (n : ℂ) ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 (∏' (k : ℕ), HAdd.hAdd (α := ℂ) 1 (0 k)))
⊢ Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
have this₁ : ∀ (h_sum : Summable (α := ℝ) fun (n : ℕ) ↦ (1 / 2) ^ (n + 1))
  (hab : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℂ) ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0))
  (h_bound : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)),
  Tendsto (β := ℂ) (fun (n : ℂ) ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
Tactic: simp only [Pi.zero_apply, norm_neg, norm_pow, add_zero, tprod_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
this :
  ∀ (h_sum : Summable (α := ℝ) fun (n : ℕ) ↦ (1 / 2) ^ (n + 1))
    (hab : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℂ) ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0))
    (h_bound : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)),
    Tendsto (β := ℂ) (fun (n : ℂ) ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) (𝓝 0) (𝓝 1)
have refine : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
Tactic: refine this
      (by simpa only [pow_succ'] using (summable_geometric_of_abs_lt_one (by norm_num)).mul_left _)
      (fun k ↦ by simpa using ((continuous_pow (M := ℂ) (k + 1)).tendsto 0).neg) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
this :
  ∀ (h_sum : Summable (α := ℝ) fun (n : ℕ) ↦ (1 / 2) ^ (n + 1))
    (hab : ∀ (k : ℕ), Tendsto (β := ℂ) (fun (x : ℂ) ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0))
    (h_bound : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)),
    Tendsto (β := ℂ) (fun (n : ℂ) ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
have h : ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 (1 / 2)) q) (k : ℕ), ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
Tactic: filter_upwards [Metric.ball_mem_nhds (0 : ℂ) (by norm_num : (0 : ℝ) < 1 / 2)] with q hq k
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
⊢ Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) atImInfty (𝓝 1)
have htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
Tactic: have htprod : Tendsto (fun q : ℂ ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1) := by
    have := tendsto_tprod_one_add_of_dominated_convergence (𝓕 := 𝓝 0) (g := 0)
      (f := fun (q : ℂ) (n : ℕ) ↦ -q ^ (n + 1)) (bound := fun n ↦ (1 / 2 : ℝ) ^ (n + 1))
    simp only [Pi.zero_apply, norm_neg, norm_pow, add_zero, tprod_one] at this
    simp_rw [sub_eq_add_neg]
    refine this
      (by simpa only [pow_succ'] using (summable_geometric_of_abs_lt_one (by norm_num)).mul_left _)
      (fun k ↦ by simpa using ((continuous_pow (M := ℂ) (k + 1)).tendsto 0).neg) ?_
    filter_upwards [Metric.ball_mem_nhds (0 : ℂ) (by norm_num : (0 : ℝ) < 1 / 2)] with q hq k
    exact pow_le_pow_left₀ (norm_nonneg _) (mem_ball_zero_iff.mp hq).le _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) atImInfty (𝓝 1)
have this : Tendsto
  (fun (x : ℍ) ↦
    HPow.hPow (α := ℂ) (β := ℕ) (((fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) ∘ fun (τ : ℍ) ↦ 𝕢 1 (↑τ : ℂ)) x) 24)
  atImInfty (𝓝 (HPow.hPow (α := ℂ) (β := ℕ) 1 24))
Tactic: have := (htprod.comp (UpperHalfPlane.qParam_tendsto_atImInfty zero_lt_one)).pow 24
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this :
  Tendsto
    (fun (x : ℍ) ↦
      HPow.hPow (α := ℂ) (β := ℕ) (((fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) ∘ fun (τ : ℍ) ↦ 𝕢 1 (↑τ : ℂ)) x) 24)
    atImInfty (𝓝 (HPow.hPow (α := ℂ) (β := ℕ) 1 24))
⊢ Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) atImInfty (𝓝 1)
have simp : ∀
  (this :
    Tendsto (β := ℂ)
      (fun (x : ℍ) ↦ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1))) 24)
      atImInfty (𝓝 1)),
  Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1)) 24)
    atImInfty (𝓝 1)
Tactic: simp only [Periodic.qParam, ofReal_one, div_one, comp_apply, one_pow, eta_q] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this :
  Tendsto (β := ℂ)
    (fun (x : ℍ) ↦ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1))) 24)
    atImInfty (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1)) 24)
    atImInfty (𝓝 1)
have h : ∀ (τ : ℍ),
  ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)) 24 =
    HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))) 24
Tactic: convert! this using 2 with τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this :
  Tendsto (β := ℂ)
    (fun (x : ℍ) ↦ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1))) 24)
    atImInfty (𝓝 1)
τ : ℍ
⊢ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)) 24 =
    HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))) 24
have h : Multipliable (α := ℂ) fun (n : ℕ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
Tactic: rw [Multipliable.tprod_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this :
  Tendsto (β := ℂ)
    (fun (x : ℍ) ↦ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1))) 24)
    atImInfty (𝓝 1)
τ : ℍ
⊢ Multipliable (α := ℂ) fun (n : ℕ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
have h : ∀ (b : ℕ), 1 - eta_q b (↑τ : ℂ) = 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1)
Tactic: apply (multipliableLocallyUniformlyOn_eta.multipliable τ.2).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
⊢ IsZeroAtImInfty Δ
have apply : Tendsto (β := ℂ) (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty (𝓝 0)
Tactic: apply Tendsto.congr (fun z ↦ (discriminant_eq_q_prod z).symm)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
⊢ Tendsto (β := ℂ) (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty
    (𝓝 0)
have rw : Tendsto (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty
  (𝓝 (HMul.hMul (α := ℂ) 0 1))
Tactic: rw [show (0 : ℂ) = 0 * 1 by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
⊢ Asymptotics.IsBigO (E := ℝ) atImInfty (fun (τ : ℍ) ↦ rexp (-2 * π * τ.im)) Δ
have refine : ∀ᶠ (x : ℍ) in atImInfty, ‖rexp (-2 * π * x.im)‖ ≤ 2 * ‖Δ x‖
Tactic: refine .of_bound 2 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
⊢ ∀ᶠ (x : ℍ) in atImInfty, ‖rexp (-2 * π * x.im)‖ ≤ 2 * ‖Δ x‖
have hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
Tactic: have hprod := tendsto_atImInfty_tprod_one_sub_eta_q_pow.eventually
    (Metric.ball_mem_nhds 1 (by norm_num : (0 : ℝ) < 1/2))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
⊢ ∀ᶠ (x : ℍ) in atImInfty, ‖rexp (-2 * π * x.im)‖ ≤ 2 * ‖Δ x‖
have h : ∀ (τ : ℍ) (hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2),
  ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖
Tactic: filter_upwards [hprod] with τ hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
⊢ ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖
have h : rexp (-2 * π * τ.im) ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
Tactic: rw [discriminant_eq_q_prod, norm_mul, Real.norm_of_nonneg (Real.exp_pos _).le]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
⊢ rexp (-2 * π * τ.im) ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
Tactic: have hq_norm : ‖𝕢 1 τ‖ = Real.exp (-2 * π * τ.im) := by simp [Periodic.qParam, Complex.norm_exp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
⊢ rexp (-2 * π * τ.im) ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have h : ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
Tactic: rw [← hq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
⊢ ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2
have rwa : ∀ (hτ : ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2)
  (hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)),
  ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2
Tactic: rwa [Complex.dist_eq] at hτ
Cleared hypotheses: hτ, hq_norm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
⊢ 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
have hsub : ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2
Tactic: have hsub : ‖∏' n, (1 - eta_q n τ) ^ 24 - 1‖ < 1 / 2 := by rwa [Complex.dist_eq] at hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
hsub : ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2
⊢ 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
have h1 : norm (E := ℂ) 1 - norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) ≤
  ‖HSub.hSub (α := ℂ) 1 (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)‖
Tactic: have h1 := norm_sub_norm_le 1 (∏' n, (1 - eta_q n τ) ^ 24)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
⊢ ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have hprod_bound : 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
Tactic: have hprod_bound : 1 / 2 ≤ ‖∏' n, (1 - eta_q n τ) ^ 24‖ := by
    have hsub : ‖∏' n, (1 - eta_q n τ) ^ 24 - 1‖ < 1 / 2 := by rwa [Complex.dist_eq] at hτ
    have h1 := norm_sub_norm_le 1 (∏' n, (1 - eta_q n τ) ^ 24)
    grind [norm_one, norm_sub_rev]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
hprod_bound : 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
⊢ ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have linarith : 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
  2 / 2 = 1
Tactic: linarith [norm_nonneg (𝕢 1 τ), mul_le_mul_of_nonneg_left hprod_bound (norm_nonneg (𝕢 1 τ))]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
hprod_bound : 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
linarith :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    2 / 2 = 1
⊢ ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have linarith₁ : 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
  HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [norm_nonneg (𝕢 1 τ), mul_le_mul_of_nonneg_left hprod_bound (norm_nonneg (𝕢 1 τ))]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
hprod_bound : 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
linarith :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    2 / 2 = 1
linarith₁ linarith₂ linarith₃ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have linarith₄ : 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
  GT.gt (α := ℝ) 2 0
Tactic: linarith [norm_nonneg (𝕢 1 τ), mul_le_mul_of_nonneg_left hprod_bound (norm_nonneg (𝕢 1 τ))]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
τ : ℍ
hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)
hprod_bound : 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)
linarith :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    2 / 2 = 1
linarith₁ linarith₂ linarith₃ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    GT.gt (α := ℝ) 2 0
linarith₅ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    2 / 2 = 1
linarith₆ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    GT.gt (α := ℝ) 2 0
linarith₈ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    2 / 2 = 1
linarith₉ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ :
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
    GT.gt (α := ℝ) 2 0
⊢ ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
have linarith₁₁ : 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) < ‖𝕢 1 (↑τ : ℂ)‖ →
  2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)) - ‖𝕢 1 (↑τ : ℂ)‖ +
      (1 * ‖𝕢 1 (↑τ : ℂ)‖ * HMul.hMul (α := ℝ) 1 1 -
        1 * ‖𝕢 1 (↑τ : ℂ)‖ * (2 * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))) =
    0
Tactic: linarith [norm_nonneg (𝕢 1 τ), mul_le_mul_of_nonneg_left hprod_bound (norm_nonneg (𝕢 1 τ))]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
⊢ cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q
have pos : ∀ (hq0 : q = 0), cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q
Tactic: by_cases hq0 : q = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
pos : ∀ (hq0 : q = 0), cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q
⊢ cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q
have neg : ∀ (hq0 : ¬q = 0), cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q
Tactic: by_cases hq0 : q = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq0 : ¬q = 0
⊢ cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q
have him : 0 < (Periodic.invQParam 1 q).im
Tactic: have him := Periodic.im_invQParam_pos_of_norm_lt_one one_pos
      (by simpa [dist_zero_right] using hq) hq0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (hypothesis)
Goal:
⊢ Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (1 : ℂ)
have hmem : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
Tactic: have hmem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) 1 := Metric.mem_ball_self one_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hmem : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
⊢ Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (1 : ℂ)
have calc : (PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0
Tactic: calc (qExpansion 1 Δ).coeff 1
      = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0 := by
        simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]
    _ = derivWithin (fun q ↦ q * ∏' i, (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) 0 :=
        derivWithin_congr discriminant_cuspFunction_eqOn (discriminant_cuspFunction_eqOn hmem)
    _ = 1 := by
        simp [derivWithin_fun_mul differentiableWithinAt_fun_id
          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
hmem : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
calc :
  (PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0
⊢ Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (1 : ℂ)
have calc₁ : Eq (α := ℂ) (derivWithin (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) (Metric.ball 0 1) 0) 1
Tactic: calc (qExpansion 1 Δ).coeff 1
      = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0 := by
        simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]
    _ = derivWithin (fun q ↦ q * ∏' i, (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) 0 :=
        derivWithin_congr discriminant_cuspFunction_eqOn (discriminant_cuspFunction_eqOn hmem)
    _ = 1 := by
        simp [derivWithin_fun_mul differentiableWithinAt_fun_id
          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
A : GL (Fin 2) ℝ
hA :
  Membership.mem (γ := outParam (Subgroup (GL (Fin 2) ℝ)))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) A
⊢ @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 A Δ = Δ
have obtain : ∀ (A : SL(2, ℤ)),
  @SlashAction.map (outParam ℤ) (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) A : GL (Fin 2) ℝ) Δ =
    Δ
Tactic: obtain ⟨A, rfl⟩ := hA
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Discriminant (goal)
Goal:
⊢ MDiff (⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ)
have rw : DifferentiableOn ℂ (F := ℂ) ((⇑{ toFun := Δ, slash_action_eq' := sorry } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))
  {z : ℂ | 0 < z.im}
Tactic: rw [UpperHalfPlane.mdifferentiable_iff]