awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
h :
  cexp (2 * (↑π : ℂ) * I * (1 + (↑z : ℂ))) *
      ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (1 + (↑z : ℂ))) ^ (n + 1)) 24 =
    cexp (2 * (↑π : ℂ) * I * (↑z : ℂ) + 2 * (↑π : ℂ) * I) *
      ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ) + 2 * (↑π : ℂ) * I) ^ (n + 1)) 24
⊢ Δ (HVAdd.hVAdd (α := ℝ) 1 z) *
      HPow.hPow (β := ℤ)
        ((↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
                          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, 1; 0, 1]
                            ModularGroup.T._proof_1))) :
                    Matrix (Fin 2) (Fin 2) ℝ)
                  1 0) :
              ℂ) *
            (↑z : ℂ) +
          (↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                      ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
                        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, 1; 0, 1]
                          ModularGroup.T._proof_1))) :
                  Matrix (Fin 2) (Fin 2) ℝ)
                1 1) :
            ℂ))
        (-12) =
    Δ z

Tactic:
simp [discriminant_eq_q_prod, eta_q, Periodic.qParam, ← exp_periodic (2 * π * I * z)]

Premises used: Function.Periodic.qParam, Real.pi, ModularForm.eta_q, HMul.hMul, UpperHalfPlane.coe, Complex.exp_periodic, ModularForm.discriminant_eq_q_prod, Complex.ofReal, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ cexp (2 * (↑π : ℂ) * I * (1 + (↑z : ℂ))) *
      ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (1 + (↑z : ℂ))) ^ (n + 1)) 24 =
    cexp (2 * (↑π : ℂ) * I * (↑z : ℂ) + 2 * (↑π : ℂ) * I) *
      ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ) + 2 * (↑π : ℂ) * I) ^ (n + 1)) 24

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
obtain :
  ∀ (z : ℂ) (hz : z ≠ 0) (h : Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet),
    Set.EqOn (η ∘ fun (x : ℂ) ↦ -1 / x) (I.sqrt⁻¹ • (sqrt * η)) upperHalfPlaneSet
⊢ Set.EqOn (η ∘ fun (x : ℂ) ↦ -1 / x) (I.sqrt⁻¹ • (sqrt * η)) upperHalfPlaneSet

Tactic:
obtain ⟨z, hz, h⟩ := eta_comp_eqOn_const_mul_csqrt_eta

Premises used: _private.0.ModularForm.eta_comp_eqOn_const_mul_csqrt_eta
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
⊢ I ∈ upperHalfPlaneSet

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
⊢ η I = z * I.sqrt * η I

Tactic:
simpa [← mul_assoc] using h (show I ∈ _ by simp)

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
⊢ η I = z * I.sqrt * η I

Tactic:
have h3 : η I = z * sqrt I * η I := by simpa [← mul_assoc] using h (show I ∈ _ by simp)
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
h3 : η I = z * I.sqrt * η I
⊢ 0 < I.im

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
h3 : η I = z * I.sqrt * η I
⊢ Set.EqOn (η ∘ fun (x : ℂ) ↦ -1 / x) (I.sqrt⁻¹ • (sqrt * η)) upperHalfPlaneSet

Tactic:
grind [sqrt, eta_ne_zero (show 0 < I.im by simp)]

Premises used: Complex.sqrt, ModularForm.eta_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
h :
  ∀ (z : ℍ),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.S Δ
        z =
      Δ z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.S Δ =
    Δ

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
this : HPow.hPow (β := ℕ) (η (-(↑z : ℂ)⁻¹)) 24 * (HPow.hPow (β := ℕ) (↑z : ℂ) 12)⁻¹ = HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24
rw :
  Δ { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } *
      HPow.hPow (β := ℤ)
        (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) ModularGroup.S))
          (↑z : ℂ))
        (-12) =
    Δ z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.S Δ
      z =
    Δ z

Tactic:
rw [SL_slash_apply, UpperHalfPlane.modular_S_smul]

Premises used: UpperHalfPlane.modular_S_smul, ModularForm.SL_slash_apply
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
this : HPow.hPow (β := ℕ) (η (-(↑z : ℂ)⁻¹)) 24 * (HPow.hPow (β := ℕ) (↑z : ℂ) 12)⁻¹ = HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24
⊢ Δ { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } *
      HPow.hPow (β := ℤ)
        (denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) ModularGroup.S))
          (↑z : ℂ))
        (-12) =
    Δ z

Tactic:
simpa [denom, ModularGroup.S]

Premises used: ModularGroup.S, UpperHalfPlane.denom
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
h : HPow.hPow (β := ℕ) (η (-(↑z : ℂ)⁻¹)) 24 * (HPow.hPow (β := ℕ) (↑z : ℂ) 12)⁻¹ = HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.S Δ
      z =
    Δ z

