awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rwa rwa₁ rwa₂ 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
⊢ ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2

Tactic:
rwa [Complex.dist_eq] at hτ

Premises used: Complex.dist_eq
-- 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)
⊢ ‖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τ
-- 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)
hsub : ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2
⊢ 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)
-- 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)
hsub : ‖HSub.hSub (α := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24) 1‖ < 1 / 2
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)‖
⊢ 1 / 2 ≤ norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24)

Tactic:
grind [norm_one, norm_sub_rev]

Premises used: NormOneClass.norm_one, norm_sub_rev
-- 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)
⊢ 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]
-- 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)
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
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
⊢ ‖𝕢 1 (↑τ : ℂ)‖ ≤ 2 * (‖𝕢 1 (↑τ : ℂ)‖ * norm (E := ℂ) (∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑τ : ℂ)) 24))

Tactic:
linarith [norm_nonneg (𝕢 1 τ), mul_le_mul_of_nonneg_left hprod_bound (norm_nonneg (𝕢 1 τ))]

Premises used: Function.Periodic.qParam, UpperHalfPlane.coe, OfNat.ofNat, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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
neg : ∀ (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

Tactic:
by_cases hq0 : q = 0
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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

Tactic:
simpa [hq0] using Periodic.cuspFunction_zero_of_zero_at_inf one_pos
      discriminant_isZeroAtImInfty.zero_at_infty_comp_ofComplex

Premises used: ModularForm.discriminant_isZeroAtImInfty, Function.Periodic.cuspFunction_zero_of_zero_at_inf, UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq0 : ¬q = 0
⊢ ‖q‖ < 1

Tactic:
simpa [dist_zero_right] using hq

Premises used: dist_zero_right
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq0 : ¬q = 0
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq0 : ¬q = 0
him : 0 < (Periodic.invQParam 1 q).im
⊢ cuspFunction 1 Δ q = (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) q

Tactic:
simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero 1 _ hq0,
      ofComplex_apply_of_im_pos him, discriminant_eq_q_prod ⟨_, him⟩,
      Periodic.qParam_right_inv one_ne_zero hq0, eta_q]

Premises used: ModularForm.eta_q, UpperHalfPlane.cuspFunction, UpperHalfPlane.ofComplex_apply_of_im_pos, UpperHalfPlane.mk, ModularForm.discriminant_eq_q_prod, Function.Periodic.qParam_right_inv, Function.Periodic.cuspFunction_eq_of_nonzero, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0

Tactic:
have hmem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) 1 := Metric.mem_ball_self one_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
hmem : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
⊢ (PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0

Tactic:
simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]

Premises used: UpperHalfPlane.qExpansion_coeff, Metric.isOpen_ball, derivWithin_of_isOpen
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
hmem : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
⊢ derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0 =
    derivWithin (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) (Metric.ball 0 1) 0

Tactic:
derivWithin_congr discriminant_cuspFunction_eqOn (discriminant_cuspFunction_eqOn hmem)

Premises used: derivWithin_congr, ModularForm.discriminant_cuspFunction_eqOn
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
hmem : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
⊢ Eq (α := ℂ) (derivWithin (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) (Metric.ball 0 1) 0)
    1

Tactic:
simp [derivWithin_fun_mul differentiableWithinAt_fun_id
          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]

Premises used: ModularForm.differentiableOn_tprod_one_sub_pow_pow, derivWithin_id', derivWithin_fun_mul, IsOpen.uniqueDiffWithinAt, Metric.isOpen_ball, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
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
calc₁ :
  Eq (α := ℂ) (derivWithin (fun (q : ℂ) ↦ q * ∏' (i : ℕ), HPow.hPow (β := ℕ) (1 - q ^ (i + 1)) 24) (Metric.ball 0 1) 0)
    1
⊢ Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (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)]

Premises used: derivWithin_congr, HMul.hMul, UpperHalfPlane.qExpansion, HSub.hSub, UpperHalfPlane.cuspFunction, Metric.ball, PowerSeries.coeff, derivWithin, HPow.hPow, HAdd.hAdd, ModularForm.discriminant, tprod, OfNat.ofNat, DFunLike.coe, SummationFilter.unconditional, ModularForm.discriminant_cuspFunction_eqOn
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
A : GL (Fin 2) ℝ
hA :
  Membership.mem (γ := outParam (Subgroup (GL (Fin 2) ℝ)))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) A
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) ℝ) Δ =
      Δ
⊢ @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 A Δ = Δ

Tactic:
obtain ⟨A, rfl⟩ := hA

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
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:
slash_action_generators_SL2Z discriminant_S_invariant discriminant_T_invariant A

Premises used: SlashInvariantForm.slash_action_generators_SL2Z, ModularForm.discriminant_T_invariant, ModularForm.discriminant_S_invariant
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
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:
exact slash_action_generators_SL2Z discriminant_S_invariant discriminant_T_invariant A

Premises used: SlashInvariantForm.slash_action_generators_SL2Z, ModularForm.discriminant_T_invariant, ModularForm.discriminant_S_invariant
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
rw :
  DifferentiableOn ℂ (F := ℂ) ((⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))
    {z : ℂ | 0 < z.im}
⊢ MDiff (⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ)

Tactic:
rw [UpperHalfPlane.mdifferentiable_iff]

Premises used: UpperHalfPlane.mdifferentiable_iff
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ (F := ℂ) ((⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))
    {z : ℂ | 0 < z.im}

Tactic:
.congr (fun z hz ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).pow
      24 |>.differentiableWithinAt) fun z hz ↦ ?_

