[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
h : a.toProd = b.toProd
⊢ a = b
[PROOFSTEP]
cases a
[GOAL]
case mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), ↑toProd✝.snd x * y = x * ↑toProd✝.fst y
h : { toProd := toProd✝, central := central✝ }.toProd = b.toProd
⊢ { toProd := toProd✝, central := central✝ } = b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
toProd✝¹ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝¹ : ∀ (x y : A), ↑toProd✝¹.snd x * y = x * ↑toProd✝¹.fst y
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), ↑toProd✝.snd x * y = x * ↑toProd✝.fst y
h : { toProd := toProd✝¹, central := central✝¹ }.toProd = { toProd := toProd✝, central := central✝ }.toProd
⊢ { toProd := toProd✝¹, central := central✝¹ } = { toProd := toProd✝, central := central✝ }
[PROOFSTEP]
simpa using h
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)
⊢ x ∈ Set.range toProd → x ∈ {lr | ∀ (x y : A), ↑lr.snd x * y = x * ↑lr.fst y}
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProd ∈ {lr | ∀ (x y : A), ↑lr.snd x * y = x * ↑lr.fst y}
[PROOFSTEP]
exact a.central
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ ↑(a.snd + b.snd) x * y = x * ↑(a.fst + b.fst) y
[PROOFSTEP]
simp only [ContinuousLinearMap.add_apply, mul_add, add_mul, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x y : A
⊢ -↑a.snd x * y = x * -↑a.fst y
[PROOFSTEP]
simp only [ContinuousLinearMap.neg_apply, neg_mul, mul_neg, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ ↑(a.snd - b.snd) x * y = x * ↑(a.fst - b.fst) y
[PROOFSTEP]
simp only [ContinuousLinearMap.sub_apply, _root_.sub_mul, _root_.mul_sub, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : SMulCommClass 𝕜 A A
inst✝⁶ : IsScalarTower 𝕜 A A
S : Type u_3
inst✝⁵ : Monoid S
inst✝⁴ : DistribMulAction S A
inst✝³ : SMulCommClass 𝕜 S A
inst✝² : ContinuousConstSMul S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass S A A
s : S
a : 𝓜(𝕜, A)
x y : A
⊢ ↑(s • a.snd) x * y = x * ↑(s • a.fst) y
[PROOFSTEP]
simp only [ContinuousLinearMap.smul_apply, mul_smul_comm, smul_mul_assoc, central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ ↑b.snd (↑a.snd x) * y = x * ↑a.fst (↑b.fst y)
[PROOFSTEP]
simp only [central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℕ
x y : A
⊢ ↑(↑n).snd x * y = x * ↑(↑n).fst y
[PROOFSTEP]
rw [Prod.snd_natCast, Prod.fst_natCast]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℕ
x y : A
⊢ ↑↑n x * y = x * ↑↑n y
[PROOFSTEP]
simp only [← Nat.smul_one_eq_coe, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ ↑(↑n).snd x * y = x * ↑(↑n).fst y
[PROOFSTEP]
rw [Prod.snd_intCast, Prod.fst_intCast]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ ↑↑n x * y = x * ↑↑n y
[PROOFSTEP]
simp only [← Int.smul_one_eq_coe, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
n : ℕ
x y : A
⊢ ↑(a.toProd ^ n).snd x * y = x * ↑(a.toProd ^ n).fst y
[PROOFSTEP]
induction' n with k hk generalizing x y
[GOAL]
case zero
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x✝ y✝ x y : A
⊢ ↑(a.toProd ^ Nat.zero).snd x * y = x * ↑(a.toProd ^ Nat.zero).fst y
[PROOFSTEP]
rfl
[GOAL]
case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x✝ y✝ : A
k : ℕ
hk : ∀ (x y : A), ↑(a.toProd ^ k).snd x * y = x * ↑(a.toProd ^ k).fst y
x y : A
⊢ ↑(a.toProd ^ Nat.succ k).snd x * y = x * ↑(a.toProd ^ Nat.succ k).fst y
[PROOFSTEP]
rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
[GOAL]
case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x✝ y✝ : A
k : ℕ
hk : ∀ (x y : A), ↑(a.snd ^ k) x * y = x * ↑(a.fst ^ k) y
x y : A
⊢ ↑(a.snd ^ Nat.succ k) x * y = x * ↑(a.fst ^ Nat.succ k) y
[PROOFSTEP]
rw [pow_succ a.snd, mul_apply, a.central, hk, pow_succ' a.fst, mul_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ
⊢ x ∈ Set.range toProdMulOpposite → x ∈ {lr | ∀ (x y : A), ↑(unop lr.snd) x * y = x * ↑lr.fst y}
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ toProdMulOpposite a ∈ {lr | ∀ (x y : A), ↑(unop lr.snd) x * y = x * ↑lr.fst y}
[PROOFSTEP]
exact a.central
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
k : 𝕜
x y : A
⊢ ↑(↑(algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k).snd x * y =
    x * ↑(↑(algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k).fst y
[PROOFSTEP]
simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
a : 𝓜(𝕜, A)
x y : A
⊢ ↑(comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.snd)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv),
              comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.fst)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)).snd
        x *
      y =
    x *
      ↑(comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.snd)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv),
              comp (comp (↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)) a.fst)
                ↑(ContinuousLinearEquiv.mk (starₗᵢ 𝕜).toLinearEquiv)).fst
        y
[PROOFSTEP]
simpa only [star_mul, star_star] using (congr_arg star (a.central (star y) (star x))).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x : 𝓜(𝕜, A)
⊢ star (star x) = x
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (star x)).fst x✝ = ↑x.fst x✝
[PROOFSTEP]
simp only [star_fst, star_snd, star_star]
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (star x)).snd x✝ = ↑x.snd x✝
[PROOFSTEP]
simp only [star_fst, star_snd, star_star]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x y : 𝓜(𝕜, A)
⊢ star (x + y) = star x + star y
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x y : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (x + y)).fst x✝ = ↑(star x + star y).fst x✝
[PROOFSTEP]
simp only [star_fst, star_snd, add_fst, add_snd, ContinuousLinearMap.add_apply, star_add]
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : Star 𝓜(𝕜, A) := instStar
x y : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (x + y)).snd x✝ = ↑(star x + star y).snd x✝
[PROOFSTEP]
simp only [star_fst, star_snd, add_fst, add_snd, ContinuousLinearMap.add_apply, star_add]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
a b : 𝓜(𝕜, A)
⊢ star (a * b) = star b * star a
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
a b : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (a * b)).fst x✝ = ↑(star b * star a).fst x✝
[PROOFSTEP]
simp only [star_fst, star_snd, mul_fst, mul_snd, star_star, ContinuousLinearMap.coe_mul, Function.comp_apply]
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
a b : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (a * b)).snd x✝ = ↑(star b * star a).snd x✝
[PROOFSTEP]
simp only [star_fst, star_snd, mul_fst, mul_snd, star_star, ContinuousLinearMap.coe_mul, Function.comp_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
k : 𝕜
a : 𝓜(𝕜, A)
⊢ star (k • a) = star k • star a
[PROOFSTEP]
ext
[GOAL]
case h.h₁.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
k : 𝕜
a : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (k • a)).fst x✝ = ↑(star k • star a).fst x✝
[PROOFSTEP]
exact star_smul _ _
[GOAL]
case h.h₂.h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
src✝ : StarAddMonoid 𝓜(𝕜, A) := instStarAddMonoid
k : 𝕜
a : 𝓜(𝕜, A)
x✝ : A
⊢ ↑(star (k • a)).snd x✝ = ↑(star k • star a).snd x✝
[PROOFSTEP]
exact star_smul _ _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
⊢ ↑𝕜 = ↑(algebraMap 𝕜 𝓜(𝕜, 𝕜))
[PROOFSTEP]
ext x : 3
[GOAL]
case h.h.h₁
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : 𝕜
⊢ (↑𝕜 x).toProd.fst = (↑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).fst
[PROOFSTEP]
rfl
  -- `fst` is defeq
