-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma max_le_prod_norm (x : C⋆ᵐᵒᵈ (E × F)) : max ‖x.1‖ ‖x.2‖ ≤ ‖x‖

Proof state:
case right.ha
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ autoParam (0 ≤ ⟪x.2, x.2⟫_A) _auto✝

case right.hab
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
all_goals
  aesop (add safe apply CStarModule.inner_self_nonneg)

Result:
no goals

Proof state:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖x.1‖ ⊔ ‖x.2‖ ≤ √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
simp only [equiv_fst, norm_eq_sqrt_norm_inner_self (E := E),
  norm_eq_sqrt_norm_inner_self (E := F), equiv_snd, max_le_iff, norm_nonneg,
  Real.sqrt_le_sqrt_iff]

Result:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Proof state:
case left
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

case right
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
all_goals
  apply CStarAlgebra.norm_le_norm_of_nonneg_of_le
  all_goals
    aesop (add safe apply CStarModule.inner_self_nonneg)

Result:
no goals

Proof state:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖x.1‖ ⊔ ‖x.2‖ ≤ ‖x‖

Tactic:
rw [prod_norm]

Result:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖x.1‖ ⊔ ‖x.2‖ ≤ √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Proof state:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
constructor

Result:
case left
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

case right
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Proof state:
case right.hab
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Result:
no goals

Proof state:
case right
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
apply CStarAlgebra.norm_le_norm_of_nonneg_of_le

Result:
case right.ha
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ autoParam (0 ≤ ⟪x.2, x.2⟫_A) _auto✝

case right.hab
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ (E × F)
⊢ ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A