awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * ‖a.im ^ t‖
⊢ ∀ 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

Premises used: UpperHalfPlane.im_pos, LT.lt.le, Real.norm_rpow_of_nonneg, Real.norm_of_nonneg
-- 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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
τ : ℍ
⊢ τ.im ^ t ≠ 0

Tactic:
positivity
-- 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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
apply : Continuous (Y := ℝ) fun (τ : ℍ) ↦ τ.im ^ t
⊢ ContinuousOn (Y := ℝ) (fun (τ : ℍ) ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)

Tactic:
apply (hf_cont.norm.div ?_ fun τ ↦ by positivity).continuousOn

Premises used: Continuous.continuousOn, Continuous.norm, Continuous.div
-- 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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
⊢ Continuous (Y := ℝ) fun (τ : ℍ) ↦ τ.im ^ t

Tactic:
continuous_im.rpow_const fun τ ↦ .inl τ.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero, UpperHalfPlane.continuous_im, Or.inl, Continuous.rpow_const
-- 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
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ b ≥ y, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
⊢ Continuous (Y := ℝ) fun (τ : ℍ) ↦ τ.im ^ t

Tactic:
exact continuous_im.rpow_const fun τ ↦ .inl τ.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero, UpperHalfPlane.continuous_im, Or.inl, Continuous.rpow_const
-- 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
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)

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
-- 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
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)
⊢ ∃ (E_1 : ℝ), ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E_1

Tactic:
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

Premises used: UpperHalfPlane.im_pos, LT.lt.le, norm_mul, norm_norm, IsCompact.exists_bound_of_continuousOn, Real.norm_rpow_of_nonneg, Real.norm_of_nonneg, ModularGroup.isCompact_truncatedFundamentalDomain
-- 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
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)
obtain :
  ∀ (E_1 : ℝ) (hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E_1),
    ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
