-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_le_of_shell' {f : E →SL[σ₁₂] F} {ε C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜}
    (hc : ‖c‖ < 1) (hf : ∀ x, ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

Proof state:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖

Tactic:
rwa [norm_inv, div_eq_mul_inv, inv_inv]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_of_ball ε_pos hC fun x hx => hf x ?_ ?_

Result:
case pos.refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
x : E
hx : x ∈ ball 0 ε
⊢ ε * ‖c‖ ≤ ‖x‖

case pos.refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
x : E
hx : x ∈ ball 0 ε
⊢ ‖x‖ < ε

Proof state:
case pos.refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
x : E
hx : x ∈ ball 0 ε
⊢ ‖x‖ < ε

Tactic:
rwa [ball_zero_eq] at hx

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Tactic:
rw [← inv_inv c, norm_inv, inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)] at hc

Result:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Proof state:
case pos.refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
x : E
hx : x ∈ ball 0 ε
⊢ ε * ‖c‖ ≤ ‖x‖

Tactic:
simp [h0]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
⊢ ‖f‖ ≤ C

Tactic:
by_cases h0 : c = 0

Result:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
⊢ ‖f‖ ≤ C

case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Proof state:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_of_shell ε_pos hC hc ?_

Result:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