[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : ModularForm Γ k
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
bdd_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ } =
    (fun f => f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
bdd_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
bdd_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_infty' := bdd_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_infty' := bdd_at_infty'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSlashInvariantForm
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
bdd_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
bdd_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_infty' := bdd_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : CuspForm Γ k
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
zero_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ } =
    (fun f => f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
zero_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
zero_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSlashInvariantForm
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
zero_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
zero_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : ModularForm Γ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty
    (↑({ toFun := ↑f, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑f ∣[k] γ = ↑f) } +
          { toFun := ↑g, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑g ∣[k] γ = ↑g) }) ∣[k]
      A)
[PROOFSTEP]
simpa using (f.bdd_at_infty' A).add (g.bdd_at_infty' A)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑0 ∣[k] A)
[PROOFSTEP]
simpa using zero_form_isBoundedAtImInfty
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : ModularForm Γ k
⊢ MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑(c • f.toSlashInvariantForm)
[PROOFSTEP]
simpa using f.holo'.const_smul (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : ModularForm Γ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑(c • f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.bdd_at_infty' A).const_smul_left (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : ModularForm Γ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑(-f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.bdd_at_infty' A).neg
[GOAL]
F : Type u_1
Γ✝ : Subgroup SL(2, ℤ)
k k_1 k_2 : ℤ
Γ : Subgroup SL(2, ℤ)
f : ModularForm Γ k_1
g : ModularForm Γ k_2
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑(SlashInvariantForm.mul f.toSlashInvariantForm g.toSlashInvariantForm) ∣[k_1 + k_2] A)
[PROOFSTEP]
rw [SlashInvariantForm.coe_mul, mul_slash_SL2]
[GOAL]
F : Type u_1
Γ✝ : Subgroup SL(2, ℤ)
k k_1 k_2 : ℤ
Γ : Subgroup SL(2, ℤ)
f : ModularForm Γ k_1
g : ModularForm Γ k_2
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑f.toSlashInvariantForm ∣[k_1] A * ↑g.toSlashInvariantForm ∣[k_2] A)
[PROOFSTEP]
exact (f.bdd_at_infty' A).mul (g.bdd_at_infty' A)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑1 ∣[0] A)
[PROOFSTEP]
simpa only [SlashInvariantForm.one_coe_eq_one, ModularForm.is_invariant_one] using
  atImInfty.const_boundedAtFilter (1 : ℂ)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : CuspForm Γ k
A : SL(2, ℤ)
⊢ IsZeroAtImInfty
    (↑({ toFun := ↑f, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑f ∣[k] γ = ↑f) } +
          { toFun := ↑g, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑g ∣[k] γ = ↑g) }) ∣[k]
      A)
[PROOFSTEP]
simpa using (f.zero_at_infty' A).add (g.zero_at_infty' A)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
⊢ ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑0 ∣[k] A)
[PROOFSTEP]
simpa using Filter.zero_zeroAtFilter _
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : CuspForm Γ k
⊢ MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑(c • f.toSlashInvariantForm)
[PROOFSTEP]
simpa using f.holo'.const_smul (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : CuspForm Γ k
A : SL(2, ℤ)
⊢ IsZeroAtImInfty (↑(c • f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.zero_at_infty' A).smul (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : CuspForm Γ k
A : SL(2, ℤ)
⊢ IsZeroAtImInfty (↑(-f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.zero_at_infty' A).neg