[GOAL]
case h.h.h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : 𝕜
⊢ (↑𝕜 x).toProd.snd = (↑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).snd
[PROOFSTEP]
refine ContinuousLinearMap.ext fun y => ?_
[GOAL]
case h.h.h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x y : 𝕜
⊢ ↑(↑𝕜 x).toProd.snd y = ↑(↑(algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).snd y
[PROOFSTEP]
exact mul_comm y x
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
⊢ Function.Injective ↑toProdMulOppositeHom
[PROOFSTEP]
simpa using toProdMulOpposite_injective
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ CompleteSpace 𝓜(𝕜, A)
[PROOFSTEP]
rw [completeSpace_iff_isComplete_range uniformEmbedding_toProdMulOpposite.toUniformInducing]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsComplete (Set.range toProdMulOpposite)
[PROOFSTEP]
apply IsClosed.isComplete
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsClosed (Set.range toProdMulOpposite)
[PROOFSTEP]
simp only [range_toProdMulOpposite, Set.setOf_forall]
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsClosed (⋂ (i : A) (i_1 : A), {x | ↑(unop x.snd) i * i_1 = i * ↑x.fst i_1})
[PROOFSTEP]
refine' isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq _ _
[GOAL]
case h.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 => ↑(unop x_1.snd) x * y
case h.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 => x * ↑x_1.fst y
[PROOFSTEP]
exact ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp <| continuous_unop.comp continuous_snd).mul continuous_const
[GOAL]
case h.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 => x * ↑x_1.fst y
[PROOFSTEP]
exact continuous_const.mul ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp continuous_fst)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
have h0 : ∀ f : A →L[𝕜] A, ∀ C : ℝ≥0, (∀ b : A, ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C :=
  by
  intro f C h
  have h1 : ∀ b, C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 :=
    by
    intro b
    convert mul_le_mul_right' (mul_le_mul_left' (f.le_op_nnnorm b) C) ‖b‖₊ using 1
    ring
  have :=
    NNReal.div_le_of_le_mul
      (f.op_nnnorm_le_bound _
        (by simpa only [sqrt_sq, sqrt_mul] using fun b => sqrt_le_sqrt_iff.mpr ((h b).trans (h1 b))))
  convert NNReal.rpow_le_rpow this two_pos.le
  · simp only [NNReal.rpow_two, div_pow, sq_sqrt]
    simp only [sq, mul_self_div_self]
  · simp only [NNReal.rpow_two, sq_sqrt]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
