-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem sum_inner_mul_inner (b : OrthonormalBasis ι 𝕜 E) (x y : E) :
    ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ((innerSL 𝕜) x) (∑ i : ι, b.repr y i • b i) = ((innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (b i) * inner (b i) y = inner x y

Tactic:
rw [map_sum] at this

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ((innerSL 𝕜) x) (b.repr y x_1 • b x_1) = ((innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (b i) * inner (b i) y = inner x y

Proof state:
case h.e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ((innerSL 𝕜) x) (b.repr y x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner x (b x✝) * inner (b x✝) y = ((innerSL 𝕜) x) (b.repr y x✝ • b x✝)

Tactic:
rw [map_smul, b.repr_apply_apply, mul_comm]

Result:
case h.e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ((innerSL 𝕜) x) (b.repr y x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (b x✝) y * inner x (b x✝) = inner (b x✝) y • ((innerSL 𝕜) x) (b x✝)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
⊢ ∑ i : ι, inner x (b i) * inner (b i) y = inner x y

Tactic:
have := congr_arg (innerSL 𝕜 x) (b.sum_repr y)

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ((innerSL 𝕜) x) (∑ i : ι, b.repr y i • b i) = ((innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (b i) * inner (b i) y = inner x y

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ((innerSL 𝕜) x) (b.repr y x_1 • b x_1) = ((innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (b i) * inner (b i) y = inner x y

Tactic:
convert this

Result:
case h.e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ((innerSL 𝕜) x) (b.repr y x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner x (b x✝) * inner (b x✝) y = ((innerSL 𝕜) x) (b.repr y x✝ • b x✝)

Proof state:
case h.e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ((innerSL 𝕜) x) (b.repr y x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (b x✝) y * inner x (b x✝) = inner (b x✝) y • ((innerSL 𝕜) x) (b x✝)

Tactic:
simp only [innerSL_apply, smul_eq_mul]

Result:
no goals