awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
    fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have right : IsBigO (E := ℝ) (F := ℝ) atImInfty
  (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
  fun (τ : ℍ) ↦ 1 * Real.exp (-a * τ.im)
Tactic: conv_rhs => enter [τ]; rw [← one_mul (Real.exp _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (hypothesis)
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
    fun (τ : ℍ) ↦ 1 * Real.exp (-a * τ.im)
have hf' : IsBoundedAtImInfty (α := ℂ) (⇑f' : (a : ℍ) → ℂ)
Tactic: have hf' : IsBoundedAtImInfty f' := ModularFormClass.bdd_at_infty f'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
hf' : IsBoundedAtImInfty (α := ℂ) (⇑f' : (a : ℍ) → ℂ)
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
    fun (τ : ℍ) ↦ 1 * Real.exp (-a * τ.im)
have right : IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ Real.exp (-b * x.im) * x.im ^ k) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
Tactic: refine hf'.norm_left.mul ((hbf.norm_left.mul <| isBigO_refl _ _).trans ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
hf' : IsBoundedAtImInfty (α := ℂ) (⇑f' : (a : ℍ) → ℂ)
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ Real.exp (-b * x.im) * x.im ^ k) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have right : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ Real.exp (-b * t) * t ^ k) fun (t : ℝ) ↦ Real.exp (-a * t)
Tactic: refine IsBigO.comp_tendsto (f := fun t : ℝ ↦ Real.exp (-b * t) * t ^ k)
     (g := fun t : ℝ ↦ Real.exp (-a * t)) ?_ tendsto_comap
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
f' : F'
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f' : (a : ℍ) → ℂ)
⊢ ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have obtain : ∀ (a : ℝ) (ha : a > 0)
  (ha' :
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f' : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)),
  ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
Tactic: obtain ⟨a, ha, ha'⟩ := h_bd.petersson_exp_decay_left k Γ f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
f : ℍ → E
hf : ∃ c > 0, IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-c * τ.im)
⊢ IsZeroAtImInfty f
have obtain : ∀ (a : ℝ) (ha : a > 0) (ha' : IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-a * τ.im)), IsZeroAtImInfty f
Tactic: obtain ⟨a, ha, ha'⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ IsZeroAtImInfty f
have refine : Tendsto (α := ℝ) (HMul.hMul (-a)) atTop atBot
Tactic: refine ha'.trans_tendsto <| (Real.tendsto_exp_atBot.comp ?_).comp tendsto_comap
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous (hypothesis)
Goal:
𝒮ℒ' : Subgroup SL(2, ℝ) := MonoidHom.range (SpecialLinearGroup.map (Int.castRingHom ℝ))
⊢ ProperlyDiscontinuousSMul ↥(MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) ℍ
have this : ProperlyDiscontinuousSMul ↥𝒮ℒ' ℍ
Tactic: have : ProperlyDiscontinuousSMul 𝒮ℒ' ℍ := inferInstance
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous (goal)
Goal:
𝒮ℒ' : Subgroup SL(2, ℝ) := MonoidHom.range (SpecialLinearGroup.map (Int.castRingHom ℝ))
this : ProperlyDiscontinuousSMul ↥𝒮ℒ' ℍ
⊢ ProperlyDiscontinuousSMul ↥(MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) ℍ
have simp : ∀
  (this :
    ∀ {K L : Set ℍ},
      IsCompact K → IsCompact L → Set.Finite (α := SL(2, ℝ)) {g : SL(2, ℝ) | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty})
  {K L : Set ℍ},
  IsCompact K →
    IsCompact L →
      Set.Finite (α := GL (Fin 2) ℝ)
        {g : GL (Fin 2) ℝ |
          Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ))
              g ∧
            (g • K ∩ L).Nonempty}
Tactic: simp only [Subgroup.properlyDiscontinuousSMul_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous (goal)
Goal:
𝒮ℒ' : Subgroup SL(2, ℝ) := MonoidHom.range (SpecialLinearGroup.map (Int.castRingHom ℝ))
this :
  ∀ {K L : Set ℍ},
    IsCompact K → IsCompact L → Set.Finite (α := SL(2, ℝ)) {g : SL(2, ℝ) | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty}
⊢ ∀ {K L : Set ℍ},
    IsCompact K →
      IsCompact L →
        Set.Finite (α := GL (Fin 2) ℝ)
          {g : GL (Fin 2) ℝ |
            Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ))
                g ∧
              (g • K ∩ L).Nonempty}