[PROOFSTEP]
intro f C h
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
⊢ ‖f‖₊ ≤ C
[PROOFSTEP]
have h1 : ∀ b, C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 :=
  by
  intro b
  convert mul_le_mul_right' (mul_le_mul_left' (f.le_op_nnnorm b) C) ‖b‖₊ using 1
  ring
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
⊢ ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
[PROOFSTEP]
intro b
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
b : A
⊢ C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
[PROOFSTEP]
convert mul_le_mul_right' (mul_le_mul_left' (f.le_op_nnnorm b) C) ‖b‖₊ using 1
[GOAL]
case h.e'_4
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
b : A
⊢ C * ‖f‖₊ * ‖b‖₊ ^ 2 = C * (‖f‖₊ * ‖b‖₊) * ‖b‖₊
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
⊢ ‖f‖₊ ≤ C
[PROOFSTEP]
have :=
  NNReal.div_le_of_le_mul
    (f.op_nnnorm_le_bound _
      (by simpa only [sqrt_sq, sqrt_mul] using fun b => sqrt_le_sqrt_iff.mpr ((h b).trans (h1 b))))
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
⊢ ∀ (x : A), ‖↑f x‖₊ ≤ ?m.1273079 * ?m.1273080 * ‖x‖₊
[PROOFSTEP]
simpa only [sqrt_sq, sqrt_mul] using fun b => sqrt_le_sqrt_iff.mpr ((h b).trans (h1 b))
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ ‖f‖₊ ≤ C
[PROOFSTEP]
convert NNReal.rpow_le_rpow this two_pos.le
[GOAL]
case h.e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ ‖f‖₊ = (‖f‖₊ / ↑sqrt ‖f‖₊) ^ 2
[PROOFSTEP]
simp only [NNReal.rpow_two, div_pow, sq_sqrt]
[GOAL]
case h.e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ ‖f‖₊ = ‖f‖₊ ^ 2 / ‖f‖₊
[PROOFSTEP]
simp only [sq, mul_self_div_self]
[GOAL]
case h.e'_4
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖↑f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / ↑sqrt ‖f‖₊ ≤ ↑sqrt C
⊢ C = ↑sqrt C ^ 2
[PROOFSTEP]
simp only [NNReal.rpow_two, sq_sqrt]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
have h1 : ∀ b, ‖a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ :=
  by
  intro b
  calc
    ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by simpa only [← sq] using CstarRing.nnnorm_star_mul_self.symm
    _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
    _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ := nnnorm_star (a.fst b) ▸ mul_le_mul_right' (a.snd.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
