awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
⊢ IsBoundedAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))
have rw : (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞).IsBoundedAt
  (⇑f : (a : ℍ) → ℂ) k
Tactic: rw [← OnePoint.isBoundedAt_infty_iff, SL_slash, ← OnePoint.IsBoundedAt.smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞).IsBoundedAt
    (⇑f : (a : ℍ) → ℂ) k
have apply : IsCusp
  (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
    ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ) ∞)
  Γ
Tactic: apply bdd_at_cusps f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
⊢ IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞)
    Γ
have rw : ∃ (g_1 : SL(2, ℤ)),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞
Tactic: rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
⊢ IsZeroAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))
have rw : (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞).IsZeroAt
  (⇑f : (a : ℍ) → ℂ) k
Tactic: rw [← OnePoint.isZeroAt_infty_iff, SL_slash, ← OnePoint.IsZeroAt.smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞).IsZeroAt
    (⇑f : (a : ℍ) → ℂ) k
have apply : IsCusp
  (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
    ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ) ∞)
  Γ
Tactic: apply zero_at_cusps f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
⊢ IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞)
    Γ
have rw : ∃ (g_1 : SL(2, ℤ)),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞
Tactic: rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : IsZeroAtImInfty f
⊢ IsZeroAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
have rw : ∀ (hf : Tendsto (β := ℝ) (fun (x : ℍ) ↦ ‖f x‖) atImInfty (nhds 0)),
  Tendsto (β := ℝ)
    (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) atImInfty
    (nhds 0)
Tactic: rw [IsZeroAtImInfty, ZeroAtFilter, tendsto_zero_iff_norm_tendsto_zero] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : IsBoundedAtImInfty f
⊢ IsBoundedAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
have rw : ∀ (hf : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖f x‖) 1),
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) 1
Tactic: rw [IsBoundedAtImInfty, BoundedAtFilter, ← Asymptotics.isBigO_norm_left] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
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 : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) 1
have suffices : 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: suffices (fun x ↦ (‖g.det.val ^ (k - 1)‖ * ‖g 1 1 ^ (-k)‖) * ‖f (g • x)‖) =O[atImInfty] 1 by
    simpa [ModularForm.slash_def, denom, hg, mul_assoc, mul_comm ‖f _‖]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (g • c).IsBoundedAt f k ↔
    c.IsBoundedAt (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f) k
have 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))
Tactic: rw [IsBoundedAt, IsBoundedAt, (Equiv.mulLeft g⁻¹).forall_congr_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (g • c).IsZeroAt f k ↔
    c.IsZeroAt (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f) k
have 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))
Tactic: rw [IsZeroAt, IsZeroAt, (Equiv.mulLeft g⁻¹).forall_congr_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ 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)
have 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)
Tactic: obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ 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)
have 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)
Tactic: obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ 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)
have 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
Tactic: refine ⟨fun hc _ hγ ↦ by simpa using hc _ hγ, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
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)
⊢ c.IsBoundedAt f k
have 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
Tactic: obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
Goal:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ 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)
have 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
Tactic: refine ⟨fun hc _ hγ ↦ by simpa using hc _ hγ, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.BoundedAtCusp (goal)
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)
⊢ c.IsZeroAt f k
have 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
Tactic: obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
have obtain : ∀ (D : ℝ) (hD : D > 0) (hf_infinity : IsBigOWith (F := ℝ) D atImInfty f fun (z : ℍ) ↦ z.im ^ t),
  ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Tactic: obtain ⟨D, hD, hf_infinity⟩ := hf_infinity.exists_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
have hf_infinity₁ : ∃ (a : ℝ), ∀ b ≥ a, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖
Tactic: rw [IsBigOWith, atImInfty, eventually_comap, eventually_atTop] at hf_infinity
Cleared hypotheses: hf_infinity
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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‖
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
have obtain : ∀ (y : ℝ) (hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖), ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Tactic: obtain ⟨y, hy⟩ := hf_infinity
Cleared hypotheses: hf_infinity
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
have hy₁ : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
Tactic: simp only [Real.norm_rpow_of_nonneg (_ : ℍ).im_pos.le,
      Real.norm_of_nonneg (_ : ℍ).im_pos.le] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
⊢ ContinuousOn (Y := ℝ) (fun (τ : ℍ) ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
have apply : Continuous (Y := ℝ) fun (τ : ℍ) ↦ τ.im ^ t
Tactic: apply (hf_cont.norm.div ?_ fun τ ↦ by positivity).continuousOn
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (hypothesis)
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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
have hfm : ContinuousOn (Y := ℝ) (fun (τ : ℍ) ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
Tactic: have hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / (im τ) ^ t) (truncatedFundamentalDomain y) := by
    apply (hf_cont.norm.div ?_ fun τ ↦ by positivity).continuousOn
    exact continuous_im.rpow_const fun τ ↦ .inl τ.im_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (Y := ℝ) (fun (τ : ℍ) ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
have obtain : ∀ (E_1 : ℝ) (hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E_1), ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Tactic: obtain ⟨E, hE⟩ : ∃ E, ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / (im τ) ^ t ≤ E := by
    simpa [norm_mul, norm_norm, Real.norm_rpow_of_nonneg (_ : ℍ).im_pos.le,
      Real.norm_of_nonneg (_ : ℍ).im_pos.le]
      using (isCompact_truncatedFundamentalDomain y).exists_bound_of_continuousOn hfm