[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
f g : SlashInvariantForm Γ k
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
g : SlashInvariantForm Γ k
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ (γ : { x // x ∈ Γ }), toFun✝ ∣[k] γ = toFun✝
h : { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
toFun✝¹ : ℍ → ℂ
slash_action_eq'✝¹ : ∀ (γ : { x // x ∈ Γ }), toFun✝¹ ∣[k] γ = toFun✝¹
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ (γ : { x // x ∈ Γ }), toFun✝ ∣[k] γ = toFun✝
h :
  { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ }.toFun =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ } =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
Γ✝ : outParam (Subgroup SL(2, ℤ))
k✝ : outParam ℤ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : { x // x ∈ Γ }
z : ℍ
⊢ ↑f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * ↑f z
[PROOFSTEP]
rw [← ModularForm.slash_action_eq'_iff, slash_action_eqn]
[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
f g : SlashInvariantForm Γ k
γ : { x // x ∈ Γ }
⊢ (↑f + ↑g) ∣[k] γ = ↑f + ↑g
[PROOFSTEP]
rw [SlashAction.add_slash, slash_action_eqn, slash_action_eqn]
[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : { x // x ∈ Γ }
⊢ (c • ↑f) ∣[k] γ = c • ↑f
[PROOFSTEP]
rw [SlashAction.smul_slash_of_tower, slash_action_eqn]
[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
f : SlashInvariantForm Γ k
γ : { x // x ∈ Γ }
⊢ (-↑f) ∣[k] γ = -↑f
[PROOFSTEP]
rw [SlashAction.neg_slash, slash_action_eqn]
[GOAL]
F : Type u_1
Γ✝ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
k₁ k₂ : ℤ
Γ : Subgroup SL(2, ℤ)
f : SlashInvariantForm Γ k₁
g : SlashInvariantForm Γ k₂
A : { x // x ∈ Γ }
⊢ (↑f * ↑g) ∣[k₁ + k₂] A = ↑f * ↑g
[PROOFSTEP]
simp_rw [ModularForm.mul_slash_subgroup, SlashInvariantFormClass.slash_action_eq]
