awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖f x‖) 1
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦
      ‖HPow.hPow (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) (k - 1)‖ *
          ‖(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ^ (-k)‖ *
        ‖f (g • x)‖)
    1

Tactic:
apply (hf.comp_tendsto (tendsto_smul_atImInfty hg)).const_mul_left

Premises used: UpperHalfPlane.tendsto_smul_atImInfty, Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
rw :
  (∀ (b : GL (Fin 2) ℝ),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) ∞ =
          g • c →
        IsBoundedAtImInfty
          (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
            (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) f)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ),
      HSMul.hSMul (β := OnePoint ℝ) g_1 ∞ = c →
        IsBoundedAtImInfty
          (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g_1
            (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f))
⊢ (g • c).IsBoundedAt f k ↔
    c.IsBoundedAt (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f) k

Tactic:
rw [IsBoundedAt, IsBoundedAt, (Equiv.mulLeft g⁻¹).forall_congr_left]

Premises used: OnePoint.IsBoundedAt, Equiv.forall_congr_left, Equiv.mulLeft, Inv.inv
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (b : GL (Fin 2) ℝ),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) ∞ =
          g • c →
        IsBoundedAtImInfty
          (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
            (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) f)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ),
      HSMul.hSMul (β := OnePoint ℝ) g_1 ∞ = c →
        IsBoundedAtImInfty
          (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g_1
            (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f))

Tactic:
simp [mul_smul, ← SlashAction.slash_mul]

Premises used: SlashAction.slash_mul, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
rw :
  (∀ (b : GL (Fin 2) ℝ),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) ∞ =
          g • c →
        IsZeroAtImInfty
          (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
            (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) f)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ),
      HSMul.hSMul (β := OnePoint ℝ) g_1 ∞ = c →
        IsZeroAtImInfty
          (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g_1
            (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f))
⊢ (g • c).IsZeroAt f k ↔
    c.IsZeroAt (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f) k

Tactic:
rw [IsZeroAt, IsZeroAt, (Equiv.mulLeft g⁻¹).forall_congr_left]

Premises used: Equiv.forall_congr_left, OnePoint.IsZeroAt, Equiv.mulLeft, Inv.inv
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (b : GL (Fin 2) ℝ),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) ∞ =
          g • c →
        IsZeroAtImInfty
          (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
            (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
            ((Equiv.symm (Equiv.mulLeft g⁻¹) : (a : GL (Fin 2) ℝ) → GL (Fin 2) ℝ) b : GL (Fin 2) ℝ) f)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ),
      HSMul.hSMul (β := OnePoint ℝ) g_1 ∞ = c →
        IsZeroAtImInfty
          (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g_1
            (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f))

Tactic:
simp [mul_smul, ← SlashAction.slash_mul]

Premises used: SlashAction.slash_mul, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
f' : ℍ → ℂ
hf : c.IsBoundedAt f k
hf' : c.IsBoundedAt f' k
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g ∞ = c
⊢ IsBoundedAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f + f'))

Tactic:
simpa using (hf g hg).add (hf' g hg)

Premises used: Filter.BoundedAtFilter.add
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
f' : ℍ → ℂ
hf : c.IsZeroAt f k
hf' : c.IsZeroAt f' k
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g ∞ = c
⊢ IsZeroAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f + f'))

Tactic:
simpa using (hf g hg).add (hf' g hg)

Premises used: Filter.ZeroAtFilter.add
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
h : IsBoundedAt ∞ f k
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) 1 ∞ = ∞

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
h : IsBoundedAt ∞ f k
⊢ IsBoundedAtImInfty f

Tactic:
simpa using h 1 (by simp)

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
h : IsZeroAt ∞ f k
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) 1 ∞ = ∞

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
h : IsZeroAt ∞ f k
⊢ IsZeroAtImInfty f

Tactic:
simpa using h 1 (by simp)

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g ∞ = c
⊢ IsBoundedAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f) →
    c.IsBoundedAt f k

Tactic:
simp [← hg, IsBoundedAt.smul_iff, isBoundedAt_infty_iff]

Premises used: OnePoint.isBoundedAt_infty_iff, OnePoint.IsBoundedAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g ∞ = c
⊢ IsZeroAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f) →
    c.IsZeroAt f k

Tactic:
simp [← hg, IsZeroAt.smul_iff, isZeroAt_infty_iff]

Premises used: OnePoint.isZeroAt_infty_iff, OnePoint.IsZeroAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
mp :
  c.IsBoundedAt f k →
    ∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)
mpr :
  (∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)) →
    c.IsBoundedAt f k
⊢ c.IsBoundedAt f k ↔
    ∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
mp :
  ∀ (γ : SL(2, ℤ))
    (hc :
      IsCusp
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞)
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))),
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
            ∞).IsBoundedAt
        f k →
      ∃ (γ_1 : SL(2, ℤ)),
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ)
              ∞ =
            HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ ∧
          IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)
⊢ c.IsBoundedAt f k →
    ∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)

Tactic:
obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc

Premises used: isCusp_SL2Z_iff', Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞)
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞).IsBoundedAt
      f k →
    ∃ (γ_1 : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ)
            ∞ =
          HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
            ∞ ∧
        IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)

Tactic:
simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using fun hfc ↦ ⟨γ, rfl, hfc⟩

