Theorem: Submodule.mem_orthogonal_Basis (src/Pre.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ v ∈ Kᗮ ↔ ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
rw [Submodule.mem_orthogonal]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) ↔ ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) ↔ ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
constructor
State after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) → ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0

case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0) → ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0

State before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ u ∈ K, ⟪u, v⟫_𝕜 = 0) → ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
intro h i
State after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
i : ι
⊢ ⟪↑(b i), v⟫_𝕜 = 0

State before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
i : ι
⊢ ⟪↑(b i), v⟫_𝕜 = 0
Tactic:
exact h _ (Submodule.coe_mem (b i))
State after:
no goals

State before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
⊢ (∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0) → ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
Tactic:
intro h x hx
State after:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : x ∈ K
⊢ ⟪x, v⟫_𝕜 = 0

State before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : x ∈ K
⊢ ⟪x, v⟫_𝕜 = 0
Tactic:
rw [Basis.mem_submodule_iff b] at hx
State after:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : ∃ c, x = Finsupp.sum c fun i x => x • ↑(b i)
⊢ ⟪x, v⟫_𝕜 = 0

State before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
x : E
hx : ∃ c, x = Finsupp.sum c fun i x => x • ↑(b i)
⊢ ⟪x, v⟫_𝕜 = 0
Tactic:
rcases hx with ⟨ a, rfl ⟩
State after:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ⟪Finsupp.sum a fun i x => x • ↑(b i), v⟫_𝕜 = 0

State before:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ⟪Finsupp.sum a fun i x => x • ↑(b i), v⟫_𝕜 = 0
Tactic:
rw [Finsupp.sum_inner]
State after:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ (Finsupp.sum a fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) = 0

State before:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ (Finsupp.sum a fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) = 0
Tactic:
apply Finset.sum_eq_zero
State after:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ∀ x ∈ a.support, (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) x (a x) = 0

State before:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
⊢ ∀ x ∈ a.support, (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) x (a x) = 0
Tactic:
intro i _
State after:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
i : ι
a✝ : i ∈ a.support
⊢ (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) i (a i) = 0

State before:
case mpr.intro.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
b : Basis ι 𝕜 ↥K
v : E
h : ∀ (i : ι), ⟪↑(b i), v⟫_𝕜 = 0
a : ι →₀ 𝕜
i : ι
a✝ : i ∈ a.support
⊢ (fun i a => (starRingEnd 𝕜) a • ⟪↑(b i), v⟫_𝕜) i (a i) = 0
Tactic:
simp only [h i, smul_eq_mul, mul_zero]
State after:
no goals