⊢ ∃ (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

Premises used: ModularGroup.truncatedFundamentalDomain
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
⟨max D E, fun τ hτ ↦ ?_⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
refine : ∀ (τ : ℍ) (hτ : τ ∈ 𝒟), ‖f τ‖ ≤ max D E * τ.im ^ t
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
refine ⟨max D E, fun τ hτ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
inl : ∀ (hτ' : y ≤ τ.im), ‖f τ‖ ≤ max D E * τ.im ^ t
inr : ∀ (hτ' : τ.im ≤ y), ‖f τ‖ ≤ max D E * τ.im ^ t
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t

Tactic:
rcases le_total y (im τ) with hτ' | hτ'

Premises used: le_total, UpperHalfPlane.im
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : y ≤ τ.im
⊢ 0 ≤ τ.im ^ t

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : y ≤ τ.im
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t

Tactic:
exact (hy _ hτ' _ rfl).trans <| mul_le_mul_of_nonneg_right (le_max_left ..) (by positivity)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, le_max_left, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ 0 < τ.im ^ t

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
inr : ‖f τ‖ / τ.im ^ t ≤ max D E
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t

Tactic:
rw [← div_le_iff₀ (by positivity)]

Premises used: div_le_iff₀
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ ‖f τ‖ / τ.im ^ t ≤ max D E

Tactic:
(hE τ ⟨hτ, hτ'⟩).trans (le_max_right _ _)

Premises used: le_max_right, And.intro, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E_1 : Type u_1
inst : SeminormedAddCommGroup E_1
f : ℍ → E_1
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)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ ‖f τ‖ / τ.im ^ t ≤ max D E

Tactic:
exact (hE τ ⟨hτ, hτ'⟩).trans (le_max_right _ _)

Premises used: le_max_right, And.intro, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ ∃ (F : ℝ), ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
exists_bound_fundamental_domain_of_isBigO hf_cont hf_infinity

Premises used: ModularGroup.exists_bound_fundamental_domain_of_isBigO
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
obtain : ∀ (F : ℝ) (hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t), ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
obtain ⟨F, hF𝒟⟩ : ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t :=
    exists_bound_fundamental_domain_of_isBigO hf_cont hf_infinity

Premises used: ModularGroup.exists_bound_fundamental_domain_of_isBigO
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
⟨F, fun τ ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
refine : ∀ (τ : ℍ), ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
refine ⟨F, fun τ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
τ : ℍ
obtain : ∀ (g : SL(2, ℤ)) (hg : g • τ ∈ 𝒟), ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t

Tactic:
obtain ⟨g, hg⟩ := exists_smul_mem_fd τ

Premises used: ModularGroup.exists_smul_mem_fd
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
⊢ ‖f (g • τ)‖ ≤ F * (g • τ).im ^ t

Tactic:
specialize hF𝒟 (g • τ) hg

Premises used: HSMul.hSMul
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f (g • τ)‖ ≤ F * (g • τ).im ^ t
⊢ ‖f τ‖ ≤ F * (g • τ).im ^ t

Tactic:
rw [hf_inv g τ] at hF𝒟
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
grw : F * (g • τ).im ^ t ≤ F * max τ.im (1 / τ.im) ^ t
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t

Tactic:
grw [hF𝒟]
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
ha : 0 ≤ F
hbc : (g • τ).im ≤ max τ.im (1 / τ.im)
⊢ F * (g • τ).im ^ t ≤ F * max τ.im (1 / τ.im) ^ t

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
⊢ 0 < (g • τ).im ^ t

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
⊢ ‖f τ‖ / (g • τ).im ^ t ≤ F

Tactic:
rw [← div_le_iff₀ (by positivity)] at hF𝒟

Premises used: div_le_iff₀
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ / (g • τ).im ^ t ≤ F
⊢ 0 ≤ ‖f τ‖ / (g • τ).im ^ t

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ / (g • τ).im ^ t ≤ F
⊢ 0 ≤ F

Tactic:
exact le_trans (by positivity) hF𝒟

Premises used: le_trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hbc :
  HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    max τ.im (1 / τ.im)
⊢ (g • τ).im ≤ max τ.im (1 / τ.im)

Tactic:
rw [im_smul_eq_div_normSq, denom_apply]

Premises used: ModularGroup.denom_apply, ModularGroup.im_smul_eq_div_normSq
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
pos :
  ∀ (hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
    HDiv.hDiv (β := ℝ) τ.im
        ((Complex.normSq : (a : ℂ) → ℝ)
            ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
          ℝ) ≤
      max τ.im (1 / τ.im)
neg :
  ∀ (hg : ¬(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0),
    HDiv.hDiv (β := ℝ) τ.im
        ((Complex.normSq : (a : ℂ) → ℝ)
            ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
          ℝ) ≤
      max τ.im (1 / τ.im)
⊢ HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    max τ.im (1 / τ.im)

Tactic:
by_cases hg : g 1 0 = 0

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg_1 : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hg' : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
⊢ Eq (α := ℤ) 0 1

Tactic:
simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe

Premises used: sub_zero, Matrix.SpecialLinearGroup.det_coe, MulZeroClass.mul_zero, Matrix.det_fin_two
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg_1 : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0

Tactic:
have : g 1 1 ≠ 0 := fun hg' ↦ zero_ne_one <| by
      simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg_1 : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
this : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
⊢ 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2

Tactic:
have : (1 : ℝ) ≤ g 1 1 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs this)
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg_1 : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
this : 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2
⊢ HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    max τ.im (1 / τ.im)

Tactic:
le_trans ?_ <| le_max_left _ _

Premises used: le_max_left, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.Bounds
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hg_1 : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
this_1 : (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
this : 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2
pos :
  HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    τ.im
⊢ HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    max τ.im (1 / τ.im)

Tactic:
refine le_trans ?_ <| le_max_left _ _

Premises used: le_max_left, le_trans