-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem mul_slash (k1 k2 : ℤ) (A : GL(2, ℝ)⁺) (f g : ℍ → ℂ) :
    (f * g) ∣[k1 + k2] A = ((↑ₘA).det : ℝ) • f ∣[k1] A * g ∣[k2] A

Proof state:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
⊢ f (A • x) * g (A • x) * ↑(↑↑A).det ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    ↑(↑↑A).det * (f (A • x) * ↑(↑↑A).det ^ (k1 - 1) * denom A x ^ (-k1)) *
      (g (A • x) * ↑(↑↑A).det ^ (k2 - 1) * denom A x ^ (-k2))

Tactic:
set d : ℂ := ↑(↑ₘ[ℝ] A).det

Result:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
⊢ f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Proof state:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Tactic:
have h22 : denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2) := by
  rw [Int.neg_add, zpow_add₀]
  exact UpperHalfPlane.denom_ne_zero A x

Result:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
h22 : denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2)
⊢ f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
⊢ d ≠ 0

Tactic:
dsimp only [d]

Result:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
⊢ ↑(↑↑A).det ≠ 0

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2)

Tactic:
rw [Int.neg_add, zpow_add₀]

Result:
case ha
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ denom A x ≠ 0

Proof state:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
⊢ f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Tactic:
have h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1) := by
  have : d ≠ 0 := by
    dsimp only [d]
    exact_mod_cast Matrix.GLPos.det_ne_zero A
  rw [← zpow_one_add₀ this, ← zpow_add₀ this]
  congr; ring

Result:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Tactic:
have : d ≠ 0 := by
  dsimp only [d]
  exact_mod_cast Matrix.GLPos.det_ne_zero A

Result:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Proof state:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
h22 : denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2)
⊢ f (A • x) * g (A • x) * (d * d ^ (k1 - 1) * d ^ (k2 - 1)) * (denom A x ^ (-k1) * denom A x ^ (-k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Tactic:
ring

Result:
no goals

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Tactic:
rw [← zpow_one_add₀ this, ← zpow_add₀ this]

Result:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))

Proof state:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
h22 : denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2)
⊢ f (A • x) * g (A • x) * d ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Tactic:
rw [h1, h22]

Result:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
h22 : denom A x ^ (-(k1 + k2)) = denom A x ^ (-k1) * denom A x ^ (-k2)
⊢ f (A • x) * g (A • x) * (d * d ^ (k1 - 1) * d ^ (k2 - 1)) * (denom A x ^ (-k1) * denom A x ^ (-k2)) =
    d * (f (A • x) * d ^ (k1 - 1) * denom A x ^ (-k1)) * (g (A • x) * d ^ (k2 - 1) * denom A x ^ (-k2))

Proof state:
case ha
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ denom A x ≠ 0

Tactic:
exact UpperHalfPlane.denom_ne_zero A x

Result:
no goals

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
⊢ ↑(↑↑A).det ≠ 0

Tactic:
exact_mod_cast Matrix.GLPos.det_ne_zero A

Result:
no goals

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))

Tactic:
congr

Result:
case e_a
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
this : d ≠ 0
⊢ k1 + k2 - 1 = 1 + (k1 - 1) + (k2 - 1)

Proof state:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
⊢ ((f * g) ∣[k1 + k2] A) x = ((↑↑A).det • f ∣[k1] A * g ∣[k2] A) x

Tactic:
simp only [slash_def, slash, Matrix.GeneralLinearGroup.val_det_apply,
  Pi.mul_apply, Pi.smul_apply, Algebra.smul_mul_assoc, real_smul]

Result:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
⊢ f (A • x) * g (A • x) * ↑(↑↑A).det ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    ↑(↑↑A).det * (f (A • x) * ↑(↑↑A).det ^ (k1 - 1) * denom A x ^ (-k1)) *
      (g (A • x) * ↑(↑↑A).det ^ (k2 - 1) * denom A x ^ (-k2))

Proof state:
case e_a
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(↑↑A).det
this : d ≠ 0
⊢ k1 + k2 - 1 = 1 + (k1 - 1) + (k2 - 1)

Tactic:
ring

Result:
no goals

Proof state:
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] A = (↑↑A).det • f ∣[k1] A * g ∣[k2] A

Tactic:
ext1 x

Result:
case h
k1 k2 : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x : ℍ
⊢ ((f * g) ∣[k1 + k2] A) x = ((↑↑A).det • f ∣[k1] A * g ∣[k2] A) x