Tactic:
suffices η (-(↑z)⁻¹) ^ 24 * ((z : ℂ) ^ 12)⁻¹ = η z ^ 24 by
    rw [SL_slash_apply, UpperHalfPlane.modular_S_smul]
    simpa [denom, ModularGroup.S]
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ η (-(↑z : ℂ)⁻¹) = I.sqrt⁻¹ * ((↑z : ℂ).sqrt * η (↑z : ℂ))

Tactic:
simpa [neg_div] using eta_comp_eq_csqrt_I_inv z.2

Premises used: neg_div, ModularForm.eta_comp_eq_csqrt_I_inv, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ η (-(↑z : ℂ)⁻¹) = I.sqrt⁻¹ * ((↑z : ℂ).sqrt * η (↑z : ℂ))

Tactic:
have he : η (-(↑z)⁻¹) = (sqrt I)⁻¹ * (sqrt z * η z) := by
    simpa [neg_div] using eta_comp_eq_csqrt_I_inv z.2
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
he : η (-(↑z : ℂ)⁻¹) = I.sqrt⁻¹ * ((↑z : ℂ).sqrt * η (↑z : ℂ))
h :
  1⁻¹ * (HPow.hPow (β := ℕ) (↑z : ℂ) 12 * HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24) * (HPow.hPow (β := ℕ) (↑z : ℂ) 12)⁻¹ =
    HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24
⊢ HPow.hPow (β := ℕ) (η (-(↑z : ℂ)⁻¹)) 24 * (HPow.hPow (β := ℕ) (↑z : ℂ) 12)⁻¹ = HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24

Tactic:
simp only [he, mul_pow, mul_pow, inv_pow, csqrt_I_pow_24, csqrt_pow_24_eq (ne_zero z)]

Premises used: _private.0.ModularForm.csqrt_pow_24_eq, UpperHalfPlane.ne_zero, inv_pow, _private.0.ModularForm.csqrt_I_pow_24, mul_pow
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
he : η (-(↑z : ℂ)⁻¹) = I.sqrt⁻¹ * ((↑z : ℂ).sqrt * η (↑z : ℂ))
⊢ 1⁻¹ * (HPow.hPow (β := ℕ) (↑z : ℂ) 12 * HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24) * (HPow.hPow (β := ℕ) (↑z : ℂ) 12)⁻¹ =
    HPow.hPow (β := ℕ) (η (↑z : ℂ)) 24

Tactic:
field_simp [z.ne_zero]

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ ∀ (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))
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)))
⊢ ∀ (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

Premises used: norm_pow, Pi.zero_apply, tprod_one, norm_neg, add_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
⊢ |1 / 2| < 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (1 / 2) ^ (n + 1)

Tactic:
simpa only [pow_succ'] using (summable_geometric_of_abs_lt_one (by norm_num)).mul_left _

Premises used: Summable.mul_left, summable_geometric_of_abs_lt_one, pow_succ'
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
k : ℕ
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)

Tactic:
simpa using ((continuous_pow (M := ℂ) (k + 1)).tendsto 0).neg

Premises used: Filter.Tendsto.neg, Continuous.tendsto, HAdd.hAdd, OfNat.ofNat, continuous_pow
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
refine : ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
⊢ Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) (𝓝 0) (𝓝 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) ?_
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
h : ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 (1 / 2)) q) (k : ℕ), ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
⊢ ∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)

Tactic:
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) (by norm_num : (0 : ℝ) < 1 / 2)] with q hq k

Premises used: Metric.ball_mem_nhds, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 (1 / 2)) q
k : ℕ
⊢ ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)

Tactic:
pow_le_pow_left₀ (norm_nonneg _) (mem_ball_zero_iff.mp hq).le _

Premises used: pow_le_pow_left₀, LT.lt.le, Iff.mp, norm_nonneg, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 (1 / 2)) q
k : ℕ
⊢ ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)

Tactic:
exact pow_le_pow_left₀ (norm_nonneg _) (mem_ball_zero_iff.mp hq).le _

Premises used: pow_le_pow_left₀, LT.lt.le, Iff.mp, norm_nonneg, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ 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 _
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
htprod : Tendsto (β := ℂ) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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))
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)
⊢ Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) atImInfty (𝓝 1)

Tactic:
simp only [Periodic.qParam, ofReal_one, div_one, comp_apply, one_pow, eta_q] at *

Premises used: one_pow, Function.Periodic.qParam, ModularForm.eta_q, Complex.ofReal_one, Function.comp_apply, div_one
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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 : ℍ) ↦ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1))) 24)
    atImInfty (𝓝 1)

