-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ)
    (h : ∀ z ∈ Metric.ball (0 : E) r, ‖f z‖ ≤ c) : ∃ C, ∀ z : E, ‖f z‖ ≤ C * ‖z‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z : E
⊢ ‖f z‖ ≤ c * (‖k‖ / r) * ‖z‖

Tactic:
refine bound_of_shell _ r_pos hk (fun x hko hxo => ?_) _

Result:
case h
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∀ (z : E), ‖f z‖ ≤ c * (‖k‖ / r) * ‖z‖

Tactic:
intro z

Result:
case h
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z : E
⊢ ‖f z‖ ≤ c * (‖k‖ / r) * ‖z‖

Proof state:
case h.calc_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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

Tactic:
rw [div_le_iff₀ (zero_lt_one.trans hk)] at hko

Result:
case h.calc_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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

Proof state:
case h.calc_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c

Tactic:
exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos]))

Result:
no goals

Proof state:
case h.calc_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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

Tactic:
exact (one_le_div r_pos).mpr hko

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
⊢ ∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖

Tactic:
obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial 𝕜 _

Result:
case intro
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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

Tactic:
simp [r_pos]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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‖

Tactic:
calc
  ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
  _ ≤ c * (‖x‖ * ‖k‖ / r) := le_mul_of_one_le_right ?_ ?_
  _ = _ := by ring

Result:
case h.calc_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c

case h.calc_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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

Proof state:
case intro
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖

Tactic:
use c * (‖k‖ / r)

Result:
case h
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
⊢ ∀ (z : E), ‖f z‖ ≤ c * (‖k‖ / r) * ‖z‖

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ 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‖

Tactic:
ring

Result:
no goals