𝕜 : 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 => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1) =
    sSup ((fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 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
⊢ ‖↑(ContinuousLinearMap.flip (mul 𝕜 E)) a‖₊ = ‖a‖₊
rw [← sSup_unit_ball_eq_nnnorm, ← nnnorm_star, ← @op_nnnorm_mul 𝕜 E, ← sSup_unit_ball_eq_nnnorm]
case e_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
⊢ (fun x => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1 =
    (fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 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 => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1) =
    sSup ((fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 1)
congr 1
case e_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
⊢ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1 = (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
case e_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
⊢ (fun x => ‖↑(↑(ContinuousLinearMap.flip (mul 𝕜 E)) a) x‖₊) '' Metric.ball 0 1 =
    (fun x => ‖↑(↑(mul 𝕜 E) a⋆) x‖₊) '' Metric.ball 0 1
simp only [mul_apply', flip_apply]
case e_a.refine'_1.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 b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) b⋆ = (fun a_1 => ‖a_1 * a‖₊) b

case e_a.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 b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a_1 * a‖₊) b⋆ = (fun a_1 => ‖a⋆ * a_1‖₊) b
case e_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
⊢ (fun a_1 => ‖a_1 * a‖₊) '' Metric.ball 0 1 = (fun a_1 => ‖a⋆ * a_1‖₊) '' Metric.ball 0 1
refine' Set.Subset.antisymm _ _ <;> rintro - ⟨b, hb, rfl⟩ <;>
  refine' ⟨star b, by simpa only [norm_star, mem_ball_zero_iff] using hb, _⟩
no goals
𝕜 : 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 b : E
hb : b ∈ Metric.ball 0 1
⊢ b⋆ ∈ Metric.ball 0 1
simpa only [norm_star, mem_ball_zero_iff] using hb
no goals
case e_a.refine'_1.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 b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a⋆ * a_1‖₊) b⋆ = (fun a_1 => ‖a_1 * a‖₊) b
simp only [← star_mul, nnnorm_star]
no goals
case e_a.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 b : E
hb : b ∈ Metric.ball 0 1
⊢ (fun a_1 => ‖a_1 * a‖₊) b⋆ = (fun a_1 => ‖a⋆ * a_1‖₊) b
simpa using (nnnorm_star (star b * a)).symm