[GOAL]
β : Type u_1
G : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup α
inst✝¹ : SMul γ α
inst✝ : SlashAction β G α γ
k : β
g : G
a : α
⊢ (-a) ∣[k;γ] g + a ∣[k;γ] g = 0
[PROOFSTEP]
rw [← SlashAction.add_slash, add_left_neg, SlashAction.zero_slash]
[GOAL]
R : Type u_1
β : Type u_2
G : Type u_3
α : Type u_4
γ : Type u_5
inst✝⁷ : Group G
inst✝⁶ : AddGroup α
inst✝⁵ : Monoid γ
inst✝⁴ : MulAction γ α
inst✝³ : SMul R γ
inst✝² : SMul R α
inst✝¹ : IsScalarTower R γ α
inst✝ : SlashAction β G α γ
k : β
g : G
a : α
r : R
⊢ (r • a) ∣[k;γ] g = r • a ∣[k;γ] g
[PROOFSTEP]
rw [← smul_one_smul γ r a, SlashAction.smul_slash, smul_one_smul]
[GOAL]
β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
γ : Type u_5
inst✝⁴ : Group G
inst✝³ : AddMonoid α
inst✝² : SMul γ α
inst✝¹ : Group H
inst✝ : SlashAction β G α γ
h : H →* G
k : β
a : α
⊢ (fun k g => SlashAction.map γ k (↑h g)) k 1 a = a
[PROOFSTEP]
simp only [map_one, SlashAction.slash_one]
[GOAL]
β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
γ : Type u_5
inst✝⁴ : Group G
inst✝³ : AddMonoid α
inst✝² : SMul γ α
inst✝¹ : Group H
inst✝ : SlashAction β G α γ
h : H →* G
k : β
g gg : H
a : α
⊢ (fun k g => SlashAction.map γ k (↑h g)) k (g * gg) a =
    (fun k g => SlashAction.map γ k (↑h g)) k gg ((fun k g => SlashAction.map γ k (↑h g)) k g a)
