-- 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 (↑τ : ℂ)
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)
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 • τ)) : ℂ)
⊢ 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 • τ)) : ℂ)

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]

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Complex.normSq, Complex.ofReal, SlashAction.map, UpperHalfPlane.im, HPow.hPow, HAdd.hAdd, UpperHalfPlane.petersson, HSMul.hSMul, UpperHalfPlane.σ, starRingEnd, OfNat.ofNat, DFunLike.coe, Neg.neg