case intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type ?u.95729
E : Type u_4
Eₗ : Type ?u.95735
F : Type u_5
Fₗ : Type ?u.95741
G : Type ?u.95744
Gₗ : Type ?u.95747
𝓕 : Type u_1
inst✝¹⁸ : SeminormedAddCommGroup E
inst✝¹⁷ : SeminormedAddCommGroup Eₗ
inst✝¹⁶ : SeminormedAddCommGroup F
inst✝¹⁵ : SeminormedAddCommGroup Fₗ
inst✝¹⁴ : SeminormedAddCommGroup G
inst✝¹³ : SeminormedAddCommGroup Gₗ
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 Eₗ
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NormedSpace 𝕜 Fₗ
inst✝⁵ : NormedSpace 𝕜₃ G
inst✝⁴ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : ‖x‖ ≠ 0
δ : 𝕜
hδ : δ ≠ 0
δxle : ‖δ • x‖ < ε
leδx : ε / ‖c‖ ≤ ‖δ • x‖
right✝ : ‖δ‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
⊢ ‖↑f x‖ ≤ C * ‖x‖
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type ?u.95729
E : Type u_4
Eₗ : Type ?u.95735
F : Type u_5
Fₗ : Type ?u.95741
G : Type ?u.95744
Gₗ : Type ?u.95747
𝓕 : Type u_1
inst✝¹⁸ : SeminormedAddCommGroup E
inst✝¹⁷ : SeminormedAddCommGroup Eₗ
inst✝¹⁶ : SeminormedAddCommGroup F
inst✝¹⁵ : SeminormedAddCommGroup Fₗ
inst✝¹⁴ : SeminormedAddCommGroup G
inst✝¹³ : SeminormedAddCommGroup Gₗ
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 Eₗ
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NormedSpace 𝕜 Fₗ
inst✝⁵ : NormedSpace 𝕜₃ G
inst✝⁴ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : ‖x‖ ≠ 0
⊢ ‖↑f x‖ ≤ C * ‖x‖
rcases rescale_to_shell_semi_normed hc ε_pos hx with ⟨δ, hδ, δxle, leδx, _⟩
no goals
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type ?u.95729
E : Type u_4
Eₗ : Type ?u.95735
F : Type u_5
Fₗ : Type ?u.95741
G : Type ?u.95744
Gₗ : Type ?u.95747
𝓕 : Type u_1
inst✝¹⁸ : SeminormedAddCommGroup E
inst✝¹⁷ : SeminormedAddCommGroup Eₗ
inst✝¹⁶ : SeminormedAddCommGroup F
inst✝¹⁵ : SeminormedAddCommGroup Fₗ
inst✝¹⁴ : SeminormedAddCommGroup G
inst✝¹³ : SeminormedAddCommGroup Gₗ
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 Eₗ
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NormedSpace 𝕜 Fₗ
inst✝⁵ : NormedSpace 𝕜₃ G
inst✝⁴ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : ‖x‖ ≠ 0
δ : 𝕜
hδ : δ ≠ 0
δxle : ‖δ • x‖ < ε
leδx : ε / ‖c‖ ≤ ‖δ • x‖
right✝ : ‖δ‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
⊢ ‖↑f x‖ ≤ C * ‖x‖
simpa only [map_smulₛₗ, norm_smul, mul_left_comm C, mul_le_mul_left (norm_pos_iff.2 hδ),
  RingHomIsometric.is_iso] using hf (δ • x) leδx δxle