[PROOFSTEP]
simp only [map_mul, SlashAction.slash_mul]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
⊢ f ∣[k](A * B) = (f ∣[k]A) ∣[k]B
[PROOFSTEP]
ext1 x
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
⊢ (f ∣[k](A * B)) x = ((f ∣[k]A) ∣[k]B) x
[PROOFSTEP]
simp_rw [slash, UpperHalfPlane.denom_cocycle A B x]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
⊢ f ((A * B) • x) * ↑(Matrix.det ↑↑(A * B)) ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) =
    f (A • B • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(Matrix.det ↑↑B) ^ (k - 1) *
      denom B x ^ (-k)
[PROOFSTEP]
have e3 : (A * B) • x = A • B • x := by convert UpperHalfPlane.mul_smul' A B x
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
⊢ (A * B) • x = A • B • x
[PROOFSTEP]
convert UpperHalfPlane.mul_smul' A B x
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
e3 : (A * B) • x = A • B • x
⊢ f ((A * B) • x) * ↑(Matrix.det ↑↑(A * B)) ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) =
    f (A • B • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(Matrix.det ↑↑B) ^ (k - 1) *
      denom B x ^ (-k)
[PROOFSTEP]
rw [e3]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
e3 : (A * B) • x = A • B • x
⊢ f (A • B • x) * ↑(Matrix.det ↑↑(A * B)) ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) =
    f (A • B • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(Matrix.det ↑↑B) ^ (k - 1) *
      denom B x ^ (-k)
[PROOFSTEP]
simp only [UpperHalfPlane.num, UpperHalfPlane.denom, ofReal_mul, Subgroup.coe_mul, UpperHalfPlane.coe_smul,
  Units.val_mul, Matrix.det_mul, UpperHalfPlane.smulAux, UpperHalfPlane.smulAux', UpperHalfPlane.coe_mk] at *
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
e3 : (A * B) • x = A • B • x
⊢ f (A • B • x) * (↑(Matrix.det ↑↑A) * ↑(Matrix.det ↑↑B)) ^ (k - 1) *
      ((↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) *
          (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^
        (-k) =
    f (A • B • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) *
          (↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) ^ (-k) *
        ↑(Matrix.det ↑↑B) ^ (k - 1) *
      (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ (-k)
[PROOFSTEP]
field_simp
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
e3 : (A * B) • x = A • B • x
⊢ f (A • B • x) * (↑(Matrix.det ↑↑A) * ↑(Matrix.det ↑↑B)) ^ (k - 1) /
      ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) *
          (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^
        k =
    f (A • B • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) * ↑(Matrix.det ↑↑B) ^ (k - 1) /
      ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) ^ k *
        (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ k)
[PROOFSTEP]
have :
  (((↑(↑A : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) *
        ((↑(↑B : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ)) ^
      (k - 1) =
    ((↑(↑A : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) ^ (k - 1) *
      ((↑(↑B : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) ^ (k - 1) :=
  by simp_rw [← mul_zpow]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
e3 : (A * B) • x = A • B • x
⊢ (↑(Matrix.det ↑↑A) * ↑(Matrix.det ↑↑B)) ^ (k - 1) = ↑(Matrix.det ↑↑A) ^ (k - 1) * ↑(Matrix.det ↑↑B) ^ (k - 1)
[PROOFSTEP]
simp_rw [← mul_zpow]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A B : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
x : ℍ
e3 : (A * B) • x = A • B • x
this : (↑(Matrix.det ↑↑A) * ↑(Matrix.det ↑↑B)) ^ (k - 1) = ↑(Matrix.det ↑↑A) ^ (k - 1) * ↑(Matrix.det ↑↑B) ^ (k - 1)
⊢ f (A • B • x) * (↑(Matrix.det ↑↑A) * ↑(Matrix.det ↑↑B)) ^ (k - 1) /
      ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) *
          (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^
        k =
    f (A • B • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) * ↑(Matrix.det ↑↑B) ^ (k - 1) /
      ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) ^ k *
        (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ k)
[PROOFSTEP]
simp_rw [this, ← mul_assoc, ← mul_zpow]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
⊢ (f + g) ∣[k]A = f ∣[k]A + g ∣[k]A
[PROOFSTEP]
ext1
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x✝ : ℍ
⊢ ((f + g) ∣[k]A) x✝ = (f ∣[k]A + g ∣[k]A) x✝
[PROOFSTEP]
simp only [slash, Pi.add_apply, denom, zpow_neg]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x✝ : ℍ
⊢ (f (A • x✝) + g (A • x✝)) * ↑(Matrix.det ↑↑A) ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ =
    f (A • x✝) * ↑(Matrix.det ↑↑A) ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ +
      g (A • x✝) * ↑(Matrix.det ↑↑A) ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹
[PROOFSTEP]
ring
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
f : ℍ → ℂ
⊢ ∀ (x : ℍ), (f ∣[k]1) x = f x
[PROOFSTEP]
simp [slash, denom]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
c : α
⊢ (c • f) ∣[k]A = c • f ∣[k]A
[PROOFSTEP]
simp_rw [← smul_one_smul ℂ c f, ← smul_one_smul ℂ c (f ∣[k] A)]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
c : α
⊢ ((c • 1) • f) ∣[k]A = (c • 1) • f ∣[k]A
[PROOFSTEP]
ext1
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ (((c • 1) • f) ∣[k]A) x✝ = ((c • 1) • f ∣[k]A) x✝
[PROOFSTEP]
simp_rw [slash]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ ((c • 1) • f) (A • x✝) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A x✝ ^ (-k) =
    ((c • 1) • fun x => f (A • x) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A x ^ (-k)) x✝
[PROOFSTEP]
simp only [slash, Algebra.id.smul_eq_mul, Matrix.GeneralLinearGroup.det_apply_val, Pi.smul_apply]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f : ℍ → ℂ
c : α
x✝ : ℍ
⊢ c • 1 * f (A • x✝) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A x✝ ^ (-k) =
    c • 1 * (f (A • x✝) * ↑(Matrix.det ↑↑A) ^ (k - 1) * denom A x✝ ^ (-k))
[PROOFSTEP]
ring
[GOAL]
Γ : Subgroup SL(2, ℤ)
k✝ : ℤ
f : ℍ → ℂ
α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
x✝ : ℍ
⊢ (0 ∣[k]A) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
simp only [slash, Pi.zero_apply, zero_mul]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : ℍ → ℂ
A : SL(2, ℤ)
⊢ 1 ∣[0] A = 1
[PROOFSTEP]
have : ((↑ₘ(A : GL(2, ℝ)⁺)).det : ℝ) = 1 := det_coe'
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : ℍ → ℂ
A : SL(2, ℤ)
this : Matrix.det ↑↑↑A = 1
⊢ 1 ∣[0] A = 1
[PROOFSTEP]
funext
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : ℍ → ℂ
A : SL(2, ℤ)
this : Matrix.det ↑↑↑A = 1
x✝ : ℍ
⊢ (1 ∣[0] A) x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
rw [SL_slash, slash_def, slash, zero_sub, this]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : ℍ → ℂ
A : SL(2, ℤ)
this : Matrix.det ↑↑↑A = 1
x✝ : ℍ
⊢ OfNat.ofNat 1 (↑A • x✝) * ↑1 ^ (-1) * denom (↑A) x✝ ^ (-0) = OfNat.ofNat 1 x✝
[PROOFSTEP]
simp
[GOAL]
Γ✝ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
f : ℍ → ℂ
γ : { x // x ∈ Γ }
z : ℍ
⊢ (f ∣[k] γ) z = f z ↔ f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
[PROOFSTEP]
simp only [subgroup_slash, slash_def, ModularForm.slash]
[GOAL]
Γ✝ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
f : ℍ → ℂ
γ : { x // x ∈ Γ }
z : ℍ
⊢ f (↑↑γ • z) * ↑(Matrix.det ↑↑↑↑γ) ^ (k - 1) * denom (↑↑γ) z ^ (-k) = f z ↔
    f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
[PROOFSTEP]
convert inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _ using 2
[GOAL]
case h.e'_1.h.e'_2
Γ✝ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
f : ℍ → ℂ
γ : { x // x ∈ Γ }
z : ℍ
⊢ f (↑↑γ • z) * ↑(Matrix.det ↑↑↑↑γ) ^ (k - 1) * denom (↑↑γ) z ^ (-k) =
    ((↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k)⁻¹ * f (γ • z)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case h.e'_1.h.e'_2
Γ✝ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
f : ℍ → ℂ
γ : { x // x ∈ Γ }
z : ℍ
⊢ denom (↑↑γ) z ^ (-k) * (f (↑↑γ • z) * ↑(Matrix.det ↑↑↑↑γ) ^ (k - 1)) =
    ((↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k)⁻¹ * f (γ • z)
[PROOFSTEP]
simp only [denom, zpow_neg, det_coe', ofReal_one, one_zpow, mul_one, subgroup_to_sl_moeb, sl_moeb]
[GOAL]
case h.e'_1.h.e'_2
Γ✝ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
f : ℍ → ℂ
γ : { x // x ∈ Γ }
z : ℍ
⊢ ((↑(↑↑↑↑γ 1 0) * ↑z + ↑(↑↑↑↑γ 1 1)) ^ k)⁻¹ * f (↑↑γ • z) = ((↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k)⁻¹ * f (↑↑γ • z)
[PROOFSTEP]
rfl
[GOAL]
case convert_4
Γ✝ : Subgroup SL(2, ℤ)
k✝ : ℤ
f✝ : ℍ → ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
f : ℍ → ℂ
γ : { x // x ∈ Γ }
z : ℍ
⊢ (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k ≠ 0
[PROOFSTEP]
convert zpow_ne_zero k (denom_ne_zero γ z)
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] A = Matrix.det ↑↑A • f ∣[k1] A * g ∣[k2] A
[PROOFSTEP]
ext1 x
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
⊢ ((f * g) ∣[k1 + k2] A) x = (Matrix.det ↑↑A • f ∣[k1] A * g ∣[k2] A) x
[PROOFSTEP]
simp only [slash_def, slash, Matrix.GeneralLinearGroup.det_apply_val, Pi.mul_apply, Pi.smul_apply,
  Algebra.smul_mul_assoc, real_smul]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
⊢ f (A • x) * g (A • x) * ↑(Matrix.det ↑↑A) ^ (k1 + k2 - 1) * denom A x ^ (-(k1 + k2)) =
    ↑(Matrix.det ↑↑A) * (f (A • x) * ↑(Matrix.det ↑↑A) ^ (k1 - 1) * denom A x ^ (-k1)) *
      (g (A • x) * ↑(Matrix.det ↑↑A) ^ (k2 - 1) * denom A x ^ (-k2))
[PROOFSTEP]
set d : ℂ := ↑((↑ₘA).det : ℝ)
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
⊢ 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))
[PROOFSTEP]
have h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1) :=
  by
  have : d ≠ 0 := by
    dsimp
    norm_cast
    exact Matrix.GLPos.det_ne_zero A
  rw [← zpow_one_add₀ this, ← zpow_add₀ this]
  congr; ring
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
[PROOFSTEP]
have : d ≠ 0 := by
  dsimp
  norm_cast
  exact Matrix.GLPos.det_ne_zero A
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
⊢ d ≠ 0
[PROOFSTEP]
dsimp
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
⊢ ¬↑(Matrix.det ↑↑A) = 0
[PROOFSTEP]
norm_cast
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
⊢ ¬Matrix.det ↑↑A = 0
[PROOFSTEP]
exact Matrix.GLPos.det_ne_zero A
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
[PROOFSTEP]
rw [← zpow_one_add₀ this, ← zpow_add₀ this]
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))
[PROOFSTEP]
congr
[GOAL]
case e_a
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
this : d ≠ 0
⊢ k1 + k2 - 1 = 1 + (k1 - 1) + (k2 - 1)
[PROOFSTEP]
ring
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
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))
[PROOFSTEP]
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
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
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)
[PROOFSTEP]
rw [Int.neg_add, zpow_add₀]
[GOAL]
case ha
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ denom A x ≠ 0
[PROOFSTEP]
exact UpperHalfPlane.denom_ne_zero A x
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
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))
[PROOFSTEP]
rw [h1, h22]
[GOAL]
case h
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : { x // x ∈ GL(2, ℝ)⁺ }
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑(Matrix.det ↑↑A)
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))
[PROOFSTEP]
ring
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] ↑A = Matrix.det ↑↑↑A • f ∣[k1] A * g ∣[k2] A
[PROOFSTEP]
apply mul_slash
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ Matrix.det ↑↑↑A • f ∣[k1] A * g ∣[k2] A = 1 • f ∣[k1] A * g ∣[k2] A
[PROOFSTEP]
rw [det_coe']
[GOAL]
Γ : Subgroup SL(2, ℤ)
k : ℤ
f✝ : ℍ → ℂ
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ 1 • f ∣[k1] A * g ∣[k2] A = f ∣[k1] A * g ∣[k2] A
[PROOFSTEP]
rw [one_smul]