⊢ ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
[PROOFSTEP]
intro b
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
b : A
⊢ ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
[PROOFSTEP]
calc
  ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by simpa only [← sq] using CstarRing.nnnorm_star_mul_self.symm
  _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
  _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ := nnnorm_star (a.fst b) ▸ mul_le_mul_right' (a.snd.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
b : A
⊢ ‖↑a.fst b‖₊ ^ 2 = ‖star (↑a.fst b) * ↑a.fst b‖₊
[PROOFSTEP]
simpa only [← sq] using CstarRing.nnnorm_star_mul_self.symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
have h2 : ∀ b, ‖a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ :=
  by
  intro b
  calc
    ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by simpa only [← sq] using CstarRing.nnnorm_self_mul_star.symm
    _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ := ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
    _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := (mul_comm _ _)
    _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ := nnnorm_star (a.snd b) ▸ mul_le_mul_right' (a.fst.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
⊢ ∀ (b : A), ‖↑a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖↑a.snd b‖₊ * ‖b‖₊
[PROOFSTEP]
intro b
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
b : A
⊢ ‖↑a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖↑a.snd b‖₊ * ‖b‖₊
[PROOFSTEP]
calc
  ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by simpa only [← sq] using CstarRing.nnnorm_self_mul_star.symm
  _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ := ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
  _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := (mul_comm _ _)
  _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ := nnnorm_star (a.snd b) ▸ mul_le_mul_right' (a.fst.le_op_nnnorm _) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
