[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
x : ℝ
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
simp only [star, id.def, norm_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
⊢ ∀ (x : E), ‖x⋆‖ = ‖x‖
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
by_cases htriv : x = 0
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : x = 0
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
simp only [htriv, star_zero]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have hnt : 0 < ‖x‖ := norm_pos_iff.mpr htriv
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have hnt_star : 0 < ‖x⋆‖ := norm_pos_iff.mpr ((AddEquiv.map_ne_zero_iff starAddEquiv (M := E)).mpr htriv)
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have h₁ :=
  calc
    ‖x‖ * ‖x‖ = ‖x⋆ * x‖ := norm_star_mul_self.symm
    _ ≤ ‖x⋆‖ * ‖x‖ := norm_mul_le _ _
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
h₁ : ‖x‖ * ‖x‖ ≤ ‖x⋆‖ * ‖x‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
have h₂ :=
  calc
    ‖x⋆‖ * ‖x⋆‖ = ‖x * x⋆‖ := by rw [← norm_star_mul_self, star_star]
    _ ≤ ‖x‖ * ‖x⋆‖ := norm_mul_le _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
h₁ : ‖x‖ * ‖x‖ ≤ ‖x⋆‖ * ‖x‖
⊢ ‖x⋆‖ * ‖x⋆‖ = ‖x * x⋆‖
[PROOFSTEP]
rw [← norm_star_mul_self, star_star]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
htriv : ¬x = 0
hnt : 0 < ‖x‖
hnt_star : 0 < ‖x⋆‖
h₁ : ‖x‖ * ‖x‖ ≤ ‖x⋆‖ * ‖x‖
h₂ : ‖x⋆‖ * ‖x⋆‖ ≤ ‖x‖ * ‖x⋆‖
⊢ ‖x⋆‖ = ‖x‖
[PROOFSTEP]
exact le_antisymm (le_of_mul_le_mul_right h₂ hnt_star) (le_of_mul_le_mul_right h₁ hnt)
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
nth_rw 1 [← star_star x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
simp only [norm_star_mul_self, norm_star]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖
[PROOFSTEP]
rw [norm_star_mul_self, norm_star]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0
[PROOFSTEP]
rw [← norm_eq_zero, norm_star_mul_self]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0
[PROOFSTEP]
exact mul_self_eq_zero.trans norm_eq_zero
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x⋆ * x ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
simp only [Ne.def, star_mul_self_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x * x⋆ = 0 ↔ x = 0
[PROOFSTEP]
simpa only [star_eq_zero, star_star] using @star_mul_self_eq_zero_iff _ _ _ _ (star x)
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
⊢ x * x⋆ ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
simp only [Ne.def, mul_star_self_eq_zero_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
dsimp only [norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖(x⋆ * x).fst‖ ⊔ ‖(x⋆ * x).snd‖ = (‖x.fst‖ ⊔ ‖x.snd‖) * (‖x.fst‖ ⊔ ‖x.snd‖)
[PROOFSTEP]
simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ^ 2 ⊔ ‖x.snd‖ ^ 2 = (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ^ 2 ⊔ ‖x.snd‖ ^ 2 ≤ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
refine' max_le _ _
[GOAL]
case refine'_1.refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ^ 2 ≤ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
rw [sq_le_sq, abs_of_nonneg (norm_nonneg _)]
[GOAL]
case refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.snd‖ ^ 2 ≤ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2
[PROOFSTEP]
rw [sq_le_sq, abs_of_nonneg (norm_nonneg _)]
[GOAL]
case refine'_1.refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.fst‖ ≤ |‖x.fst‖ ⊔ ‖x.snd‖|
case refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.snd‖ ≤ |‖x.fst‖ ⊔ ‖x.snd‖|
[PROOFSTEP]
exact (le_max_left _ _).trans (le_abs_self _)
[GOAL]
case refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ ‖x.snd‖ ≤ |‖x.fst‖ ⊔ ‖x.snd‖|
[PROOFSTEP]
exact (le_max_right _ _).trans (le_abs_self _)
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ⊔ ‖x.snd‖ ^ 2
[PROOFSTEP]
rw [le_sup_iff]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ∨ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.snd‖ ^ 2
[PROOFSTEP]
rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h)
[GOAL]
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
h : ‖x.fst‖ ≤ ‖x.snd‖
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ∨ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.snd‖ ^ 2
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_2.inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : R₁ × R₂
h : ‖x.snd‖ ≤ ‖x.fst‖
⊢ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.fst‖ ^ 2 ∨ (‖x.fst‖ ⊔ ‖x.snd‖) ^ 2 ≤ ‖x.snd‖ ^ 2
[PROOFSTEP]
simp [h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
simp only [norm, Pi.mul_apply, Pi.star_apply, nnnorm_star_mul_self, ← sq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ ↑(Finset.sup Finset.univ fun b => ‖x b‖₊ ^ 2) = ↑(Finset.sup Finset.univ fun b => ‖x b‖₊) ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ (Finset.sup Finset.univ fun b => ‖x b‖₊ ^ 2) = (Finset.sup Finset.univ fun b => ‖x b‖₊) ^ 2
[PROOFSTEP]
exact
  (Finset.comp_sup_eq_sup_comp_of_is_total (fun x : NNReal => x ^ 2)
      (fun x y h => by simpa only [sq] using mul_le_mul' h h) (by simp)).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ (fun x => x ^ 2) x ≤ (fun x => x ^ 2) y
[PROOFSTEP]
simpa only [sq] using mul_le_mul' h h
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CstarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CstarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CstarRing (R i)
x : (i : ι) → R i
⊢ (fun x => x ^ 2) ⊥ = ⊥
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1
[PROOFSTEP]
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1
[PROOFSTEP]
rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CstarRing E
inst✝ : Nontrivial E
U : { x // x ∈ unitary E }
⊢ ‖↑U‖ = 1
[PROOFSTEP]
rw [← sq_eq_sq (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CstarRing.norm_star_mul_self, unitary.coe_star_mul_self,
  CstarRing.norm_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
⊢ ‖↑U * A‖ = ‖A‖
[PROOFSTEP]
nontriviality E
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ = ‖A‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ ≤ ‖A‖
[PROOFSTEP]
calc
  _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
  _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U‖ * ‖A‖ = ‖A‖
[PROOFSTEP]
rw [norm_coe_unitary, one_mul]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ ≤ ‖↑U * A‖
[PROOFSTEP]
calc
  _ = ‖(U : E)⋆ * U * A‖ := by rw [unitary.coe_star_mul_self U, one_mul]
  _ ≤ ‖(U : E)⋆‖ * ‖(U : E) * A‖ := by
    rw [mul_assoc]
    exact norm_mul_le _ _
  _ = ‖(U : E) * A‖ := by rw [norm_star, norm_coe_unitary, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ = ‖(↑U)⋆ * ↑U * A‖
[PROOFSTEP]
rw [unitary.coe_star_mul_self U, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * ↑U * A‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * (↑U * A)‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
[PROOFSTEP]
exact norm_mul_le _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆‖ * ‖↑U * A‖ = ‖↑U * A‖
[PROOFSTEP]
rw [norm_star, norm_coe_unitary, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
A : E
U : { x // x ∈ unitary E }
⊢ ‖A * ↑U‖ = ‖((↑U)⋆ * A⋆)⋆‖
[PROOFSTEP]
simp only [star_star, star_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
A : E
U : { x // x ∈ unitary E }
⊢ ‖((↑U)⋆ * A⋆)⋆‖ = ‖(↑U)⋆ * A⋆‖
[PROOFSTEP]
rw [norm_star]
[GOAL]
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
[PROOFSTEP]
induction' n with k hk
[GOAL]
case zero
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ Nat.zero‖₊ = ‖x‖₊ ^ 2 ^ Nat.zero
[PROOFSTEP]
simp only [pow_zero, pow_one, Nat.zero_eq]
[GOAL]
case succ
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ Nat.succ k‖₊ = ‖x‖₊ ^ 2 ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ, pow_mul', sq]
[GOAL]
case succ
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
[PROOFSTEP]
nth_rw 1 [← selfAdjoint.mem_iff.mp hx]
[GOAL]
case succ
𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x⋆ ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
[PROOFSTEP]
rw [← star_pow, CstarRing.nnnorm_star_mul_self, ← sq, hk, pow_mul']
