awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f + g) = cuspFunction h f + cuspFunction h g

Tactic:
Periodic.cuspFunction_add hfcts hgcts

Premises used: UpperHalfPlane.cuspFunction, Function.Periodic.cuspFunction_add
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f - g) = cuspFunction h f - cuspFunction h g

Tactic:
Periodic.cuspFunction_sub hfcts hgcts

Premises used: Function.Periodic.cuspFunction_sub, UpperHalfPlane.cuspFunction
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
h₁ :
  ∀ (n : ℕ),
    Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f * g)) : ℂ)
      ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f * qExpansion h g) : ℂ)
⊢ qExpansion h (f * g) = qExpansion h f * qExpansion h g

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n : ℕ
h₁ :
  Eq (α := ℂ)
    (∑ i ∈ Finset.range (n + 1),
      (↑n.factorial : ℂ)⁻¹ *
        ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0))
    (∑ x ∈ Finset.range (n + 1),
      (↑x.factorial : ℂ)⁻¹ * iteratedDeriv x (cuspFunction h f) 0 *
        ((↑(n - x).factorial : ℂ)⁻¹ * iteratedDeriv (n - x) (cuspFunction h g) 0))
⊢ Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f * g)) : ℂ)
    ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h f * qExpansion h g) : ℂ)

Tactic:
simp only [qExpansion_coeff, cuspFunction_mul hf.continuousAt hg.continuousAt,
    iteratedDeriv_mul hf.contDiffAt hg.contDiffAt, Finset.mul_sum, PowerSeries.coeff_mul,
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Nat.succ_eq_add_one]

Premises used: Finset.mul_sum, Nat.succ_eq_add_one, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, iteratedDeriv_mul, UpperHalfPlane.qExpansion_coeff, PowerSeries.coeff_mul, AnalyticAt.continuousAt, AnalyticAt.contDiffAt, UpperHalfPlane.cuspFunction_mul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n : ℕ
⊢ Eq (α := ℂ)
    (∑ i ∈ Finset.range (n + 1),
      (↑n.factorial : ℂ)⁻¹ *
        ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0))
    (∑ x ∈ Finset.range (n + 1),
      (↑x.factorial : ℂ)⁻¹ * iteratedDeriv x (cuspFunction h f) 0 *
        ((↑(n - x).factorial : ℂ)⁻¹ * iteratedDeriv (n - x) (cuspFunction h g) 0))

Tactic:
Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n : ℕ
h₁ :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
    (↑n.factorial : ℂ)⁻¹ *
        ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0) =
      (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
        ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)
⊢ Eq (α := ℂ)
    (∑ i ∈ Finset.range (n + 1),
      (↑n.factorial : ℂ)⁻¹ *
        ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0))
    (∑ x ∈ Finset.range (n + 1),
      (↑x.factorial : ℂ)⁻¹ * iteratedDeriv x (cuspFunction h f) 0 *
        ((↑(n - x).factorial : ℂ)⁻¹ * iteratedDeriv (n - x) (cuspFunction h g) 0))

Tactic:
refine Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h₁ :
  (↑n.factorial : ℂ)⁻¹ *
      ((↑n.factorial : ℂ) / HMul.hMul (α := ℂ) (↑i.factorial : ℂ) (↑(n - i).factorial : ℂ) *
          iteratedDeriv i (cuspFunction h f) 0 *
        iteratedDeriv (n - i) (cuspFunction h g) 0) =
    (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)
⊢ (↑n.factorial : ℂ)⁻¹ *
      ((↑(n.choose i) : ℂ) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n - i) (cuspFunction h g) 0) =
    (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)

Tactic:
rw [Nat.cast_choose _ (by grind)]

Premises used: Nat.cast_choose
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (↑n.factorial : ℂ)⁻¹ *
      ((↑n.factorial : ℂ) / HMul.hMul (α := ℂ) (↑i.factorial : ℂ) (↑(n - i).factorial : ℂ) *
          iteratedDeriv i (cuspFunction h f) 0 *
        iteratedDeriv (n - i) (cuspFunction h g) 0) =
    (↑i.factorial : ℂ)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n - i).factorial : ℂ)⁻¹ * iteratedDeriv (n - i) (cuspFunction h g) 0)