Premises used: DifferentiableOn.congr, DifferentiableAt.differentiableWithinAt, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, DifferentiableAt.pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
refine :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z),
    ((⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) z = HPow.hPow (β := ℕ) η 24 z
⊢ DifferentiableOn ℂ (F := ℂ) ((⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ))
    {z : ℂ | 0 < z.im}

Tactic:
refine .congr (fun z hz ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).pow
      24 |>.differentiableWithinAt) fun z hz ↦ ?_
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
⊢ ((⇑{ toFun := Δ, slash_action_eq' := ⋯ } : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) z = HPow.hPow (β := ℕ) η 24 z

Tactic:
simp [ModularForm.discriminant, ofComplex_apply_of_im_pos hz]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, ModularForm.discriminant
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
rw :
  ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
        c →
      IsZeroAtImInfty
        (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ Δ)
⊢ c.IsZeroAt Δ 12

Tactic:
rw [OnePoint.isZeroAt_iff_forall_SL2Z hc]

Premises used: OnePoint.isZeroAt_iff_forall_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
_ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
      c →
    IsZeroAtImInfty
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ Δ)
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
      c →
    IsZeroAtImInfty
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ Δ)

Tactic:
_
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
    c
rw : IsZeroAtImInfty Δ
⊢ IsZeroAtImInfty
    (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ Δ)

Tactic:
rw [slash_action_generators_SL2Z discriminant_S_invariant discriminant_T_invariant]

Premises used: SlashInvariantForm.slash_action_generators_SL2Z, ModularForm.discriminant_T_invariant, ModularForm.discriminant_S_invariant
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
    c
⊢ IsZeroAtImInfty Δ

Tactic:
discriminant_isZeroAtImInfty

Premises used: ModularForm.discriminant_isZeroAtImInfty
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
    c
⊢ IsZeroAtImInfty Δ

Tactic:
exact discriminant_isZeroAtImInfty

Premises used: ModularForm.discriminant_isZeroAtImInfty
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ (⇑discriminant : (a : ℍ) → ℂ) = Δ

Tactic:
rfl

Premises used: ModularForm.discriminant, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ Asymptotics.IsBigO (E := ℝ) atImInfty (fun (τ : ℍ) ↦ rexp (-2 * π * τ.im / 1)) Δ

Tactic:
simpa using exp_isBigO_discriminant

Premises used: ModularForm.exp_isBigO_discriminant
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Goal:
k : ℤ
N : ℕ
inst : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(N))
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Goal:
k : ℤ
N : ℕ
inst : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
rw :
  ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
        c →
      UpperHalfPlane.IsBoundedAtImInfty (α := ℂ)
        (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : UpperHalfPlane) ↦ ℂ)) _ k
          γ (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ))
⊢ c.IsBoundedAt (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ) k

Tactic:
rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]

Premises used: OnePoint.isBoundedAt_iff_forall_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Goal:
k : ℤ
N : ℕ
inst : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
        c →
      UpperHalfPlane.IsBoundedAtImInfty (α := ℂ)
        (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : UpperHalfPlane) ↦ ℂ)) _ k
          γ (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ))

Tactic:
fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeriesSIF a hk γ

Premises used: EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Goal:
k : ℤ
N : ℕ
inst : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) OnePoint.infty =
        c →
      UpperHalfPlane.IsBoundedAtImInfty (α := ℂ)
        (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : UpperHalfPlane) ↦ ℂ)) _ k
          γ (⇑(eisensteinSeriesSIF a k) : (a : UpperHalfPlane) → ℂ))

Tactic:
exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeriesSIF a hk γ

Premises used: EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Goal:
⊢ LE.le (α := ℕ) 3 4

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
Goal:
⊢ LE.le (α := ℕ) 3 6

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
⊢ Pairwise (Disjoint on gammaSet N r)

Tactic:
fun u v huv ↦ ?_

Premises used: Pairwise
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
refine : ∀ (u v : Fin 2 → ZMod N) (huv : u ≠ v), (Disjoint on gammaSet N r) u v
⊢ Pairwise (Disjoint on gammaSet N r)

Tactic:
refine fun u v huv ↦ ?_
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
u v : Fin 2 → ZMod N
huv : u ≠ v
contrapose : ∀ (huv : ¬(Disjoint on gammaSet N r) u v), u = v
⊢ (Disjoint on gammaSet N r) u v

Tactic:
contrapose huv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N r) u v
obtain : ∀ (f : Fin 2 → ℤ) (hf : f ∈ gammaSet N r u ∧ f ∈ gammaSet N r v), u = v
⊢ u = v

Tactic:
obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv

Premises used: Set.not_disjoint_iff, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N r) u v
f : Fin 2 → ℤ
hf : f ∈ gammaSet N r u ∧ f ∈ gammaSet N r v
⊢ u = v

Tactic:
hf.1.1.symm.trans hf.2.1

Premises used: And.right, And.left, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
N r : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N r) u v
f : Fin 2 → ℤ
hf : f ∈ gammaSet N r u ∧ f ∈ gammaSet N r v
⊢ u = v

Tactic:
exact hf.1.1.symm.trans hf.2.1

Premises used: And.right, And.left, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
a a' : Fin 2 → ZMod 1
⊢ gammaSet 1 r a = gammaSet 1 r a'

Tactic:
congr_arg _ (Subsingleton.elim _ _)

Premises used: congr_arg, Subsingleton.elim
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
a : Fin 2 → ZMod 1
⊢ gammaSet 1 r a = {v : Fin 2 → ℤ | (v 0).gcd (v 1) = r}

Tactic:
simp [gammaSet, Subsingleton.eq_zero]

Premises used: EisensteinSeries.gammaSet, Subsingleton.eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Goal:
r : ℕ
v : Fin 2 → ℤ
⊢ v ∈ gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r

Tactic:
simp [gammaSet, Subsingleton.eq_zero]

Premises used: EisensteinSeries.gammaSet, Subsingleton.eq_zero