no goals
R : Type ?u.1768534
M : Type ?u.1768537
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.1768573
M₁ : Type ?u.1768576
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type ?u.1769185
M₂ : Type ?u.1769188
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.1769375
M₃ : Type ?u.1769378
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.1771183
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
i j : ι
⊢ bilin B (↑(dualBasis B hB b) i) (↑b j) = if j = i then 1 else 0
rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
  LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]