Tactic:
field_simp [Nat.factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
a : ℂ
h₁ :
  ∀ (m : ℕ),
    Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (a • f)) : ℂ)
      ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (a • qExpansion h f) : ℂ)
⊢ qExpansion h (a • f) = a • qExpansion h f

Tactic:
ext m
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
a : ℂ
m : ℕ
⊢ Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (a • f)) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (a • qExpansion h f) : ℂ)

Tactic:
simp [qExpansion_coeff, cuspFunction_smul hf.continuousAt, iteratedDeriv_const_smul_field,
    mul_left_comm]

Premises used: UpperHalfPlane.qExpansion_coeff, mul_left_comm, UpperHalfPlane.cuspFunction_smul, iteratedDeriv_const_smul_field, AnalyticAt.continuousAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
⊢ qExpansion h (-f) = -qExpansion h f

Tactic:
simpa using qExpansion_smul hf (-1)

Premises used: UpperHalfPlane.qExpansion_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
h₁ :
  ∀ (m : ℕ),
    Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f + g)) : ℂ)
      ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f + qExpansion h g) : ℂ)
⊢ qExpansion h (f + g) = qExpansion h f + qExpansion h g

Tactic:
ext m
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
m : ℕ
⊢ Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (f + g)) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f + qExpansion h g) : ℂ)

Tactic:
simp [qExpansion_coeff, cuspFunction_add hf.continuousAt hg.continuousAt,
    iteratedDeriv_add hf.contDiffAt hg.contDiffAt, mul_add]

Premises used: iteratedDeriv_add, UpperHalfPlane.qExpansion_coeff, UpperHalfPlane.cuspFunction_add, AnalyticAt.continuousAt, mul_add, AnalyticAt.contDiffAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ AnalyticAt ℂ (cuspFunction h (-g)) 0

Tactic:
simpa [cuspFunction_neg hg.continuousAt] using hg.neg

Premises used: UpperHalfPlane.cuspFunction_neg, AnalyticAt.neg, AnalyticAt.continuousAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ AnalyticAt ℂ (cuspFunction h (-g)) 0

Tactic:
have hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0 := by
    simpa [cuspFunction_neg hg.continuousAt] using hg.neg
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0
⊢ qExpansion h (f - g) = qExpansion h f - qExpansion h g

Tactic:
simpa [sub_eq_add_neg, qExpansion_neg hg] using (qExpansion_add hf hg')

Premises used: sub_eq_add_neg, UpperHalfPlane.qExpansion_add, UpperHalfPlane.qExpansion_neg
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
this : cuspFunction h 0 = 0
h₁ :
  ∀ (n : ℕ),
    Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h 0) : ℂ)
      ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) 0 : ℂ)
⊢ qExpansion h 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
this : cuspFunction h 0 = 0
n : ℕ
⊢ Eq (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h 0) : ℂ)
    ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) 0 : ℂ)

Tactic:
simp [qExpansion_coeff, this]

Premises used: UpperHalfPlane.qExpansion_coeff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
suffices : cuspFunction h 0 = 0
⊢ qExpansion h 0 = 0

Tactic:
suffices cuspFunction h 0 = 0 by ext; simp [qExpansion_coeff, this]
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
⊢ cuspFunction h 0 = 0

Tactic:
simpa [cuspFunction, Periodic.cuspFunction]
    using (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).limUnder_eq

Premises used: tendsto_const_nhds, Function.Periodic.cuspFunction, UpperHalfPlane.cuspFunction, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
mp : qExpansion h f = 0 → f = 0
mpr : f = 0 → qExpansion h f = 0
⊢ qExpansion h f = 0 ↔ f = 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : qExpansion h f = 0
mp : ∀ (z : ℍ), f z = 0 z
⊢ f = 0

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : qExpansion h f = 0
z : ℍ
⊢ f z = 0 z

Tactic:
simp [← (hasSum_qExpansion hh hfper hfhol hfbdd z).tsum_eq, H]

Premises used: HasSum.tsum_eq, UpperHalfPlane.hasSum_qExpansion
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : f = 0
⊢ qExpansion h f = 0

Tactic:
simpa [H] using qExpansion_zero h

Premises used: UpperHalfPlane.qExpansion_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
h₁ :
  ∀ (m : ℕ),
    Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h 1) : ℂ)
      ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) 1 : ℂ)
