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 : ℝ
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
⊢ (Complex.normSq : (a : ℂ) → ℝ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) =
    HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2

Tactic:
simp [hg, sq]

Premises used: sq
-- 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 : τ.im / HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2 ≤ τ.im
⊢ HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    τ.im

Tactic:
rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) = (g 1 1) ^ 2 by simp [hg, sq]]
-- 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
⊢ τ.im / HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2 ≤ τ.im

Tactic:
simpa [field] using inv_le_one_of_one_le₀ this

Premises used: inv_le_one_of_one_le₀
-- 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
⊢ 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_right _ _

Premises used: le_max_right, 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
neg :
  HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 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_right _ _

Premises used: le_max_right, 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
⊢ 1 / τ.im = τ.im / HPow.hPow (β := ℕ) τ.im 2

Tactic:
field_simp
-- 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
neg :
  HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    τ.im / HPow.hPow (β := ℕ) τ.im 2
⊢ HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    1 / τ.im

Tactic:
rw [show 1 / τ.im = τ.im / τ.im ^ 2 by field_simp]
-- 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
neg :
  HPow.hPow (β := ℕ) τ.im 2 ≤
    (Complex.normSq : (a : ℂ) → ℝ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ))
⊢ HDiv.hDiv (β := ℝ) τ.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
        ℝ) ≤
    τ.im / HPow.hPow (β := ℕ) τ.im 2

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_1 : g • τ ∈ 𝒟
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : ¬(↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
simp :
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) +
      (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.im * ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.im) =
    HPow.hPow (β := ℕ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2
⊢ (Complex.normSq : (a : ℂ) → ℝ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) =
    HPow.hPow (β := ℕ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2

Tactic:
simp [Complex.normSq_apply]

Premises used: Complex.normSq_apply
-- 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 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) +
      (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.im * ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.im) =
    HPow.hPow (β := ℕ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2

Tactic:
ring
-- 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
neg :
  HPow.hPow (β := ℕ) τ.im 2 ≤
    HPow.hPow (β := ℕ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2
⊢ HPow.hPow (β := ℕ) τ.im 2 ≤
    (Complex.normSq : (a : ℂ) → ℝ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ))

Tactic:
rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) =
      ((g 1 0) * τ.re + (g 1 1)) ^ 2 + (g 1 0) ^ 2 * τ.im ^ 2 by simp [Complex.normSq_apply]; ring]
-- 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
⊢ 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2

Tactic:
have : (1 : ℝ) ≤ g 1 0 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs hg)
-- 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 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2
nlinarith :
  HPow.hPow (β := ℕ)
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2 <
      HPow.hPow (β := ℕ) τ.im 2 →
    0 -
            HPow.hPow (β := ℕ)
              ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
          (HPow.hPow (β := ℕ)
                ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
              HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2 -
            HPow.hPow (β := ℕ) τ.im 2) +
        (0 -
          (0 - HPow.hPow (β := ℕ) τ.im 2) *
            (1 - HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2)) =
      0
⊢ HPow.hPow (β := ℕ) τ.im 2 ≤
    HPow.hPow (β := ℕ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) * τ.re + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ)) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℝ) 2 * HPow.hPow (β := ℕ) τ.im 2

Tactic:
nlinarith
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
⊢ g⁻¹ * h ∈ Γ

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hgh

Premises used: Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g⁻¹ * h ∈ Γ
⊢ ∃ j ∈ Γ, h = g * j

Tactic:
⟨g⁻¹ * h, hgh, (mul_inv_cancel_left g h).symm⟩

Premises used: HMul.hMul, Inv.inv, And.intro, Exists.intro, Eq.symm, mul_inv_cancel_left
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g⁻¹ * h ∈ Γ
⊢ ∃ j ∈ Γ, h = g * j

Tactic:
exact ⟨g⁻¹ * h, hgh, (mul_inv_cancel_left g h).symm⟩
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
obtain :
  ∀ (j : SL(2, ℤ)) (hj : j ∈ Γ) (hj' : h = g * j),
    Eq.{u_1 + 1} (α := E) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) g) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) h)