Premises used: OnePoint.isBoundedAt_infty_iff, OnePoint.IsBoundedAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
b : IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞)
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
        ∞).IsBoundedAt
    f k

Tactic:
simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using b

Premises used: OnePoint.isBoundedAt_infty_iff, OnePoint.IsBoundedAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
mp :
  c.IsZeroAt f k →
    ∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)
mpr :
  (∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)) →
    c.IsZeroAt f k
⊢ c.IsZeroAt f k ↔
    ∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
mp :
  ∀ (γ : SL(2, ℤ))
    (hc :
      IsCusp
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞)
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))),
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
            ∞).IsZeroAt
        f k →
      ∃ (γ_1 : SL(2, ℤ)),
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ)
              ∞ =
            HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ ∧
          IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)
⊢ c.IsZeroAt f k →
    ∃ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c ∧
        IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)

Tactic:
obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc

Premises used: isCusp_SL2Z_iff', Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞)
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞).IsZeroAt
      f k →
    ∃ (γ_1 : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ)
            ∞ =
          HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
            ∞ ∧
        IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)

Tactic:
simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using fun hfc ↦ ⟨γ, rfl, hfc⟩

Premises used: OnePoint.isZeroAt_infty_iff, OnePoint.IsZeroAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
b : IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞)
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
        ∞).IsZeroAt
    f k

Tactic:
simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using b

Premises used: OnePoint.isZeroAt_infty_iff, OnePoint.IsZeroAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc_1 : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
hc : c.IsBoundedAt f k
x : SL(2, ℤ)
hγ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ) ∞ = c
⊢ IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f)

Tactic:
simpa using hc _ hγ
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
refine :
  ∀
    (h :
      ∀ (γ : SL(2, ℤ)),
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
              ∞ =
            c →
          IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)),
    c.IsBoundedAt f k
⊢ c.IsBoundedAt f k ↔
    ∀ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c →
        IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)

Tactic:
refine ⟨fun hc _ hγ ↦ by simpa using hc _ hγ, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
h :
  ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
        c →
      IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)
obtain :
  ∀ (γ : SL(2, ℤ))
    (hc :
      IsCusp
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞)
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)))
    (h :
      ∀ (γ_1 : SL(2, ℤ)),
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ)
              ∞ =
            HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ →
          IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)),
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞).IsBoundedAt
      f k
⊢ c.IsBoundedAt f k

Tactic:
obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc

Premises used: isCusp_SL2Z_iff', Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞)
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
h :
  ∀ (γ_1 : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ) ∞ =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞ →
      IsBoundedAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
        ∞).IsBoundedAt
    f k

Tactic:
simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using h γ rfl

Premises used: OnePoint.isBoundedAt_infty_iff, OnePoint.IsBoundedAt.smul_iff, rfl
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc_1 : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
hc : c.IsZeroAt f k
x : SL(2, ℤ)
hγ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ) ∞ = c
⊢ IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f)

Tactic:
simpa using hc _ hγ
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
refine :
  ∀
    (h :
      ∀ (γ : SL(2, ℤ)),
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
              ∞ =
            c →
          IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)),
    c.IsZeroAt f k
⊢ c.IsZeroAt f k ↔
    ∀ (γ : SL(2, ℤ)),
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
          c →
        IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)

Tactic:
refine ⟨fun hc _ hγ ↦ by simpa using hc _ hγ, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
h :
  ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
        c →
      IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f)
obtain :
  ∀ (γ : SL(2, ℤ))
    (hc :
      IsCusp
        (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞)
        (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)))
    (h :
      ∀ (γ_1 : SL(2, ℤ)),
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ)
              ∞ =
            HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
              ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ →
          IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)),
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞).IsZeroAt
      f k
⊢ c.IsZeroAt f k

Tactic:
obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc

Premises used: isCusp_SL2Z_iff', Iff.mp, rfl
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
hc :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞)
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
h :
  ∀ (γ_1 : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ_1 : GL (Fin 2) ℝ) ∞ =
        HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
          ∞ →
      IsZeroAtImInfty (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ_1 f)
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)
        ∞).IsZeroAt
    f k

Tactic:
simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using h γ rfl

Premises used: OnePoint.isZeroAt_infty_iff, OnePoint.IsZeroAt.smul_iff, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
obtain :
  ∀ (D : ℝ) (hD : D > 0) (hf_infinity : IsBigOWith (F := ℝ) D atImInfty f fun (z : ℍ) ↦ z.im ^ t),
    ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
obtain ⟨D, hD, hf_infinity⟩ := hf_infinity.exists_pos

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity_1 : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : IsBigOWith (F := ℝ) D atImInfty f fun (z : ℍ) ↦ z.im ^ t
⊢ ∃ (a : ℝ), ∀ b ≥ a, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖

Tactic:
rw [IsBigOWith, atImInfty, eventually_comap, eventually_atTop] at hf_infinity

Premises used: Asymptotics.IsBigOWith, UpperHalfPlane.atImInfty, Filter.eventually_comap, Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity_1 : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : ∃ (a : ℝ), ∀ b ≥ a, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖
obtain :
  ∀ (y : ℝ) (hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖), ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
obtain ⟨y, hy⟩ := hf_infinity