𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
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
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
⊢ x = y
refine' ext_inner_left_basis b fun i => _
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
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
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
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
rw [← inner_conj_symm]
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
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))
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
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
conv_rhs => rw [← inner_conj_symm]
no goals
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
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))
exact congr_arg conj (h i)