𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ sSup ((fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1) = ‖a‖₊
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ‖↑(mul 𝕜 E) a‖₊ = ‖a‖₊
rw [← sSup_closed_unit_ball_eq_nnnorm]
case refine'_1
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ Set.Nonempty ((fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1)

case refine'_2
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ∀ (a_1 : NNReal), a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 → a_1 ≤ ‖a‖₊

case refine'_3
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ sSup ((fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1) = ‖a‖₊
refine' csSup_eq_of_forall_le_of_forall_lt_exists_gt _ _ fun r hr => _
no goals
case refine'_1
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ Set.Nonempty ((fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1)
exact (Metric.nonempty_closedBall.mpr zero_le_one).image _
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a x : E
hx : x ∈ Metric.closedBall 0 1
⊢ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) x ≤ ‖a‖₊
case refine'_2
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ∀ (a_1 : NNReal), a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 → a_1 ≤ ‖a‖₊
rintro - ⟨x, hx, rfl⟩
no goals
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a x : E
hx : x ∈ Metric.closedBall 0 1
⊢ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) x ≤ ‖a‖₊
exact
  ((mul 𝕜 E a).unit_le_op_norm x <| mem_closedBall_zero_iff.mp hx).trans
    (op_norm_mul_apply_le 𝕜 E a)
case refine'_3
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
case refine'_3
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr
case refine'_3
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
case refine'_3
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr
case refine'_3.intro.intro
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
case refine'_3
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
obtain ⟨k, hk₁, hk₂⟩ :=
  NormedField.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr <| inv_pos.2 ha)
case refine'_3.intro.intro.refine'_1
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ k • a⋆ ∈ Metric.closedBall 0 1

case refine'_3.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) (k • a⋆)
case refine'_3.intro.intro
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ ∃ a_1, a_1 ∈ (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1 ∧ r < a_1
refine' ⟨_, ⟨k • star a, _, rfl⟩, _⟩
no goals
case refine'_3.intro.intro.refine'_1
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ k • a⋆ ∈ Metric.closedBall 0 1
simpa only [mem_closedBall_zero_iff, norm_smul, one_mul, norm_star] using
  (NNReal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹)
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x => ‖↑(↑(mul 𝕜 E) a) x‖₊) (k • a⋆)
simp only [map_smul, nnnorm_smul, mul_apply', mul_smul_comm, CstarRing.nnnorm_self_mul_star]
no goals
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_2
E : Type u_1
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
rwa [← NNReal.div_lt_iff (mul_pos ha ha).ne', div_eq_mul_inv, mul_inv, ← mul_assoc]