⊢ qExpansion h 1 = 1

Tactic:
ext m
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
h₁ : ∀ (q : ℂ), cuspFunction h 1 q = 1 q
⊢ cuspFunction h 1 = 1

Tactic:
ext q
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
q : ℂ
h₁ : cuspFunction h 1 0 = 1 0
h₂ : ∀ (hq : q ≠ 0), cuspFunction h 1 q = 1 q
⊢ cuspFunction h 1 q = 1 q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
⊢ cuspFunction h 1 0 = 1 0

Tactic:
simpa [cuspFunction, Periodic.cuspFunction] using tendsto_const_nhds.limUnder_eq

Premises used: tendsto_const_nhds, Function.Periodic.cuspFunction, UpperHalfPlane.cuspFunction, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
q : ℂ
hq : q ≠ 0
⊢ cuspFunction h 1 q = 1 q

Tactic:
simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero h _ hq]

Premises used: UpperHalfPlane.cuspFunction, Function.Periodic.cuspFunction_eq_of_nonzero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
⊢ cuspFunction h 1 = 1

Tactic:
have h1 : cuspFunction h 1 = 1 := by
    ext q
    rcases eq_or_ne q 0 with rfl | hq
    · simpa [cuspFunction, Periodic.cuspFunction] using tendsto_const_nhds.limUnder_eq
    · simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero h _ hq]
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
⊢ Eq (α := ℂ) (iteratedDeriv (𝕜 := ℂ) m 1 0) (if m = 0 then 1 else 0)

Tactic:
simpa [ite_apply] using iteratedDeriv_const

Premises used: ite_apply, iteratedDeriv_const
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
⊢ Eq (α := ℂ) (iteratedDeriv (𝕜 := ℂ) m 1 0) (if m = 0 then 1 else 0)

Tactic:
have h2 : iteratedDeriv m (1 : ℂ → ℂ) 0 = if m = 0 then 1 else 0 := by
    simpa [ite_apply] using iteratedDeriv_const
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
h2 : Eq (α := ℂ) (iteratedDeriv (𝕜 := ℂ) m 1 0) (if m = 0 then 1 else 0)
⊢ Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h 1) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) 1 : ℂ)

Tactic:
simp +contextual [qExpansion_coeff, h1, h2]

Premises used: UpperHalfPlane.qExpansion_coeff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a : ℂ
f : F
inst_1 : ModularFormClass F Γ k
⊢ cuspFunction h (HSMul.hSMul (β := (a : ℍ) → ℂ) a (⇑f : (a : ℍ) → ℂ)) = a • cuspFunction h (⇑f : (a : ℍ) → ℂ)

Tactic:
cuspFunction_smul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt a

Premises used: UpperHalfPlane.cuspFunction_smul, AnalyticAt.continuousAt, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : F
inst_1 : ModularFormClass F Γ k
⊢ cuspFunction h (-(⇑f : (a : ℍ) → ℂ)) = -cuspFunction h (⇑f : (a : ℍ) → ℂ)

