-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.independent {V : ι → Submodule 𝕜 E}
    (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) :
    iSupIndep V

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ ∀ x ∈ LinearMap.ker ((DFinsupp.lsum ℕ) fun i => (V i).subtype), x = 0

Tactic:
intro v hv

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : v ∈ LinearMap.ker ((DFinsupp.lsum ℕ) fun i => (V i).subtype)
⊢ v = 0

Proof state:
case h.h.a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
⊢ inner ↑(v i) ↑(v i) = 0

Tactic:
calc
  ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
    simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
      (hV.inner_right_dfinsupp v i (v i)).symm
  _ = 0 := by simp only [hv, inner_zero_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
⊢ inner (↑(v i)) (((DFinsupp.lsum ℕ) fun i => (V i).subtype) v) = 0

Tactic:
simp only [hv, inner_zero_right]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
⊢ v = 0

Tactic:
ext i

Result:
case h.h.a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
⊢ ↑(v i) = ↑(0 i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
⊢ inner ↑(v i) ↑(v i) = inner (↑(v i)) (((DFinsupp.lsum ℕ) fun i => (V i).subtype) v)

Tactic:
simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
  (hV.inner_right_dfinsupp v i (v i)).symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ iSupIndep V

Tactic:
classical
apply iSupIndep_of_dfinsupp_lsum_injective
refine LinearMap.ker_eq_bot.mp ?_
rw [Submodule.eq_bot_iff]
intro v hv
rw [LinearMap.mem_ker] at hv
ext i
suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
calc
  ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
    simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
      (hV.inner_right_dfinsupp v i (v i)).symm
  _ = 0 := by simp only [hv, inner_zero_right]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : v ∈ LinearMap.ker ((DFinsupp.lsum ℕ) fun i => (V i).subtype)
⊢ v = 0

Tactic:
rw [LinearMap.mem_ker] at hv

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
⊢ v = 0

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (V i).subtype)

Tactic:
refine LinearMap.ker_eq_bot.mp ?_

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ LinearMap.ker ((DFinsupp.lsum ℕ) fun i => (V i).subtype) = ⊥

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ LinearMap.ker ((DFinsupp.lsum ℕ) fun i => (V i).subtype) = ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ ∀ x ∈ LinearMap.ker ((DFinsupp.lsum ℕ) fun i => (V i).subtype), x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ iSupIndep V

Tactic:
apply iSupIndep_of_dfinsupp_lsum_injective

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (V i).subtype)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
this : inner ↑(v i) ↑(v i) = 0
⊢ ↑(v i) = ↑(0 i)

Tactic:
simpa only [inner_self_eq_zero] using this

Result:
no goals

Proof state:
case h.h.a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
⊢ ↑(v i) = ↑(0 i)

Tactic:
suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this

Result:
case h.h.a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i => (V i).subtype) v = 0
i : ι
⊢ inner ↑(v i) ↑(v i) = 0