-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem OrthogonalFamily.projection_directSum_coeAddHom [DecidableEq ι] {V : ι → Submodule 𝕜 E}
    (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (x : ⨁ i, V i) (i : ι)
    [CompleteSpace (V i)] :
    orthogonalProjection (V i) (DirectSum.coeAddMonoidHom V x) = x i

Proof state:
case H_plus
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) (x + y)) = (x + y) i

Tactic:
simp_rw [map_add]

Result:
case H_plus
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) +
      (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) y) =
    (x + y) i

Proof state:
case H_zero
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) 0) = 0 i

Tactic:
simp

Result:
no goals

Proof state:
case H_basic
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) ((of (fun i => ↥(V i)) j) x)) =
    ((of (fun i => ↥(V i)) j) x) i

Tactic:
simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of]

Result:
case H_basic
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
⊢ (orthogonalProjection (V i)) ↑x = ((DFinsupp.singleAddHom (fun i => ↥(V i)) j) x) i

Proof state:
case H_basic.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ ↑x ∈ (V i)ᗮ

Tactic:
exact hV.isOrtho hij.symm x.prop

Result:
no goals

Proof state:
case H_basic.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (orthogonalProjection (V i)) ↑x = (DFinsupp.single j x) i

Tactic:
rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
  DFinsupp.single_eq_of_ne hij.symm]

Result:
case H_basic.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ ↑x ∈ (V i)ᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
x : ⨁ (i : ι), ↥(V i)
i : ι
inst✝ : CompleteSpace ↥(V i)
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i

Tactic:
induction' x using DirectSum.induction_on with j x x y hx hy

Result:
case H_zero
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) 0) = 0 i

case H_basic
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) ((of (fun i => ↥(V i)) j) x)) =
    ((of (fun i => ↥(V i)) j) x) i

case H_plus
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) (x + y)) = (x + y) i

Proof state:
case H_basic
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
⊢ (orthogonalProjection (V i)) ↑x = ((DFinsupp.singleAddHom (fun i => ↥(V i)) j) x) i

Tactic:
erw [DFinsupp.singleAddHom_apply]

Result:
case H_basic
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
⊢ (orthogonalProjection (V i)) ↑x = (DFinsupp.single j x) i

Proof state:
case H_basic
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
⊢ (orthogonalProjection (V i)) ↑x = (DFinsupp.single j x) i

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case H_basic.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x : ↥(V i)
⊢ (orthogonalProjection (V i)) ↑x = (DFinsupp.single i x) i

case H_basic.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (orthogonalProjection (V i)) ↑x = (DFinsupp.single j x) i