awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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)
⊢ (↑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)
have 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)
Tactic: rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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)
⊢ (↑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)
have 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)
Tactic: rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom 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 • τ)) : ℂ)
have calc : 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: calc petersson k (f ∣[k] g) (f' ∣[k] g) τ
  _ = D ^ (k - 2 + k) * conj (σ g (f (g • τ))) * σ g (f' (g • τ))
      * (τ.im ^ k * j.normSq ^ (-k)) := by
    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]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (D * τ.im / j.normSq) ^ k) := by
    rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (im (g • τ)) ^ k) := by
    rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
  _ = D ^ (k - 2) * σ g (petersson k f f' (g • τ)) := by simp [petersson, σ_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
calc :
  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))
⊢ 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 • τ)) : ℂ)
have calc₁ : 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: calc petersson k (f ∣[k] g) (f' ∣[k] g) τ
  _ = D ^ (k - 2 + k) * conj (σ g (f (g • τ))) * σ g (f' (g • τ))
      * (τ.im ^ k * j.normSq ^ (-k)) := by
    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]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (D * τ.im / j.normSq) ^ k) := by
    rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (im (g • τ)) ^ k) := by
    rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
  _ = D ^ (k - 2) * σ g (petersson k f f' (g • τ)) := by simp [petersson, σ_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
calc :
  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))
calc₁ :
  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)
⊢ 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 • τ)) : ℂ)
have calc₂ : (↑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: calc petersson k (f ∣[k] g) (f' ∣[k] g) τ
  _ = D ^ (k - 2 + k) * conj (σ g (f (g • τ))) * σ g (f' (g • τ))
      * (τ.im ^ k * j.normSq ^ (-k)) := by
    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]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (D * τ.im / j.normSq) ^ k) := by
    rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (im (g • τ)) ^ k) := by
    rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
  _ = D ^ (k - 2) * σ g (petersson k f f' (g • τ)) := by simp [petersson, σ_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
calc :
  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))
calc₁ :
  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)
calc₂ :
  (↑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)
⊢ 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 • τ)) : ℂ)
have calc₃ : (↑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: calc petersson k (f ∣[k] g) (f' ∣[k] g) τ
  _ = D ^ (k - 2 + k) * conj (σ g (f (g • τ))) * σ g (f' (g • τ))
      * (τ.im ^ k * j.normSq ^ (-k)) := by
    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]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (D * τ.im / j.normSq) ^ k) := by
    rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
    ring
  _ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (im (g • τ)) ^ k) := by
    rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
  _ = D ^ (k - 2) * σ g (petersson k f f' (g • τ)) := by simp [petersson, σ_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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 ∈ Γ
| ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
have rw : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
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_σ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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 ∈ Γ
⊢ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖ = ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
have conv_rhs : ‖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_σ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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 : ℍ) → ℂ) τ‖
⊢ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖ = ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) τ‖
have conv_rhs₁ : ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖ =
  ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) (g • τ)‖
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_σ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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'
⊢ ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have 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)
Tactic: obtain ⟨b, hb, hbf⟩ := ModularFormClass.exp_decay_atImInfty' f h_bd
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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 > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have obtain : ∀ (a : ℝ) (ha : 0 < a) (ha' : a < b),
  ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
Tactic: obtain ⟨a, ha, ha'⟩ := exists_between hb
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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
⊢ ∃ a > 0,
    IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have right : IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
Tactic: use a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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
⊢ IsBigO (F := ℝ) atImInfty (petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ)) fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have right : IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) x‖) fun (τ : ℍ) ↦
  Real.exp (-a * τ.im)
Tactic: apply IsBigO.of_norm_left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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
⊢ IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖petersson k (⇑f : (a : ℍ) → ℂ) (⇑f' : (a : ℍ) → ℂ) x‖)
    fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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
| fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have h : ∀ (τ : ℍ), Real.exp (-a * τ.im)
Tactic: enter [τ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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
τ : ℍ
| Real.exp (-a * τ.im)
have h : 1 * Real.exp (-a * τ.im)
Tactic: rw [← one_mul (Real.exp _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
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
| fun (τ : ℍ) ↦ Real.exp (-a * τ.im)
have h : ∀ (τ : ℍ), 1 * Real.exp (-a * τ.im)
Tactic: enter [τ]; rw [← one_mul (Real.exp _)]