Tactic:
cuspFunction_neg (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt

Premises used: UpperHalfPlane.cuspFunction_neg, AnalyticAt.continuousAt, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
G : Type u_2
inst_1 : FunLike G ℍ ℂ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : F
inst_2 : ModularFormClass F Γ a
g : G
inst_3 : ModularFormClass G Γ b
⊢ cuspFunction h (HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    cuspFunction h (⇑f : (a : ℍ) → ℂ) + cuspFunction h (⇑g : (a : ℍ) → ℂ)

Tactic:
cuspFunction_add (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt
    (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ).continuousAt

Premises used: UpperHalfPlane.cuspFunction_add, AnalyticAt.continuousAt, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
G : Type u_2
inst_1 : FunLike G ℍ ℂ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : F
inst_2 : ModularFormClass F Γ a
g : G
inst_3 : ModularFormClass G Γ b
⊢ cuspFunction h (HSub.hSub (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    cuspFunction h (⇑f : (a : ℍ) → ℂ) - cuspFunction h (⇑g : (a : ℍ) → ℂ)

Tactic:
cuspFunction_sub (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt
    (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ).continuousAt

Premises used: UpperHalfPlane.cuspFunction_sub, AnalyticAt.continuousAt, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
⊢ cuspFunction h (⇑(f.mul g) : (a : ℍ) → ℂ) = cuspFunction h (⇑f : (a : ℍ) → ℂ) * cuspFunction h (⇑g : (a : ℍ) → ℂ)

Tactic:
cuspFunction_mul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt
    (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ).continuousAt

Premises used: AnalyticAt.continuousAt, ModularFormClass.analyticAt_cuspFunction_zero, UpperHalfPlane.cuspFunction_mul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a : ℂ
f : F
inst_1 : ModularFormClass F Γ k
⊢ qExpansion h (HSMul.hSMul (β := (a : ℍ) → ℂ) a (⇑f : (a : ℍ) → ℂ)) = a • qExpansion h (⇑f : (a : ℍ) → ℂ)

Tactic:
qExpansion_smul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ) a

Premises used: UpperHalfPlane.qExpansion_smul, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : F
inst_1 : ModularFormClass F Γ k
⊢ qExpansion h (-(⇑f : (a : ℍ) → ℂ)) = -qExpansion h (⇑f : (a : ℍ) → ℂ)

Tactic:
qExpansion_neg (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ)

Premises used: ModularFormClass.analyticAt_cuspFunction_zero, UpperHalfPlane.qExpansion_neg
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
G : Type u_2
inst_1 : FunLike G ℍ ℂ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : F
inst_2 : ModularFormClass F Γ a
g : G
inst_3 : ModularFormClass G Γ b
⊢ qExpansion h (HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) + qExpansion h (⇑g : (a : ℍ) → ℂ)

Tactic:
qExpansion_add (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ)
      (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ)

Premises used: UpperHalfPlane.qExpansion_add, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
G : Type u_2
inst_1 : FunLike G ℍ ℂ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : F
inst_2 : ModularFormClass F Γ a
g : G
inst_3 : ModularFormClass G Γ b
⊢ qExpansion h (HSub.hSub (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) - qExpansion h (⇑g : (a : ℍ) → ℂ)

Tactic:
qExpansion_sub (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ)
    (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ)

Premises used: UpperHalfPlane.qExpansion_sub, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
G : Type u_2
inst_1 : FunLike G ℍ ℂ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : F
inst_2 : ModularFormClass F Γ a
g : G
inst_3 : ModularFormClass G Γ b
⊢ qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) * qExpansion h (⇑g : (a : ℍ) → ℂ)

Tactic:
qExpansion_mul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ)
    (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ)

Premises used: UpperHalfPlane.qExpansion_mul, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
⊢ qExpansion h (⇑(f.mul g) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) * qExpansion h (⇑g : (a : ℍ) → ℂ)

Tactic:
ModularForm.qExpansion_mul_coe hh hΓ f g

Premises used: ModularForm.qExpansion_mul_coe
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
k : ℤ
f : ModularForm Γ k
⊢ Fact (IsCusp OnePoint.infty Γ)

Tactic:
have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
k : ℤ
f : ModularForm Γ k
this : Fact (IsCusp OnePoint.infty Γ)
⊢ qExpansion h (⇑f : (a : ℍ) → ℂ) = 0 ↔ f = 0

Tactic:
simp [qExpansion_eq_zero_iff hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f)]

Premises used: SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, UpperHalfPlane.qExpansion_eq_zero_iff, ModularFormClass.holo
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
⊢ qExpansion h (⇑1 : (a : ℍ) → ℂ) = 1

Tactic:
simp [qExpansion_one]

Premises used: UpperHalfPlane.qExpansion_one
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
a b : ℤ
Γ' : Subgroup (GL (Fin 2) ℝ)
heq : a = b
hΓ : Γ' = Γ
f : ModularForm Γ a
⊢ qExpansion h (⇑(mcast heq f hΓ) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
⊢ qExpansion h (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) 0

Tactic:
simp only [coe_pow, pow_zero, qExpansion_one]

Premises used: UpperHalfPlane.qExpansion_one, ModularForm.coe_pow, pow_zero
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₁ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₂ :
  qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑(f.pow n) : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₃ : qExpansion h (⇑((f.pow n).mul f) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₄ :
  qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₅ :
  qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₆ succ₇ :
  qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)

Tactic:
rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]

Premises used: ModularForm.coe_mul, pow_succ, ModularForm.coe_pow, ModularForm.qExpansion_mul