𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ = ‖A‖
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
⊢ ‖↑U * A‖ = ‖A‖
nontriviality E
case refine'_1
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ ≤ ‖A‖

case refine'_2
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ ≤ ‖↑U * A‖
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ = ‖A‖
refine' le_antisymm _ _
no goals
case refine'_1
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U * A‖ ≤ ‖A‖
calc
  _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
  _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]
no goals
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖↑U‖ * ‖A‖ = ‖A‖
rw [norm_coe_unitary, one_mul]
no goals
case refine'_2
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ ≤ ‖↑U * A‖
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]
no goals
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖A‖ = ‖(↑U)⋆ * ↑U * A‖
rw [unitary.coe_star_mul_self U, one_mul]
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * (↑U * A)‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * ↑U * A‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
rw [mul_assoc]
no goals
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆ * (↑U * A)‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖
exact norm_mul_le _ _
no goals
𝕜 : Type ?u.77873
E : Type u_1
α : Type ?u.77879
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
U : { x // x ∈ unitary E }
A : E
✝ : Nontrivial E
⊢ ‖(↑U)⋆‖ * ‖↑U * A‖ = ‖↑U * A‖
rw [norm_star, norm_coe_unitary, one_mul]