[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ x = y
[PROOFSTEP]
apply (toDualMap 𝕜 E).map_eq_iff.mp
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ↑(toDualMap 𝕜 E) x = ↑(toDualMap 𝕜 E) y
[PROOFSTEP]
refine' (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (Basis.ext b _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ∀ (i : ι), ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
[PROOFSTEP]
intro i
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
[PROOFSTEP]
simp only [ContinuousLinearMap.coe_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑(↑(toDualMap 𝕜 E) y) (↑b i)
[PROOFSTEP]
rw [toDualMap_apply, toDualMap_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ inner x (↑b i) = inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = inner y (↑b i)
[PROOFSTEP]
conv_rhs => rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
| inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
| inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
| inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = ↑(starRingEnd 𝕜) (inner (↑b i) y)
[PROOFSTEP]
exact congr_arg conj (h i)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
⊢ x = y
[PROOFSTEP]
refine' ext_inner_left_basis b fun i => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
⊢ inner (↑b i) x = inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
⊢ ↑(starRingEnd 𝕜) (inner x (↑b i)) = inner (↑b i) y
[PROOFSTEP]
conv_rhs => rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
| inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
| inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
| inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
⊢ ↑(starRingEnd 𝕜) (inner x (↑b i)) = ↑(starRingEnd 𝕜) (inner y (↑b i))
[PROOFSTEP]
exact congr_arg conj (h i)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ Function.Surjective ↑(toDualMap 𝕜 E)
[PROOFSTEP]
intro ℓ
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
set Y := LinearMap.ker ℓ
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
by_cases htriv : Y = ⊤
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
have hℓ : ℓ = 0 := by
  have h' := LinearMap.ker_eq_top.mp htriv
  rw [← coe_zero] at h' 
  apply coe_injective
  exact h'
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
⊢ ℓ = 0
[PROOFSTEP]
have h' := LinearMap.ker_eq_top.mp htriv
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
h' : ↑ℓ = 0
⊢ ℓ = 0
[PROOFSTEP]
rw [← coe_zero] at h' 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
h'✝ : ↑ℓ = 0
h' : ↑ℓ = ↑0
⊢ ℓ = 0
[PROOFSTEP]
apply coe_injective
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
h'✝ : ↑ℓ = 0
h' : ↑ℓ = ↑0
⊢ ↑ℓ = ↑0
[PROOFSTEP]
exact h'
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
exact ⟨0, by simp [hℓ]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ ↑(toDualMap 𝕜 E) 0 = ℓ
[PROOFSTEP]
simp [hℓ]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : ¬Y = ⊤
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
rw [← Submodule.orthogonal_eq_bot_iff] at htriv 
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : ¬Yᗮ = ⊥
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
change Yᗮ ≠ ⊥ at htriv 
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Yᗮ ≠ ⊥
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
rw [Submodule.ne_bot_iff] at htriv 
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : ∃ x, x ∈ Yᗮ ∧ x ≠ 0
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
refine' ⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, _⟩
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z) = ℓ
[PROOFSTEP]
apply ContinuousLinearMap.ext
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ∀ (x : E), ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
intro x
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
have h₁ : ℓ z • x - ℓ x • z ∈ Y :=
  by
  rw [LinearMap.mem_ker, map_sub, ContinuousLinearMap.map_smul, ContinuousLinearMap.map_smul, Algebra.id.smul_eq_mul,
    Algebra.id.smul_eq_mul, mul_comm]
  exact sub_self (ℓ x * ℓ z)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑ℓ z • x - ↑ℓ x • z ∈ Y
[PROOFSTEP]
rw [LinearMap.mem_ker, map_sub, ContinuousLinearMap.map_smul, ContinuousLinearMap.map_smul, Algebra.id.smul_eq_mul,
  Algebra.id.smul_eq_mul, mul_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑ℓ x * ↑ℓ z - ↑ℓ x * ↑ℓ z = 0
[PROOFSTEP]
exact sub_self (ℓ x * ℓ z)
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
have h₂ : ℓ z * ⟪z, x⟫ = ℓ x * ⟪z, z⟫ :=
  haveI h₃ :=
    calc
      0 = ⟪z, ℓ z • x - ℓ x • z⟫ := by
        rw [(Y.mem_orthogonal' z).mp hz]
        exact h₁
      _ = ⟪z, ℓ z • x⟫ - ⟪z, ℓ x • z⟫ := by rw [inner_sub_right]
      _ = ℓ z * ⟪z, x⟫ - ℓ x * ⟪z, z⟫ := by simp [inner_smul_right]
  sub_eq_zero.mp (Eq.symm h₃)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ 0 = inner z (↑ℓ z • x - ↑ℓ x • z)
[PROOFSTEP]
rw [(Y.mem_orthogonal' z).mp hz]
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ ↑ℓ z • x - ↑ℓ x • z ∈ Y
[PROOFSTEP]
exact h₁
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ inner z (↑ℓ z • x - ↑ℓ x • z) = inner z (↑ℓ z • x) - inner z (↑ℓ x • z)
[PROOFSTEP]
rw [inner_sub_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ inner z (↑ℓ z • x) - inner z (↑ℓ x • z) = ↑ℓ z * inner z x - ↑ℓ x * inner z z
[PROOFSTEP]
simp [inner_smul_right]
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
have h₄ :=
  calc
    ⟪(ℓ z† / ⟪z, z⟫) • z, x⟫ = ℓ z / ⟪z, z⟫ * ⟪z, x⟫ := by simp [inner_smul_left, conj_conj]
    _ = ℓ z * ⟪z, x⟫ / ⟪z, z⟫ := by rw [← div_mul_eq_mul_div]
    _ = ℓ x * ⟪z, z⟫ / ⟪z, z⟫ := by rw [h₂]
    _ = ℓ x := by field_simp [inner_self_ne_zero.2 z_ne_0]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ inner ((↑(starRingEnd ((fun a => 𝕜) z)) (↑ℓ z) / inner z z) • z) x = ↑ℓ z / inner z z * inner z x
[PROOFSTEP]
simp [inner_smul_left, conj_conj]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑ℓ z / inner z z * inner z x = ↑ℓ z * inner z x / inner z z
[PROOFSTEP]
rw [← div_mul_eq_mul_div]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑ℓ z * inner z x / inner z z = ↑ℓ x * inner z z / inner z z
[PROOFSTEP]
rw [h₂]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑ℓ x * inner z z / inner z z = ↑ℓ x
[PROOFSTEP]
field_simp [inner_self_ne_zero.2 z_ne_0]
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
h₄ : inner ((↑(starRingEnd ((fun a => 𝕜) z)) (↑ℓ z) / inner z z) • z) x = ↑ℓ x
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
exact h₄
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ inner (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y) x = ↑y x
[PROOFSTEP]
rw [← toDual_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ↑(↑(toDual 𝕜 E) (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y)) x = ↑y x
[PROOFSTEP]
simp only [LinearIsometryEquiv.apply_symm_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v w : E
⊢ inner (↑B♯ v) w = ↑(↑B v) w
[PROOFSTEP]
simp [continuousLinearMapOfBilin]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ f = ↑B♯ v
[PROOFSTEP]
refine' ext_inner_right 𝕜 _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ ∀ (v_1 : E), inner f v_1 = inner (↑B♯ v) v_1
[PROOFSTEP]
intro w
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = inner (↑B♯ v) w
[PROOFSTEP]
rw [continuousLinearMapOfBilin_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = ↑(↑B v) w
[PROOFSTEP]
exact is_lax_milgram w
