awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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)

Tactic:
hf'.norm_left.mul ((hbf.norm_left.mul <| isBigO_refl _ _).trans ?_)

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Asymptotics.isBigO_refl
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 : ℍ) → ℂ)
right :
  IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ Real.exp (-b * x.im) * x.im ^ k) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ 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:
refine hf'.norm_left.mul ((hbf.norm_left.mul <| isBigO_refl _ _).trans ?_)

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, Asymptotics.isBigO_refl
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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)

Tactic:
IsBigO.comp_tendsto (f := fun t : ℝ ↦ Real.exp (-b * t) * t ^ k)
     (g := fun t : ℝ ↦ Real.exp (-a * t)) ?_ tendsto_comap

Premises used: Real.exp, Filter.tendsto_comap, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 : ℍ) → ℂ)
right : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ Real.exp (-b * t) * t ^ k) fun (t : ℝ) ↦ Real.exp (-a * t)
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ Real.exp (-b * x.im) * x.im ^ k) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
refine IsBigO.comp_tendsto (f := fun t : ℝ ↦ Real.exp (-b * t) * t ^ k)
     (g := fun t : ℝ ↦ Real.exp (-a * t)) ?_ tendsto_comap

Premises used: Filter.tendsto_comap, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 := ℝ) atTop (fun (t : ℝ) ↦ Real.exp (-b * t) * t ^ k) fun (t : ℝ) ↦ Real.exp (-a * t)

Tactic:
simpa using (isLittleO_exp_mul_rpow_of_lt k (neg_lt_neg ha')).isBigO

Premises used: Int.cast, isLittleO_exp_mul_rpow_of_lt, neg_lt_neg, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 : ℍ) → ℂ)
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)
⊢ ∃ 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

Premises used: UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 : ℝ
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:
⟨a, ha, .of_norm_left <| ha'.norm_left.congr_left <| petersson_norm_symm k f f'⟩

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.congr_left, UpperHalfPlane.petersson_norm_symm, And.intro, Exists.intro, DFunLike.coe, Asymptotics.IsBigO.of_norm_left
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 : ℝ
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:
exact ⟨a, ha, .of_norm_left <| ha'.norm_left.congr_left <| petersson_norm_symm k f f'⟩
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
E : Type u_3
inst : NormedAddCommGroup E
f : ℍ → E
hf : ∃ c > 0, IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-c * τ.im)
obtain :
  ∀ (a : ℝ) (ha : a > 0) (ha' : IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-a * τ.im)), IsZeroAtImInfty f
⊢ IsZeroAtImInfty f

Tactic:
obtain ⟨a, ha, ha'⟩ := hf
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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

Tactic:
ha'.trans_tendsto <| (Real.tendsto_exp_atBot.comp ?_).comp tendsto_comap

Premises used: Filter.ZeroAtFilter, Filter.tendsto_comap, Real.tendsto_exp_atBot, Asymptotics.IsBigO.trans_tendsto, UpperHalfPlane.IsZeroAtImInfty, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
E : Type u_3
inst : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
refine : Tendsto (α := ℝ) (HMul.hMul (-a)) atTop atBot
⊢ IsZeroAtImInfty f

Tactic:
refine ha'.trans_tendsto <| (Real.tendsto_exp_atBot.comp ?_).comp tendsto_comap

Premises used: Filter.tendsto_comap, Real.tendsto_exp_atBot, Asymptotics.IsBigO.trans_tendsto, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
E : Type u_3
inst : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ Tendsto (α := ℝ) (HMul.hMul (-a)) atTop atBot

Tactic:
tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr ha)

Premises used: Iff.mpr, Filter.tendsto_id, neg_lt_zero, Filter.Tendsto.const_mul_atTop_of_neg
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
E : Type u_3
inst : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : IsBigO (F := ℝ) atImInfty f fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ Tendsto (α := ℝ) (HMul.hMul (-a)) atTop atBot

Tactic:
exact tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr ha)

Premises used: Iff.mpr, Filter.tendsto_id, neg_lt_zero, Filter.Tendsto.const_mul_atTop_of_neg
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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'
⊢ IsZeroAtImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ))

Tactic:
of_exp_decay (h_bd.petersson_exp_decay_left k Γ f')

Premises used: UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left, UpperHalfPlane.IsZeroAtImInfty.of_exp_decay
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
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 : ℍ) → ℂ)
⊢ IsZeroAtImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ))