have refine : ∀ (K L : Set ℍ) (hK : IsCompact K) (hL : IsCompact L) (g : GL (Fin 2) ℝ),
  Membership.mem (γ := Set (GL (Fin 2) ℝ))
      {g : GL (Fin 2) ℝ |
        Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) g ∧
          (g • K ∩ L).Nonempty}
      g →
    Membership.mem (γ := Set (GL (Fin 2) ℝ))
      (Functor.map (α := SL(2, ℝ)) (⇑SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        {g : SL(2, ℝ) | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty})
      g
Tactic: refine fun K L hK hL ↦ ((this hK hL).map SpecialLinearGroup.toGL).subset fun g ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ
have rw : ProperlyDiscontinuousSMul ↥(MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) ℍ
Tactic: rw [is_commensurable.properlyDiscontinuousSMul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction h f) q
have inl : ∀ (hq : norm (E := ℂ) 0 < 1), DifferentiableAt ℂ (cuspFunction h f) 0
Tactic: rcases eq_or_ne q 0 with rfl | hq'
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
inl : ∀ (hq : norm (E := ℂ) 0 < 1), DifferentiableAt ℂ (cuspFunction h f) 0
⊢ DifferentiableAt ℂ (cuspFunction h f) q
have inr : ∀ (hq' : q ≠ 0), DifferentiableAt ℂ (cuspFunction h f) q
Tactic: rcases eq_or_ne q 0 with rfl | hq'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ cuspFunction h f 0 = valueAtInfty f
have refine : Tendsto f atImInfty (𝓝 (cuspFunction h f 0))
Tactic: refine (Tendsto.limUnder_eq ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) = f
have h₁ : ∀ (τ : ℍ), (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) τ = f τ
Tactic: funext τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ Tendsto f atImInfty (𝓝 (cuspFunction h f 0))
have this : (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) = f
Tactic: have : (cuspFunction h f ∘ fun τ ↦ 𝕢 h τ : ℍ → ℂ) = f := by
    funext τ
    simpa using eq_cuspFunction τ hh.ne' hfper
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
have pos : ∀ (hw : 0 < w.im),
  Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
Tactic: by_cases! hw : 0 < im w
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
pos :
  ∀ (hw : 0 < w.im),
    Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
      (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
have neg : ∀ (hw : w.im ≤ 0),
  Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
Tactic: by_cases! hw : 0 < im w
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
have this : 0 < (w + (↑h : ℂ)).im
Tactic: have : 0 < im (w + h) := by simp [hw]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
have pos : Eq (α := ℂ) ((f : (a : ℍ) → ℂ) { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ)
  ((f : (a : ℍ) → ℂ) { coe := w, coe_im_pos := hw : ℍ } : ℂ)
Tactic: simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ)
    ((f : (a : ℍ) → ℂ) { coe := w, coe_im_pos := hw : ℍ } : ℂ)
have h₁ : { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } = h +ᵥ { coe := w, coe_im_pos := hw : ℍ }
Tactic: convert! SlashInvariantForm.vAdd_apply_of_mem_strictPeriods f ⟨w, hw⟩ hΓ using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + (↑h : ℂ)).im
⊢ { coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } = h +ᵥ { coe := w, coe_im_pos := hw : ℍ }
have h₁ : (↑{ coe := w + (↑h : ℂ), coe_im_pos := this : ℍ } : ℂ) = (↑(h +ᵥ { coe := w, coe_im_pos := hw : ℍ }) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst_1 : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
have this : (w + (↑h : ℂ)).im ≤ 0
Tactic: have : im (w + h) ≤ 0 := by simpa using hw
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ HasSum
    (fun (m : ℕ) ↦ HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (q ^ m))
    (cuspFunction h f q)
have h₁ : ∀ (m : ℕ),
  HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (q ^ m) =
    HSMul.hSMul (α := ℂ) (↑m.factorial : ℂ)⁻¹ ((q - 0) ^ m • iteratedDeriv m (cuspFunction h f) 0)
Tactic: convert!
    hasSum_taylorSeries_on_ball (differentiableOn_cuspFunction_ball hh hfper hfhol hfbdd)
      (by simpa using hq) using
    2 with m
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
⊢ HasSum
    (fun (m : ℕ) ↦
      HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (𝕢 h (↑τ : ℂ) ^ m))
    (f τ)
have this : 0 < 2 * π * τ.im / h
Tactic: have : 0 < 2 * π * τ.im / h := by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
this : 0 < 2 * π * τ.im / h
⊢ HasSum
    (fun (m : ℕ) ↦
      HSMul.hSMul (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h f) : ℂ) (𝕢 h (↑τ : ℂ) ^ m))
    (f τ)
have this₁ : ‖𝕢 h (↑τ : ℂ)‖ < 1
Tactic: have : ‖𝕢 h τ‖ < 1 := by simpa [Periodic.qParam, Complex.norm_exp, neg_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖qExpansionFormalMultilinearSeries h f m‖ =
    norm (E := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)
have rw : norm (E := ℂ)
    ((LinearIsometryEquiv.symm (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ) :
          (a : ContinuousMultilinearMap ℂ (fun (x : Fin m) ↦ ℂ) ℂ) → ℂ)
        (FormalMultilinearSeries.ofScalars ℂ
          (fun (m : ℕ) ↦ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))) m) :
      ℂ) =
  norm (E := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)
Tactic: rw [qExpansionFormalMultilinearSeries,
    ← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ 1 ≤ (qExpansionFormalMultilinearSeries h f).radius
have refine : ∀ (r : ENNReal) (hr : r < 1), r ≤ (qExpansionFormalMultilinearSeries h f).radius
Tactic: refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : ENNReal
hr : r < 1
⊢ r ≤ (qExpansionFormalMultilinearSeries h f).radius
have lift : ∀ (r : NNReal) (hr : (↑r : ENNReal) < 1), (↑r : ENNReal) ≤ (qExpansionFormalMultilinearSeries h f).radius
Tactic: lift r to NNReal using hr.ne_top
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
⊢ (↑r : ENNReal) ≤ (qExpansionFormalMultilinearSeries h f).radius
have h₁ : Summable (α := ℝ) fun (n : ℕ) ↦ ‖qExpansionFormalMultilinearSeries h f n‖ * (↑r : ℝ) ^ n
Tactic: apply FormalMultilinearSeries.le_radius_of_summable
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖qExpansionFormalMultilinearSeries h f n‖ * (↑r : ℝ) ^ n
have h₁ : Summable (α := ℝ) fun (n : ℕ) ↦
  norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) * (↑r : ℝ) ^ n
Tactic: simp only [qExpansionFormalMultilinearSeries_apply_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) * (↑r : ℝ) ^ n
have h₁ : Summable (α := ℝ) fun (n : ℕ) ↦
  norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) * |(↑r : ℝ)| ^ n
