awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
f : ModularForm 𝒢 0
⊢ ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c

Tactic:
eq_const_of_weight_zero₀ (𝒢 := 𝒢 ⊓ 𝒮ℒ) {
    toFun := f
    holo' := f.holo'
    bdd_at_cusps' hc := f.bdd_at_cusps' (hc.mono inf_le_left)
    slash_action_eq' γ hγ := f.slash_action_eq' γ hγ.1 }

Premises used: SlashInvariantForm.slash_action_eq', ModularForm.toSlashInvariantForm, _private.0.ModularForm.eq_const_of_weight_zero₀, IsCusp.mono, SlashInvariantForm.mk, And.left, ModularForm.mk, ModularForm.holo', inf_le_left, DFunLike.coe, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ ∀ (a : ℍ), (↑a.im : ℂ) ≠ 0 ∨ 0 ≤ k

Tactic:
simp [im_ne_zero _]

Premises used: UpperHalfPlane.im_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
funProp : ∀ (a : ℂ), a ≠ 0 ∨ 0 ≤ k
funProp₁ : ∀ (a : ℍ), (↑a.im : ℂ) ≠ 0 ∨ 0 ≤ k
⊢ Continuous (Y := ℂ) fun (τ : ℍ) ↦
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (f τ) : ℂ) (f' τ) * (↑τ.im : ℂ) ^ k

Tactic:
fun_prop (disch := simp [im_ne_zero _])

Premises used: UpperHalfPlane.im_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
set :
  let D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|;
  petersson k (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f') τ =
    HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2)) ((σ g : (a : ℂ) → ℂ) (petersson k f f' (g • τ)) : ℂ)
⊢ petersson k (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f') τ =
    HMul.hMul (β := ℂ) ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 2))
      ((σ g : (a : ℂ) → ℂ) (petersson k f f' (g • τ)) : ℂ)

Tactic:
set D := |g.det.val|

Premises used: Units.val, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
⊢ (↑D : ℂ) ≠ 0

Tactic:
have hD : (D : ℂ) ≠ 0 := mod_cast abs_ne_zero.mpr g.det_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ k - 2 + k = k - 1 + (k - 1)

Tactic:
abel
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
simp :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
          (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (denom g (↑τ : ℂ)) : ℂ) k)⁻¹ *
        (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
          (denom g (↑τ : ℂ) ^ k)⁻¹) *
      (↑τ.im : ℂ) ^ k =
    HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 1) * (↑D : ℂ) ^ (k - 1))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * ((j ^ k)⁻¹ * (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) j : ℂ) k)⁻¹))
⊢ petersson k (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f') τ =
    HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2 + k))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ (-k))

Tactic:
simp [Complex.normSq_eq_conj_mul_self, (by abel : k - 2 + k = (k - 1) + (k - 1)), petersson,
      zpow_add₀ hD, mul_zpow, ModularForm.slash_def, -Matrix.GeneralLinearGroup.val_det_apply]

Premises used: mul_zpow, zpow_add₀, UpperHalfPlane.petersson, Complex.normSq_eq_conj_mul_self, ModularForm.slash_def, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
          (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (denom g (↑τ : ℂ)) : ℂ) k)⁻¹ *
        (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
          (denom g (↑τ : ℂ) ^ k)⁻¹) *
      (↑τ.im : ℂ) ^ k =
    HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 1) * (↑D : ℂ) ^ (k - 1))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * ((j ^ k)⁻¹ * (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) j : ℂ) k)⁻¹))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
rw :
  HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2) * (↑D : ℂ) ^ k)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * ((↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ k)⁻¹) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) ^ k * (↑τ.im : ℂ) ^ k * ((↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ k)⁻¹))
⊢ HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2 + k))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ (-k)) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k)

Tactic:
rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]

Premises used: div_zpow, mul_zpow, div_eq_mul_inv, zpow_add₀, zpow_neg
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2) * (↑D : ℂ) ^ k)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * ((↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ k)⁻¹) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) ^ k * (↑τ.im : ℂ) ^ k * ((↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ k)⁻¹))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
rw :
  (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        (↑(HDiv.hDiv (β := ℝ) (|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * τ.im)
                ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑τ : ℂ)) : ℝ)) :
            ℂ) ^
          k)
rw₁ :
  (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑(|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * τ.im) : ℂ) /
            (↑((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑τ : ℂ))) : ℂ)) ^
          k)
rw₂ rw₃ :
  (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) * (↑τ.im : ℂ) /
            (↑((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑τ : ℂ))) : ℂ)) ^
          k)
⊢ (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        (↑(g • τ).im : ℂ) ^ k)

Tactic:
rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]

