-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.inner_right_dfinsupp
    [∀ (i) (x : G i), Decidable (x ≠ 0)] [DecidableEq ι] (l : ⨁ i, G i) (i : ι) (v : G i) :
    ⟪V i v, l.sum fun j => V j⟫ = ⟪v, l i⟫ :=
  calc
    ⟪V i v, l.sum fun j => V j⟫ = l.sum fun j => fun w => ⟪V i v, V j w⟫ :=
      DFinsupp.inner_sum (fun j => V j) l (V i v)
    _ = l.sum fun j => fun w => ite (i = j) ⟪V i v, V j w⟫ 0 :=
      (congr_arg l.sum <| funext fun _ => funext <| hV.eq_ite v)
    _ = ⟪v, l i⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
⊢ (if l i ≠ 0 then inner ((V i) v) ((V i) (l i)) else 0) = inner v (l i)

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
h : l i ≠ 0
⊢ inner ((V i) v) ((V i) (l i)) = inner v (l i)

case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
h : ¬l i ≠ 0
⊢ 0 = inner v (l i)

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
h : ¬l i ≠ 0
⊢ 0 = inner v (l i)

Tactic:
simp only [of_not_not h, inner_zero_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
⊢ (DFinsupp.sum l fun j w => if i = j then inner ((V i) v) ((V j) w) else 0) = inner v (l i)

Tactic:
simp only [DFinsupp.sum, Submodule.coe_inner, Finset.sum_ite_eq, ite_eq_left_iff,
  DFinsupp.mem_support_toFun]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
⊢ (if l i ≠ 0 then inner ((V i) v) ((V i) (l i)) else 0) = inner v (l i)

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst✝ : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
h : l i ≠ 0
⊢ inner ((V i) v) ((V i) (l i)) = inner v (l i)

Tactic:
simp only [LinearIsometry.inner_map_map]

Result:
no goals