Tactic: rw [← r.abs_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff (⇑f : (a : ℍ) → ℂ)
hfbdd : IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
r : NNReal
hr : (↑r : ENNReal) < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ) *
      |(↑r : ℝ)| ^ n
have h₁ : Summable (α := ℝ) fun (n : ℕ) ↦
  ‖HMul.hMul (α := ℂ) ((PowerSeries.coeff n : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) : ℂ)
      ((↑(↑r : ℝ) : ℂ) ^ n)‖
Tactic: simp_rw [← Real.norm_eq_abs, ← Complex.norm_real, ← norm_pow, ← norm_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
⊢ HasSum (fun (m : ℕ) ↦ c m • q ^ m) (cuspFunction h f q)
have h1 : 0 < (Periodic.invQParam h q).im
Tactic: have h1 := Periodic.im_invQParam_pos_of_norm_lt_one hh hq hq1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
⊢ HasSum (fun (m : ℕ) ↦ c m • q ^ m) (cuspFunction h f q)
have h2 : Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) q = (f ∘ (↑ofComplex : ℂ → ℍ)) (Periodic.invQParam h q)
Tactic: have h2 := (Periodic.cuspFunction_eq_of_nonzero h (f ∘ ofComplex) hq1)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ (↑ofComplex : ℂ → ℍ)) q = (f ∘ (↑ofComplex : ℂ → ℍ)) (Periodic.invQParam h q)
⊢ HasSum (fun (m : ℕ) ↦ c m • q ^ m) (cuspFunction h f q)
have this : cuspFunction h f q = f τ
Tactic: have : cuspFunction h f q = f τ := by simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1] using h2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
⊢ HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
have r_le : 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r_le : 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
⊢ HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
have r_pos : LT.lt (α := ENNReal) 0 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) (f τ)
r_le : 1 ≤ FormalMultilinearSeries.radius (FormalMultilinearSeries.ofScalars ℂ c)
r_pos : LT.lt (α := ENNReal) 0 1
⊢ HasFPowerSeriesOnBall (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0))
    (FormalMultilinearSeries.ofScalars ℂ c) 0 1
have hasSum : ∀ {y : ℂ},
  Membership.mem (γ := Set ℂ) (eball 0 1) y →
    HasSum (fun (n : ℕ) ↦ (FormalMultilinearSeries.ofScalars ℂ c n : (a : (i : Fin n) → ℂ) → ℂ) fun (x : Fin n) ↦ y)
      (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (c 0) (0 + y))
Tactic: constructor