Premises used: UpperHalfPlane.im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        (↑(g • τ).im : ℂ) ^ k) =
    HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2)) ((σ g : (a : ℂ) → ℂ) (petersson k f f' (g • τ)) : ℂ)

Tactic:
simp [petersson, σ_conj]

Premises used: UpperHalfPlane.petersson, UpperHalfPlane.σ_conj
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
g : SL(2, ℤ)
τ : ℍ
⊢ petersson k (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f') τ =
    petersson k f f' (g • τ)

Tactic:
simp [σ, ModularForm.SL_slash, petersson_slash,
    -Matrix.SpecialLinearGroup.map_apply_coe, -Matrix.SpecialLinearGroup.coe_matrix_coe]

Premises used: ModularForm.SL_slash, Matrix.SpecialLinearGroup.map_apply_coe, UpperHalfPlane.σ, Matrix.SpecialLinearGroup.coe_matrix_coe, UpperHalfPlane.petersson_slash
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
τ : ℍ
⊢ petersson k f' f τ = (starRingEnd ℂ : (a : ℂ) → ℂ) (petersson k f f' τ)

Tactic:
simp [petersson, mul_comm]

Premises used: UpperHalfPlane.petersson, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
k : ℤ
f f' : ℍ → ℂ
τ : ℍ
⊢ ‖petersson k f' f τ‖ = ‖petersson k f f' τ‖

Tactic:
simp [petersson_symm k f]

Premises used: UpperHalfPlane.petersson_symm
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : SlashInvariantFormClass F Γ k
f : F
inst_4 : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
rw : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
| ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖

Tactic:
rw [← slash_action_eq f _ hg, ← slash_action_eq f' _ hg, petersson_slash,
    Subgroup.HasDetPlusMinusOne.abs_det hg, Complex.ofReal_one, one_zpow, one_mul, norm_σ]

Premises used: one_zpow, UpperHalfPlane.norm_σ, Complex.ofReal_one, Subgroup.HasDetPlusMinusOne.abs_det, SlashInvariantFormClass.slash_action_eq, one_mul, UpperHalfPlane.petersson_slash
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : SlashInvariantFormClass F Γ k
f : F
inst_4 : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
conv_rhs :
  ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖ = ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
conv_rhs₁ :
  ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖ =
    ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
⊢ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖ = ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖

Tactic:
conv_rhs => rw [← slash_action_eq f _ hg, ← slash_action_eq f' _ hg, petersson_slash,
    Subgroup.HasDetPlusMinusOne.abs_det hg, Complex.ofReal_one, one_zpow, one_mul, norm_σ]

Premises used: one_zpow, UpperHalfPlane.norm_σ, Complex.ofReal_one, Subgroup.HasDetPlusMinusOne.abs_det, SlashInvariantFormClass.slash_action_eq, one_mul, UpperHalfPlane.petersson_slash
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Γ.HasDetOne
inst_3 : SlashInvariantFormClass F Γ k
f : F
inst_4 : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ) = petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ

Tactic:
simpa [SlashInvariantFormClass.slash_action_eq _ _ hg, Subgroup.HasDetOne.det_eq hg, σ]
    using (petersson_slash k f f' g τ).symm

Premises used: Subgroup.HasDetOne.det_eq, UpperHalfPlane.σ, Eq.symm, DFunLike.coe, SlashInvariantFormClass.slash_action_eq, UpperHalfPlane.petersson_slash
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
obtain :
  ∀ (b : ℝ) (hb : b > 0)
    (hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)),
    ∃ a > 0,
      IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
obtain ⟨b, hb, hbf⟩ := ModularFormClass.exp_decay_atImInfty' f h_bd

Premises used: ModularFormClass.exp_decay_atImInfty'
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
obtain :
  ∀ (a : ℝ) (ha : 0 < a) (ha' : a < b),
    ∃ a > 0,
      IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
obtain ⟨a, ha, ha'⟩ := exists_between hb

Premises used: exists_between
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
right :
  IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
use a, ha
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
right :
  IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) x‖)
    fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
apply IsBigO.of_norm_left

Premises used: Asymptotics.IsBigO.of_norm_left
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
right :
  IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
    fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) x‖)
    fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
simp_rw [petersson, norm_mul, Complex.norm_conj, mul_comm ‖f _‖ ‖f' _‖, norm_zpow, mul_assoc,
      Complex.norm_real, Real.norm_of_nonneg (fun {τ : ℍ} ↦ τ.im_pos).le]

Premises used: Complex.norm_conj, Norm.norm, UpperHalfPlane.im_pos, mul_assoc, LT.lt.le, norm_mul, Complex.norm_real, UpperHalfPlane.petersson, mul_comm, norm_zpow, DFunLike.coe, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
h : ∀ (τ : ℍ), Real.exp (-a * τ.im)
| fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
enter [τ]
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
τ : ℍ
h : 1 * Real.exp (-a * τ.im)
| Real.exp (-a * τ.im)

Tactic:
rw [← one_mul (Real.exp _)]

Premises used: Real.exp, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
h : ∀ (τ : ℍ), 1 * Real.exp (-a * τ.im)
| fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
enter [τ]; rw [← one_mul (Real.exp _)]

Premises used: Real.exp, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
right :
  IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
    fun (τ : ℍ) ↦ 1 * Real.exp (-a * τ.im)
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ norm (E := ℂ) ((f' : (a : ℍ) → ℂ) x : ℂ) * (norm (E := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) * x.im ^ k))
    fun (τ : ℍ) ↦ Real.exp (-a * τ.im)

Tactic:
conv_rhs => enter [τ]; rw [← one_mul (Real.exp _)]

Premises used: Real.exp, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.Petersson
Goal:
F : Type u_1
F' : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_2 : Fact (IsCusp OnePoint.infty Γ)
inst_3 : Γ.HasDetPlusMinusOne
inst_4 : DiscreteTopology ↥Γ
inst_5 : ModularFormClass F Γ k
inst_6 : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
f' : F'
b : ℝ
hb : b > 0
hbf : IsBigO (E := ℂ) (F := ℝ) atImInfty (⇑f : (a : ℍ) → ℂ) fun (τ : ℍ) ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ IsBoundedAtImInfty (α := ℂ) (⇑f' : (a : ℍ) → ℂ)

Tactic:
have hf' : IsBoundedAtImInfty f' := ModularFormClass.bdd_at_infty f'