awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
have refine : ∀ (τ : ℍ) (hτ : τ ∈ 𝒟), ‖f τ‖ ≤ max D E * τ.im ^ t
Tactic: refine ⟨max D E, fun τ hτ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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τ : τ ∈ 𝒟
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t
have inl : ∀ (hτ' : y ≤ τ.im), ‖f τ‖ ≤ max D E * τ.im ^ t
Tactic: rcases le_total y (im τ) with hτ' | hτ'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t
have inr : ∀ (hτ' : τ.im ≤ y), ‖f τ‖ ≤ max D E * τ.im ^ t
Tactic: rcases le_total y (im τ) with hτ' | hτ'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Bounds (goal)
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 τ‖ ≤ max D E * τ.im ^ t
have inr : ‖f τ‖ / τ.im ^ t ≤ max D E
Tactic: rw [← div_le_iff₀ (by positivity)]
-- 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 : ℝ
ht : 0 ≤ t
hf_infinity : IsBigO (F := ℝ) atImInfty f fun (z : ℍ) ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ ∃ (C : ℝ), ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
have obtain : ∀ (F : ℝ) (hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.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
-- 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 : ℝ
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
have refine : ∀ (τ : ℍ), ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
Tactic: refine ⟨F, fun τ ↦ ?_⟩
-- 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 : ℝ
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
τ : ℍ
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
have obtain : ∀ (g : SL(2, ℤ)) (hg : g • τ ∈ 𝒟), ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
Tactic: obtain ⟨g, hg⟩ := exists_smul_mem_fd τ
-- 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 : ℝ
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 τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
have hF𝒟₁ : ‖f (g • τ)‖ ≤ F * (g • τ).im ^ t
Tactic: specialize hF𝒟 (g • τ) hg
Cleared hypotheses: hF𝒟
-- 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 : ℝ
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 * max τ.im (1 / τ.im) ^ t
have hF𝒟₁ : ‖f τ‖ ≤ F * (g • τ).im ^ t
Tactic: rw [hf_inv g τ] at hF𝒟
Cleared hypotheses: hF𝒟
-- 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 : ℝ
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 τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
have grw : F * (g • τ).im ^ t ≤ F * max τ.im (1 / τ.im) ^ t
Tactic: grw [hF𝒟]
-- 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 : ℝ
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 * max τ.im (1 / τ.im) ^ t
have ha : 0 ≤ F
Tactic: gcongr
-- 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 : ℝ
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
⊢ F * (g • τ).im ^ t ≤ F * max τ.im (1 / τ.im) ^ t
have hbc : (g • τ).im ≤ max τ.im (1 / τ.im)
Tactic: gcongr
-- 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 : ℝ
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 ≤ F
have hF𝒟₁ : ‖f τ‖ / (g • τ).im ^ t ≤ F
Tactic: rw [← div_le_iff₀ (by positivity)] at hF𝒟
Cleared hypotheses: hF𝒟
-- 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 : ℝ
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
⊢ (g • τ).im ≤ max τ.im (1 / τ.im)
have 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)
Tactic: rw [im_smul_eq_div_normSq, denom_apply]
-- 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 : ℝ
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
⊢ 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)
have 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)
Tactic: by_cases hg : g 1 0 = 0
-- 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 : ℝ
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)
⊢ 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)
have 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)
Tactic: by_cases hg : g 1 0 = 0
-- 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 : ℝ
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)
have this : (↑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
-- 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 : ℝ
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
⊢ 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)
have this₁ : 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)
-- 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 : ℝ
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)
have pos : HDiv.hDiv (β := ℝ) τ.im
    ((Complex.normSq : (a : ℂ) → ℝ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) :
      ℝ) ≤
  τ.im
Tactic: refine le_trans ?_ <| le_max_left _ _
-- 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 : ℝ
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) : ℂ)) :
        ℝ) ≤
    τ.im
have pos : τ.im / HPow.hPow (α := ℝ) (β := ℕ) (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℝ) 2 ≤ τ.im
Tactic: rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) = (g 1 1) ^ 2 by simp [hg, sq]]
-- 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 : ℝ
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)
have 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
Tactic: refine le_trans ?_ <| le_max_right _ _
-- 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 : ℝ
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) : ℂ)) :
        ℝ) ≤
    1 / τ.im
have 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
Tactic: rw [show 1 / τ.im = τ.im / τ.im ^ 2 by field_simp]
-- 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 : ℝ
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) : ℂ)) :
        ℝ) ≤
    τ.im / HPow.hPow (β := ℕ) τ.im 2
have neg : HPow.hPow (β := ℕ) τ.im 2 ≤
  (Complex.normSq : (a : ℂ) → ℝ)
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ))
Tactic: gcongr
-- 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 : ℝ
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
⊢ (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
have 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
Tactic: simp [Complex.normSq_apply]
-- 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 : ℝ
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
⊢ HPow.hPow (β := ℕ) τ.im 2 ≤
    (Complex.normSq : (a : ℂ) → ℝ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ))
have 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
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]
-- 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 : ℝ
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
⊢ 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
have this : 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)
-- 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 : ℝ
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
⊢ 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
have 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
Tactic: nlinarith
-- 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 : ℝ
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
have hgh₁ : g⁻¹ * h ∈ Γ
Tactic: rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hgh
Cleared hypotheses: hgh
-- 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 : ℝ
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
⊢ Eq.{u_1 + 1} (α := E) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) g) ((fun (g : SL(2, ℤ)) ↦ f (g⁻¹ • τ)) h)
have 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)
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⟩