-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
@[simp]
lemma inner_single_right [DecidableEq ι] (x : C⋆ᵐᵒᵈ (Π i, E i)) {i : ι} (y : E i) :
    ⟪x, equiv _ |>.symm <| Pi.single i y⟫_A = ⟪x i, y⟫_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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ⟪x i, Pi.single i y i⟫_A = ⟪x i, y⟫_A

case h₀
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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ⟪x b, Pi.single i y b⟫_A = 0

case h₁
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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪x i, Pi.single i y i⟫_A = 0

Tactic:
all_goals simp_all

Result:
no goals

Proof state:
case h₁
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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪x i, Pi.single i y i⟫_A = 0

Tactic:
simp_all

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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ⟪x, (equiv ((i : ι) → E i)).symm (Pi.single i y)⟫_A = ⟪x i, y⟫_A

Tactic:
simp only [pi_inner, equiv_symm_pi_apply]

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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ∑ x_1 : ι, ⟪x x_1, Pi.single i y x_1⟫_A = ⟪x i, y⟫_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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ∑ x_1 : ι, ⟪x x_1, Pi.single i y x_1⟫_A = ⟪x i, y⟫_A

Tactic:
rw [Finset.sum_eq_single i]

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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ⟪x i, Pi.single i y i⟫_A = ⟪x i, y⟫_A

case h₀
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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ⟪x b, Pi.single i y b⟫_A = 0

case h₁
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 ι
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪x i, Pi.single i y i⟫_A = 0