no goals
R : Type ?u.1740676
M : Type ?u.1740679
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.1740715
M₁ : Type ?u.1740718
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type ?u.1741327
M₂ : Type ?u.1741330
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.1741517
M₃ : Type ?u.1741520
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1743325
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : Module R₂ M₂'
inst✝² : FiniteDimensional K V
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
B : BilinForm K V
hB : Nondegenerate B
b : Basis ι K V
x : V
i : ι
⊢ ↑(↑(dualBasis B hB b).repr x) i = bilin B x (↑b i)
rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
  Basis.dualBasis_repr, toDual_def]