[GOAL]
𝕜 : Type u_1
E : Type u_2
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‖₊
[PROOFSTEP]
rw [← sSup_closed_unit_ball_eq_nnnorm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
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‖₊
[PROOFSTEP]
refine' csSup_eq_of_forall_le_of_forall_lt_exists_gt _ _ fun r hr => _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
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)
[PROOFSTEP]
exact (Metric.nonempty_closedBall.mpr zero_le_one).image _
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
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‖₊
[PROOFSTEP]
rintro - ⟨x, hx, rfl⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
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‖₊
[PROOFSTEP]
exact ((mul 𝕜 E a).unit_le_op_norm x <| mem_closedBall_zero_iff.mp hx).trans (op_norm_mul_apply_le 𝕜 E a)
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
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
[PROOFSTEP]
have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
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
[PROOFSTEP]
rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr 
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
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
[PROOFSTEP]
obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr <| inv_pos.2 ha)
[GOAL]
case refine'_3.intro.intro
𝕜 : Type u_1
E : Type u_2
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
[PROOFSTEP]
refine' ⟨_, ⟨k • star a, _, rfl⟩, _⟩
[GOAL]
case refine'_3.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
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
[PROOFSTEP]
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‖₊⁻¹)
[GOAL]
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
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⋆)
[PROOFSTEP]
simp only [map_smul, nnnorm_smul, mul_apply', mul_smul_comm, CstarRing.nnnorm_self_mul_star]
[GOAL]
case refine'_3.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
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‖₊)
[PROOFSTEP]
rwa [← NNReal.div_lt_iff (mul_pos ha ha).ne', div_eq_mul_inv, mul_inv, ← mul_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ‖↑(ContinuousLinearMap.flip (mul 𝕜 E)) a‖₊ = ‖a‖₊
[PROOFSTEP]
rw [← sSup_unit_ball_eq_nnnorm, ← nnnorm_star, ← @op_nnnorm_mul 𝕜 E, ← sSup_unit_ball_eq_nnnorm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
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 => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1) =
    sSup ((fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 1)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun x => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1 =
    (fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 1
[PROOFSTEP]
simp only [mul_apply', flip_apply]
[GOAL]
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1 = (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
[PROOFSTEP]
refine' Set.Subset.antisymm _ _
[GOAL]
case e_a.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1 ⊆ (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
[PROOFSTEP]
rintro - ⟨b, hb, rfl⟩
[GOAL]
case e_a.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1 ⊆ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1
[PROOFSTEP]
rintro - ⟨b, hb, rfl⟩
[GOAL]
case e_a.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a_1 * a‖₊) b ∈ (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
[PROOFSTEP]
refine' ⟨star b, by simpa only [norm_star, mem_ball_zero_iff] using hb, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ b⋆ ∈ Metric.ball 0 1
[PROOFSTEP]
simpa only [norm_star, mem_ball_zero_iff] using hb
[GOAL]
case e_a.refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) b ∈ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1
[PROOFSTEP]
refine' ⟨star b, by simpa only [norm_star, mem_ball_zero_iff] using hb, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ b⋆ ∈ Metric.ball 0 1
[PROOFSTEP]
simpa only [norm_star, mem_ball_zero_iff] using hb
[GOAL]
case e_a.refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) b⋆ = (fun a_1 => ‖a_1 * a‖₊) b
[PROOFSTEP]
simp only [← star_mul, nnnorm_star]
[GOAL]
case e_a.refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CstarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a_1 * a‖₊) b⋆ = (fun a_1 => ‖a⋆ * a_1‖₊) b
[PROOFSTEP]
simpa using (nnnorm_star (star b * a)).symm
