-- Mathlib/Analysis/CStarAlgebra/Unitization.lean
lemma opNorm_mul_flip_apply (a : E) : ‖(mul 𝕜 E).flip a‖ = ‖a‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a : E
this : ‖(mul 𝕜 E) a⋆‖ ≤ ‖(mul 𝕜 E).flip a‖
⊢ ‖a‖ ≤ ‖(mul 𝕜 E).flip a‖

Tactic:
simpa only [ge_iff_le, opNorm_mul_apply, norm_star] using this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E).flip a) b‖ ≤ ‖a‖ * ‖b‖

Tactic:
simpa only [mul_comm] using norm_mul_le b a

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E).flip a) b⋆‖ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖

Tactic:
simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E) a⋆) b‖ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖

Tactic:
calc ‖mul 𝕜 E (star a) b‖ = ‖(mul 𝕜 E).flip a (star b)‖ := by
      simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)
  _ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖ := by
      simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a : E
⊢ ‖(mul 𝕜 E) a⋆‖ ≤ ‖(mul 𝕜 E).flip a‖

Tactic:
refine opNorm_le_bound _ (norm_nonneg _) fun b => ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E) a⋆) b‖ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a : E
⊢ ‖(mul 𝕜 E).flip a‖ = ‖a‖

Tactic:
refine le_antisymm
  (opNorm_le_bound _ (norm_nonneg _) fun b => by simpa only [mul_comm] using norm_mul_le b a) ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a : E
⊢ ‖a‖ ≤ ‖(mul 𝕜 E).flip a‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a b : E
⊢ ‖((mul 𝕜 E) a⋆) b‖ = ‖((mul 𝕜 E).flip a) b⋆‖

Tactic:
simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a : E
⊢ ‖a‖ ≤ ‖(mul 𝕜 E).flip a‖

Tactic:
suffices ‖mul 𝕜 E (star a)‖ ≤ ‖(mul 𝕜 E).flip a‖ by
  simpa only [ge_iff_le, opNorm_mul_apply, norm_star] using this

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NonUnitalNormedRing E
inst✝⁵ : StarRing E
inst✝⁴ : NormedStarGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : IsScalarTower 𝕜 E E
inst✝¹ : SMulCommClass 𝕜 E E
inst✝ : RegularNormedAlgebra 𝕜 E
a : E
⊢ ‖(mul 𝕜 E) a⋆‖ ≤ ‖(mul 𝕜 E).flip a‖