b : A
⊢ ‖↑a.snd b‖₊ ^ 2 = ‖↑a.snd b * star (↑a.snd b)‖₊
[PROOFSTEP]
simpa only [← sq] using CstarRing.nnnorm_self_mul_star.symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖↑f b‖₊ ^ 2 ≤ C * ‖↑f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖↑a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖↑a.fst b‖₊ * ‖b‖₊
h2 : ∀ (b : A), ‖↑a.snd b‖₊ ^ 2 ≤ ‖a.fst‖₊ * ‖↑a.snd b‖₊ * ‖b‖₊
⊢ ‖a.fst‖ = ‖a.snd‖
[PROOFSTEP]
exact le_antisymm (h0 _ _ h1) (h0 _ _ h2)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.fst‖ = ‖a‖
[PROOFSTEP]
simp only [norm_def, toProdHom_apply, Prod.norm_def, norm_fst_eq_snd, max_eq_right le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CstarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.snd‖ = ‖a‖
[PROOFSTEP]
rw [← norm_fst, norm_fst_eq_snd]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
have hball : (Metric.closedBall (0 : A) 1).Nonempty := Metric.nonempty_closedBall.2 zero_le_one
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
have key : ∀ x y, ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.snd (star (a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊ :=
  by
  intro x y hx hy
  rw [a.central]
  calc
    ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
      nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
    _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
      (mul_le_mul' (a.fst.le_op_norm_of_le ((nnnorm_star x).trans_le hx)) (a.fst.le_op_norm_of_le hy))
    _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
⊢ ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
intro x y hx hy
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rw [a.central]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖star (↑a.fst (star x)) * ↑a.fst y‖₊ ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
calc
  ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
    nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
  _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
    (mul_le_mul' (a.fst.le_op_norm_of_le ((nnnorm_star x).trans_le hx)) (a.fst.le_op_norm_of_le hy))
  _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [mul_one, nnnorm_fst, le_rfl]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rw [← nnnorm_snd]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ‖(star a * a).snd‖₊ = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [mul_snd, ← sSup_closed_unit_ball_eq_nnnorm, star_snd, mul_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup ((fun a_1 => ‖↑a.snd (star (↑a.fst (star a_1)))‖₊) '' Metric.closedBall 0 1) = ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [← @_root_.op_nnnorm_mul 𝕜 A]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup ((fun a_1 => ‖↑(ContinuousLinearMap.mul 𝕜 A) (↑a.snd (star (↑a.fst (star a_1))))‖₊) '' Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
simp only [← sSup_closed_unit_ball_eq_nnnorm, mul_apply']
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun a_1 => sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
refine' csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) _ fun r hr => _
[GOAL]
case refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ∀ (a_1 : ℝ≥0),
    a_1 ∈
        (fun a_2 => sSup ((fun a_3 => ‖↑a.snd (star (↑a.fst (star a_2))) * a_3‖₊) '' Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1 →
      a_1 ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rintro - ⟨x, hx, rfl⟩
[GOAL]
case refine'_1.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
⊢ (fun a_1 => sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)) x ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
refine' csSup_le (hball.image _) _
[GOAL]
case refine'_1.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
⊢ ∀ (b : ℝ≥0), b ∈ (fun a_1 => ‖↑a.snd (star (↑a.fst (star x))) * a_1‖₊) '' Metric.closedBall 0 1 → b ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
rintro - ⟨y, hy, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
y : A
hy : y ∈ Metric.closedBall 0 1
⊢ (fun a_1 => ‖↑a.snd (star (↑a.fst (star x))) * a_1‖₊) y ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
⊢ ∃ a_1,
    a_1 ∈
        (fun a_2 => sSup ((fun a_3 => ‖↑a.snd (star (↑a.fst (star a_2))) * a_3‖₊) '' Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1 ∧
      r < a_1
[PROOFSTEP]
simp only [Set.mem_image, Set.mem_setOf_eq, exists_prop, exists_exists_and_eq_and]
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
have hr' : NNReal.sqrt r < ‖a‖₊ := ‖a‖₊.sqrt_mul_self ▸ NNReal.sqrt_lt_sqrt_iff.2 hr
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < ‖a‖₊
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
simp_rw [← nnnorm_fst, ← sSup_closed_unit_ball_eq_nnnorm] at hr' 
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
obtain ⟨_, ⟨x, hx, rfl⟩, hxr⟩ := exists_lt_of_lt_csSup (hball.image _) hr'
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
have hx' : ‖x‖₊ ≤ 1 := mem_closedBall_zero_iff.1 hx
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ ∃ a_1,
    a_1 ∈ Metric.closedBall 0 1 ∧
      r < sSup ((fun a_2 => ‖↑a.snd (star (↑a.fst (star a_1))) * a_2‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
refine' ⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < sSup ((fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
refine' lt_csSup_of_lt _ ⟨x, hx, rfl⟩ _
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ BddAbove ((fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
refine' ⟨‖a‖₊ * ‖a‖₊, _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ ‖a‖₊ * ‖a‖₊ ∈ upperBounds ((fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) '' Metric.closedBall 0 1)
[PROOFSTEP]
rintro - ⟨y, hy, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_1.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
y : A
hy : y ∈ Metric.closedBall 0 1
⊢ (fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) y ≤ ‖a‖₊ * ‖a‖₊
[PROOFSTEP]
exact key (star x) y ((nnnorm_star x).trans_le hx') (mem_closedBall_zero_iff.1 hy)
[GOAL]
case refine'_2.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CstarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty (Metric.closedBall 0 1)
key :
  ∀ (x : A) (y : (fun x => A) (star (↑a.fst (star x)))),
    ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖↑a.snd (star (↑a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : ↑sqrt r < sSup ((fun a_1 => ‖↑a.fst a_1‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : ↑sqrt r < (fun a_1 => ‖↑a.fst a_1‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < (fun a_1 => ‖↑a.snd (star (↑a.fst (star (star x)))) * a_1‖₊) x
[PROOFSTEP]
simpa only [a.central, star_star, CstarRing.nnnorm_star_mul_self, NNReal.sq_sqrt, ← sq] using
  pow_lt_pow_of_lt_left hxr zero_le' two_pos
