-- Mathlib/Analysis/InnerProductSpace/Dual.lean
theorem ext_inner_left_basis {ι : Type*} {x y : E} (b : Basis ι 𝕜 E)
    (h : ∀ i : ι, ⟪b i, x⟫ = ⟪b i, y⟫) : x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
⊢ ∀ (i : ι), ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)

Tactic:
intro i

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜

Tactic:
rw [← inner_conj_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪b i, x⟫_𝕜 = ⟪y, b i⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
⊢ x = y

Tactic:
apply (toDualMap 𝕜 E).map_eq_iff.mp

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
⊢ (toDualMap 𝕜 E) x = (toDualMap 𝕜 E) y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
⊢ (toDualMap 𝕜 E) x = (toDualMap 𝕜 E) y

Tactic:
refine (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (Basis.ext b ?_)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
⊢ ∀ (i : ι), ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ ((toDualMap 𝕜 E) x) (b i) = ((toDualMap 𝕜 E) y) (b i)

Tactic:
rw [toDualMap_apply, toDualMap_apply]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ ↑((toDualMap 𝕜 E) x) (b i) = ↑((toDualMap 𝕜 E) y) (b i)

Tactic:
simp only [ContinuousLinearMap.coe_coe]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ ((toDualMap 𝕜 E) x) (b i) = ((toDualMap 𝕜 E) y) (b i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪b i, x⟫_𝕜 = ⟪y, b i⟫_𝕜

Tactic:
conv_rhs => rw [← inner_conj_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪b i, x⟫_𝕜 = (starRingEnd 𝕜) ⟪b i, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪b i, x⟫_𝕜 = (starRingEnd 𝕜) ⟪b i, y⟫_𝕜

Tactic:
exact congr_arg conj (h i)

Result:
no goals