Tactic:
of_exp_decay (h_bd.petersson_exp_decay_right k Γ f)

Premises used: UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right, UpperHalfPlane.IsZeroAtImInfty.of_exp_decay
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
Goal:
𝒮ℒ' : Subgroup SL(2, ℝ) := MonoidHom.range (SpecialLinearGroup.map (Int.castRingHom ℝ))
⊢ ProperlyDiscontinuousSMul ↥𝒮ℒ' ℍ

Tactic:
have : ProperlyDiscontinuousSMul 𝒮ℒ' ℍ := inferInstance
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
Goal:
𝒮ℒ' : Subgroup SL(2, ℝ) := MonoidHom.range (SpecialLinearGroup.map (Int.castRingHom ℝ))
this : ProperlyDiscontinuousSMul ↥𝒮ℒ' ℍ
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}
⊢ ProperlyDiscontinuousSMul ↥(MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) ℍ

Tactic:
simp only [Subgroup.properlyDiscontinuousSMul_iff] at this ⊢

Premises used: Subgroup.properlyDiscontinuousSMul_iff
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
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}

Tactic:
fun K L hK hL ↦ ((this hK hL).map SpecialLinearGroup.toGL).subset fun g ↦ ?_

Premises used: Set.Finite.subset, Set.Finite.map, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
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}
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
⊢ ∀ {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:
refine fun K L hK hL ↦ ((this hK hL).map SpecialLinearGroup.toGL).subset fun g ↦ ?_

Premises used: Set.Finite.subset, Set.Finite.map, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
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 ℍ
hK : IsCompact K
hL : IsCompact L
γ : SL(2, ℤ)
hγ :
  (HSMul.hSMul (α := GL (Fin 2) ℝ) ((SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) K ∩
      L).Nonempty
⊢ Membership.mem (α := SL(2, ℝ)) 𝒮ℒ'
    ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ : SL(2, ℝ))

Tactic:
simp [𝒮ℒ']
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
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 ℍ
hK : IsCompact K
hL : IsCompact L
γ : SL(2, ℤ)
hγ :
  (HSMul.hSMul (α := GL (Fin 2) ℝ) ((SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) K ∩
      L).Nonempty
⊢ Membership.mem (α := GL (Fin 2) ℝ) (γ := Set (GL (Fin 2) ℝ))
    (Functor.map (α := SL(2, ℝ)) (⇑SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
      {g : SL(2, ℝ) | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty})
    ((SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)

Tactic:
exact ⟨γ, ⟨by simp [𝒮ℒ'], hγ⟩, rfl⟩
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
rw : ProperlyDiscontinuousSMul ↥(MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) ℍ
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ

Tactic:
rw [is_commensurable.properlyDiscontinuousSMul_iff]

Premises used: Subgroup.IsArithmetic.is_commensurable, Subgroup.Commensurable.properlyDiscontinuousSMul_iff
-- Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
⊢ ProperlyDiscontinuousSMul ↥(MonoidHom.range (G := SL(2, ℤ)) (SpecialLinearGroup.mapGL ℝ)) ℍ

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
f : ℍ → ℂ
hf : IsZeroAtImInfty f
⊢ valueAtInfty f = 0

Tactic:
hf.limUnder_eq

Premises used: UpperHalfPlane.valueAtInfty, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℂ) (fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) atImInfty (𝓝 0)

Tactic:
((Periodic.qParam_tendsto hh).mono_right nhdsWithin_le_nhds).comp tendsto_coe_atImInfty

Premises used: Function.Periodic.qParam, nhdsWithin_le_nhds, Function.Periodic.qParam_tendsto, Filter.Tendsto.mono_right, Filter.Tendsto.comp, UpperHalfPlane.tendsto_coe_atImInfty
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
τ : ℍ
hh : h ≠ 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ cuspFunction h f (𝕢 h (↑τ : ℂ)) = f τ

Tactic:
simpa [cuspFunction] using (Periodic.eq_cuspFunction hh hfper τ)

Premises used: UpperHalfPlane.coe, UpperHalfPlane.cuspFunction, Function.Periodic.eq_cuspFunction
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
inr : ∀ (hq' : q ≠ 0), DifferentiableAt ℂ (cuspFunction h f) q
⊢ DifferentiableAt ℂ (cuspFunction h f) 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 : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
hq : norm (E := ℂ) 0 < 1
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
hfper.differentiableAt_cuspFunction_zero hh
      (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
        (fun z hz ↦ UpperHalfPlane.mdifferentiableAt_iff.mp (hfhol ⟨z, hz⟩)))
      (hfbdd.comp_tendsto tendsto_comap_im_ofComplex)

Premises used: UpperHalfPlane.cuspFunction, UpperHalfPlane.mk, Filter.Ioi_mem_atTop, Filter.eventually_of_mem, Filter.preimage_mem_comap, Iff.mp, Asymptotics.IsBigO.comp_tendsto, UpperHalfPlane.mdifferentiableAt_iff, OfNat.ofNat, Function.Periodic.differentiableAt_cuspFunction_zero, UpperHalfPlane.tendsto_comap_im_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
hq : norm (E := ℂ) 0 < 1
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
exact hfper.differentiableAt_cuspFunction_zero hh
      (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
        (fun z hz ↦ UpperHalfPlane.mdifferentiableAt_iff.mp (hfhol ⟨z, hz⟩)))
      (hfbdd.comp_tendsto tendsto_comap_im_ofComplex)

Premises used: UpperHalfPlane.mk, Filter.Ioi_mem_atTop, Filter.eventually_of_mem, Filter.preimage_mem_comap, Iff.mp, Asymptotics.IsBigO.comp_tendsto, UpperHalfPlane.mdifferentiableAt_iff, OfNat.ofNat, Function.Periodic.differentiableAt_cuspFunction_zero, UpperHalfPlane.tendsto_comap_im_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
hq' : q ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
exact Periodic.qParam_right_inv hh.ne' hq' ▸
      hfper.differentiableAt_cuspFunction hh.ne' <| UpperHalfPlane.mdifferentiableAt_iff.mp <|
        hfhol ⟨_, Periodic.im_invQParam_pos_of_norm_lt_one hh hq hq'⟩

Premises used: UpperHalfPlane.mk, Function.Periodic.im_invQParam_pos_of_norm_lt_one, Iff.mp, UpperHalfPlane.mdifferentiableAt_iff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ DifferentiableOn ℂ (cuspFunction h f) (ball 0 1)

Tactic:
fun _ hz ↦ (differentiableAt_cuspFunction hh hfper hfhol hfbdd <| mem_ball_zero_iff.mp hz)
    |>.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, UpperHalfPlane.differentiableAt_cuspFunction, DifferentiableOn, Iff.mp, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ Membership.mem (γ := Filter ℂ) (𝓝 0) (ball 0 1)

Tactic:
simpa [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one

Premises used: ball_zero_eq, Metric.ball_mem_nhds, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ cuspFunction h f 0 = valueAtInfty f

Tactic:
(Tendsto.limUnder_eq ?_).symm

Premises used: UpperHalfPlane.valueAtInfty, Eq.symm, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
refine : Tendsto f atImInfty (𝓝 (cuspFunction h f 0))
⊢ cuspFunction h f 0 = valueAtInfty f

Tactic:
refine (Tendsto.limUnder_eq ?_).symm

Premises used: Eq.symm, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
h₁ : ∀ (τ : ℍ), (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) τ = f τ
⊢ (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) = f

Tactic:
funext τ
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
τ : ℍ
⊢ (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) τ = f τ

Tactic:
simpa using eq_cuspFunction τ hh.ne' hfper

Premises used: UpperHalfPlane.eq_cuspFunction, LT.lt.ne'
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
⊢ (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) = f

Tactic:
have : (cuspFunction h f ∘ fun τ ↦ 𝕢 h τ : ℍ → ℂ) = f := by
    funext τ
    simpa using eq_cuspFunction τ hh.ne' hfper
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ (↑ofComplex : ℂ → ℍ)) (↑h : ℂ)
this : (cuspFunction h f ∘ fun (τ : ℍ) ↦ 𝕢 h (↑τ : ℂ)) = f
⊢ Tendsto f atImInfty (𝓝 (cuspFunction h f 0))

Tactic:
simpa [this] using hfanalytic.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)

Premises used: UpperHalfPlane.qParam_tendsto_atImInfty, ContinuousAt.tendsto, AnalyticAt.continuousAt, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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)
neg :
  ∀ (hw : w.im ≤ 0),
    Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
      (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)
⊢ Eq (α := ℂ) (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (w + (↑h : ℂ)))
    (((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) w)

Tactic:
by_cases! hw : 0 < im w

Premises used: Complex.im
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ 0 < (w + (↑h : ℂ)).im

Tactic:
simp [hw]