-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
@[simp]
lemma norm_single [DecidableEq ι] (i : ι) (y : E i) :
    ‖equiv _ |>.symm <| Pi.single i y‖ = ‖y‖

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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ 0 ≤ ‖(equiv ((j : ι) → E j)).symm (Pi.single i y)‖

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
inst✝ : DecidableEq ι
i : ι
y : E i
⊢ ‖(equiv ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖

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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖(equiv ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖

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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖(equiv ((j : ι) → E j)).symm (Pi.single i y)‖ ^ 2 = ‖y‖ ^ 2

Tactic:
simp [norm_sq_eq]

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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ 0 ≤ ‖y‖

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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖(equiv ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity)]

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
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖(equiv ((j : ι) → E j)).symm (Pi.single i y)‖ ^ 2 = ‖y‖ ^ 2