R : Type ?u.43148
M : Type ?u.43151
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.43187
M₁ : Type ?u.43190
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_2
M₂ : Type ?u.43802
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.43989
M₃ : Type ?u.43992
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.44580
K : Type ?u.44583
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂✝ : BilinForm R₂ M₂
n : Type u_1
o : Type ?u.45800
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
B₂ : BilinForm R₂ (n → R₂)
i j : n
⊢ bilin (toBilin'Aux (↑(toMatrixAux fun j => ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) B₂)) (↑(Pi.basisFun R₂ n) i)
      (↑(Pi.basisFun R₂ n) j) =
    bilin B₂ (↑(Pi.basisFun R₂ n) i) (↑(Pi.basisFun R₂ n) j)
R : Type ?u.43148
M : Type ?u.43151
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.43187
M₁ : Type ?u.43190
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_2
M₂ : Type ?u.43802
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.43989
M₃ : Type ?u.43992
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.44580
K : Type ?u.44583
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂✝ : BilinForm R₂ M₂
n : Type u_1
o : Type ?u.45800
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
B₂ : BilinForm R₂ (n → R₂)
⊢ toBilin'Aux (↑(toMatrixAux fun j => ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) B₂) = B₂
refine' ext_basis (Pi.basisFun R₂ n) fun i j => _
no goals
R : Type ?u.43148
M : Type ?u.43151
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.43187
M₁ : Type ?u.43190
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type u_2
M₂ : Type ?u.43802
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.43989
M₃ : Type ?u.43992
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.44580
K : Type ?u.44583
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂✝ : BilinForm R₂ M₂
n : Type u_1
o : Type ?u.45800
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : DecidableEq n
B₂ : BilinForm R₂ (n → R₂)
i j : n
⊢ bilin (toBilin'Aux (↑(toMatrixAux fun j => ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) B₂)) (↑(Pi.basisFun R₂ n) i)
      (↑(Pi.basisFun R₂ n) j) =
    bilin B₂ (↑(Pi.basisFun R₂ n) i) (↑(Pi.basisFun R₂ n) j)
rw [Pi.basisFun_apply, Pi.basisFun_apply, Matrix.toBilin'Aux_stdBasis,
  BilinForm.toMatrixAux_apply]