Tactic:
this
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
h :
  ∀ (τ : ℍ),
    ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)) 24 =
      HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))) 24
⊢ Tendsto (β := ℂ) (fun (x : ℍ) ↦ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑x : ℂ)) ^ (n + 1)) 24)
    atImInfty (𝓝 1)

Tactic:
convert! this using 2 with τ
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
τ : ℍ
h : Multipliable (α := ℂ) fun (n : ℕ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)) 24 =
    HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))) 24

Tactic:
rw [Multipliable.tprod_pow]

Premises used: Multipliable.tprod_pow
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
τ : ℍ
h : ∀ (b : ℕ), 1 - eta_q b (↑τ : ℂ) = 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1)
⊢ Multipliable (α := ℂ) fun (n : ℕ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)

Tactic:
apply (multipliableLocallyUniformlyOn_eta.multipliable τ.2).congr

Premises used: MultipliableLocallyUniformlyOn.multipliable, Multipliable.congr, UpperHalfPlane.coe_im_pos, ModularForm.multipliableLocallyUniformlyOn_eta
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
τ : ℍ
⊢ ∀ (b : ℕ), 1 - eta_q b (↑τ : ℂ) = 1 - cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (b + 1)

Tactic:
simp [eta_q, Periodic.qParam, ← exp_nat_mul]

Premises used: Function.Periodic.qParam, ModularForm.eta_q, Complex.exp_nat_mul
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
apply :
  Tendsto (β := ℂ) (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty
    (𝓝 0)
⊢ IsZeroAtImInfty Δ

Tactic:
apply Tendsto.congr (fun z ↦ (discriminant_eq_q_prod z).symm)

Premises used: ModularForm.discriminant_eq_q_prod, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ 0 = HMul.hMul (α := ℂ) 0 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
rw :
  Tendsto (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty
    (𝓝 (HMul.hMul (α := ℂ) 0 1))
⊢ Tendsto (β := ℂ) (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty
    (𝓝 0)

Tactic:
rw [show (0 : ℂ) = 0 * 1 by ring]
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ Eq (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24)
    (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ Tendsto (fun (z : ℍ) ↦ 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24) atImInfty
    (𝓝 (HMul.hMul (α := ℂ) 0 1))

Tactic:
exact (qParam_tendsto_atImInfty zero_lt_one).mul
    (tendsto_atImInfty_tprod_one_sub_eta_q_pow.congr fun z ↦ by congr 1)

Premises used: UpperHalfPlane.qParam_tendsto_atImInfty, Filter.Tendsto.mul, zero_lt_one, ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow, Filter.Tendsto.congr
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ Asymptotics.IsBigO (E := ℝ) atImInfty (fun (τ : ℍ) ↦ rexp (-2 * π * τ.im)) Δ

Tactic:
.of_bound 2 ?_

Premises used: Asymptotics.IsBigO.of_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
refine : ∀ᶠ (x : ℍ) in atImInfty, ‖rexp (-2 * π * x.im)‖ ≤ 2 * ‖Δ x‖
⊢ Asymptotics.IsBigO (E := ℝ) atImInfty (fun (τ : ℍ) ↦ rexp (-2 * π * τ.im)) Δ

Tactic:
refine .of_bound 2 ?_
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ ∀ᶠ (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))
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑x : ℂ)) 24) 1 < 1 / 2
h :
  ∀ (τ : ℍ) (hτ : dist (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1 < 1 / 2),
    ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖
⊢ ∀ᶠ (x : ℍ) in atImInfty, ‖rexp (-2 * π * x.im)‖ ≤ 2 * ‖Δ x‖

Tactic:
filter_upwards [hprod] with τ hτ
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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
h :
  rexp (-2 * π * τ.im) ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
⊢ ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖

Tactic:
rw [discriminant_eq_q_prod, norm_mul, Real.norm_of_nonneg (Real.exp_pos _).le]

Premises used: LT.lt.le, ModularForm.discriminant_eq_q_prod, norm_mul, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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
⊢ ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)

Tactic:
simp [Periodic.qParam, Complex.norm_exp]

Premises used: Function.Periodic.qParam, Complex.norm_exp
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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
⊢ ‖𝕢 1 (↑τ : ℂ)‖ = rexp (-2 * π * τ.im)

Tactic:
have hq_norm : ‖𝕢 1 τ‖ = Real.exp (-2 * π * τ.im) := by simp [Periodic.qParam, Complex.norm_exp]
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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)
h : ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))
⊢ rexp (-2 * π * τ.im) ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))

Tactic:
rw [← hq_norm]