-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma norm_apply_le_norm (x : C⋆ᵐᵒᵈ (Π i, E i)) (i : ι) : ‖x i‖ ≤ ‖x‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖x i‖ ≤ ‖x‖

Tactic:
refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖x i‖ ^ 2 ≤ ‖x‖ ^ 2

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖⟪x i, x i⟫_A‖ ≤ ‖∑ i : ι, ⟪x i, x i⟫_A‖

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖x i‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
rw [pi_norm_sq, norm_sq_eq]

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖⟪x i, x i⟫_A‖ ≤ ‖∑ i : ι, ⟪x i, x i⟫_A‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ 0 ≤ ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ⟪x i, x i⟫_A ≤ ∑ i : ι, ⟪x i, x i⟫_A

Tactic:
exact Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (x := x j)) (Finset.mem_univ i)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
⊢ ‖x i‖ ≤ ‖x‖

Tactic:
let _ : NormedAddCommGroup (C⋆ᵐᵒᵈ (Π i, E i)) := normedAddCommGroup

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖x i‖ ≤ ‖x‖