case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∃ C, ∀ (z : E), ‖↑f z‖ ≤ C * ‖z‖
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
⊢ ∃ C, ∀ (z : E), ‖↑f z‖ ≤ C * ‖z‖
cases' @NontriviallyNormedField.non_trivial 𝕜 _ with k hk
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∀ (z : E), ‖↑f z‖ ≤ c * (‖k‖ / r) * ‖z‖
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∃ C, ∀ (z : E), ‖↑f z‖ ≤ C * ‖z‖
use c * (‖k‖ / r)
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z : E
⊢ ‖↑f z‖ ≤ c * (‖k‖ / r) * ‖z‖
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∀ (z : E), ‖↑f z‖ ≤ c * (‖k‖ / r) * ‖z‖
intro z
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ ‖↑f x‖ ≤ c * (‖k‖ / r) * ‖x‖
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z : E
⊢ ‖↑f z‖ ≤ c * (‖k‖ / r) * ‖z‖
refine' bound_of_shell _ r_pos hk (fun x hko hxo => _) _
case intro.calc_1
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c

case intro.calc_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
case intro
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ ‖↑f x‖ ≤ c * (‖k‖ / r) * ‖x‖
calc
  ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
  _ ≤ c * (‖x‖ * ‖k‖ / r) := (le_mul_of_one_le_right ?_ ?_)
  _ = _ := by ring
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ c * (‖x‖ * ‖k‖ / r) = c * (‖k‖ / r) * ‖x‖
ring
no goals
case intro.calc_1
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c
exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos]))
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ∈ ball 0 r
simp [r_pos]
case intro.calc_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r ≤ ‖x‖ * ‖k‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
case intro.calc_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
rw [div_le_iff (zero_lt_one.trans hk)] at hko
no goals
case intro.calc_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2556341
𝕜₃ : Type ?u.2556344
E : Type u_2
Eₗ : Type ?u.2556350
F : Type ?u.2556353
Fₗ : Type u_3
G : Type ?u.2556359
Gₗ : Type ?u.2556362
𝓕 : Type ?u.2556365
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z✝ : E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), z ∈ ball 0 r → ‖↑f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r ≤ ‖x‖ * ‖k‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
exact (one_le_div r_pos).mpr hko