-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
theorem cuspFunction_eqOn_const_of_nonpos_wt (hk : k ≤ 0) (f : F) :
    Set.EqOn (cuspFunction 1 f) (const ℂ (cuspFunction 1 f 0)) (Metric.ball 0 1)

Proof state:
case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Tactic:
obtain ⟨ξ, hξ, hξ₂⟩ := exists_one_half_le_im_and_norm_le hk f
  ⟨_, im_invQParam_pos_of_norm_lt_one Real.zero_lt_one (mem_ball_zero_iff.mp hq) hq'⟩

Result:
case refine_3.inr.intro.intro
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f ⟨invQParam 1 q, ⋯⟩‖ ≤ ‖f ξ‖
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Proof state:
case refine_3
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ ∃ w ∈ Metric.closedBall 0 (rexp (-π)),
    ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Tactic:
simp only [Metric.mem_closedBall, dist_zero_right]

Result:
case refine_3
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Proof state:
case refine_2
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
⊢ rexp (-π) < 1

Tactic:
simp only [exp_lt_one_iff, Left.neg_neg_iff, pi_pos]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f ⟨invQParam 1 q, ⋯⟩‖ ≤ ‖f ξ‖
⊢ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f (𝕢 1 ↑ξ)‖

Tactic:
simpa only [← eq_cuspFunction 1 f, Nat.cast_one, coe_mk_subtype,
qParam_right_inv one_ne_zero hq'] using hξ₂

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ‖0‖ ≤ rexp (-π)

Tactic:
simpa only [norm_zero] using exp_nonneg _

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
⊢ Set.EqOn (SlashInvariantFormClass.cuspFunction 1 f) (Function.const ℂ (SlashInvariantFormClass.cuspFunction 1 f 0))
    (Metric.ball 0 1)

Tactic:
refine eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)

Result:
case refine_1
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ DifferentiableWithinAt ℂ (SlashInvariantFormClass.cuspFunction 1 f) (Metric.ball 0 1) q

case refine_2
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
⊢ rexp (-π) < 1

case refine_3
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ ∃ w ∈ Metric.closedBall 0 (rexp (-π)),
    ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Proof state:
case refine_3
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Tactic:
rcases eq_or_ne q 0 with rfl | hq'

Result:
case refine_3.inl
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f 0‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Proof state:
case refine_1
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ DifferentiableWithinAt ℂ (SlashInvariantFormClass.cuspFunction 1 f) (Metric.ball 0 1) q

Tactic:
exact (differentiableAt_cuspFunction 1 f (mem_ball_zero_iff.mp hq)).differentiableWithinAt

Result:
no goals

Proof state:
case refine_3.inl
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f 0‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Tactic:
refine ⟨0, by simpa only [norm_zero] using exp_nonneg _, le_rfl⟩

Result:
no goals

Proof state:
case refine_3.inr.intro.intro
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f ⟨invQParam 1 q, ⋯⟩‖ ≤ ‖f ξ‖
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖SlashInvariantFormClass.cuspFunction 1 f q‖ ≤ ‖SlashInvariantFormClass.cuspFunction 1 f w‖

Tactic:
exact ⟨_, norm_qParam_le_of_one_half_le_im hξ,
  by simpa only [← eq_cuspFunction 1 f, Nat.cast_one, coe_mk_subtype,
    qParam_right_inv one_ne_zero hq'] using hξ₂⟩

Result:
no goals