-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem inner_single_left [DecidableEq ι] (i : ι) (a : G i) (f : lp G 2) :
    ⟪lp.single 2 i a, f⟫ = ⟪a, f i⟫

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) (inner a (↑f i))

Tactic:
simp_rw [lp.coeFn_single]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun i_1 => inner (Pi.single i a i_1) (↑f i_1)) (inner a (↑f i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun i_1 => inner (Pi.single i a i_1) (↑f i_1)) (inner a (↑f i))

Tactic:
convert hasSum_ite_eq i ⟪a, f i⟫ using 1

Result:
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ (fun i_1 => inner (Pi.single i a i_1) (↑f i_1)) = fun b' => if b' = i then inner a (↑f i) else 0

Proof state:
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ (fun i_1 => inner (Pi.single i a i_1) (↑f i_1)) = fun b' => if b' = i then inner a (↑f i) else 0

Tactic:
ext j

Result:
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
⊢ inner (Pi.single i a j) (↑f j) = if j = i then inner a (↑f i) else 0

Proof state:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
h : j = i
⊢ inner (Pi.single i a j) (↑f j) = inner a (↑f i)

Tactic:
subst h

Result:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
f : ↥(lp G 2)
j : ι
a : G j
⊢ inner (Pi.single j a j) (↑f j) = inner a (↑f j)

Proof state:
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
⊢ inner (Pi.single i a j) (↑f j) = if j = i then inner a (↑f i) else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
h : j = i
⊢ inner (Pi.single i a j) (↑f j) = inner a (↑f i)

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
h : ¬j = i
⊢ inner (Pi.single i a j) (↑f j) = 0

Proof state:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
j : ι
h : ¬j = i
⊢ inner (Pi.single i a j) (↑f j) = 0

Tactic:
simp [Pi.single_eq_of_ne h]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ inner (lp.single 2 i a) f = inner a (↑f i)

Tactic:
refine (hasSum_inner (lp.single 2 i a) f).unique ?_

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) (inner a (↑f i))

Proof state:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
f : ↥(lp G 2)
j : ι
a : G j
⊢ inner (Pi.single j a j) (↑f j) = inner a (↑f j)

Tactic:
rw [Pi.single_eq_same]

Result:
no goals