⊢ Eq.{u_1 + 1} (α := E) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) g) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) h)

Tactic:
obtain ⟨j, hj, hj'⟩ : ∃ j ∈ Γ, h = g * j := by
      rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hgh
      exact ⟨g⁻¹ * h, hgh, (mul_inv_cancel_left g h).symm⟩
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
j : SL(2, ℤ)
hj : j ∈ Γ
hj' : h = g * j
⊢ Eq.{u_1 + 1} (α := E) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) g) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) h)

Tactic:
simp [-sl_moeb, hj', mul_smul, hf_inv j⁻¹ (inv_mem hj)]

Premises used: ModularGroup.sl_moeb, InvMemClass.inv_mem, Inv.inv, SemigroupAction.mul_smul
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
γ : SL(2, ℤ) ⧸ Γ
g : SL(2, ℤ)
simp :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦
    f
      (HSMul.hSMul (α := GL (Fin 2) ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        x)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x (↑g : SL(2, ℤ) ⧸ Γ)

Tactic:
simp only [sl_moeb, Quotient.lift_mk, f']

Premises used: ModularGroup.sl_moeb, Quotient.lift_mk
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
γ : SL(2, ℤ) ⧸ Γ
g : SL(2, ℤ)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦
    f
      (HSMul.hSMul (α := GL (Fin 2) ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g⁻¹) :
          GL (Fin 2) ℝ)
        x)

Tactic:
fun_prop
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
⊢ ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ

Tactic:
have hf'_cont γ : Continuous (f' · γ) := QuotientGroup.induction_on γ fun g ↦ by
    simp only [sl_moeb, Quotient.lift_mk, f']
    fun_prop
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
τ : ℍ
g : SL(2, ℤ)
γ : SL(2, ℤ) ⧸ Γ
H : ∀ (z : SL(2, ℤ)), f' (g • τ) (HSMul.hSMul (β := SL(2, ℤ) ⧸ Γ) g (↑z : SL(2, ℤ) ⧸ Γ)) = f' τ (↑z : SL(2, ℤ) ⧸ Γ)
⊢ f' (g • τ) (g • γ) = f' τ γ

Tactic:
induction γ using QuotientGroup.induction_on
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
τ : ℍ
g z : SL(2, ℤ)
⊢ f' (g • τ) (HSMul.hSMul (β := SL(2, ℤ) ⧸ Γ) g (↑z : SL(2, ℤ) ⧸ Γ)) = f' τ (↑z : SL(2, ℤ) ⧸ Γ)

Tactic:
simp [-sl_moeb, f', mul_smul]

Premises used: ModularGroup.sl_moeb, SemigroupAction.mul_smul
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
⊢ ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ

Tactic:
have hf'_inv τ (g : SL(2, ℤ)) γ : f' (g • τ) (g • γ) = f' τ γ := by
    induction γ using QuotientGroup.induction_on
    simp [-sl_moeb, f', mul_smul]
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
⊢ ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t

Tactic:
have hf'_infty γ : (f' · γ) =O[_] _ := γ.induction_on fun h ↦ hf_infinity h⁻¹
-- 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 :
  ∀ (g : SL(2, ℤ)), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (τ : ℍ) ↦ f (g • τ)) fun (z : ℍ) ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst_1 : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : (τ : ℍ) → SL(2, ℤ) ⧸ Γ → E := fun (τ : ℍ) ↦ Quotient.lift (fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : ℍ) ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty :
  ∀ (γ : SL(2, ℤ) ⧸ Γ), IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atImInfty (fun (x : ℍ) ↦ f' x γ) fun (z : ℍ) ↦ z.im ^ t
have : ∀ (this : Fintype (SL(2, ℤ) ⧸ Γ)), ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
have : Fintype (SL(2, ℤ) ⧸ Γ) := Subgroup.fintypeQuotientOfFiniteIndex