R : Type ?u.810929
M : Type ?u.810932
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.810968
M₁ : Type ?u.810971
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_3
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.811770
M₃ : Type ?u.811773
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.812361
K : Type ?u.812364
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.813578
M₂'' : Type ?u.813581
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
F₂ : BilinForm R₂ M₂
ι : Type u_2
b : Basis ι R₂ M₂
x y : M₂
⊢ (Finsupp.sum (↑b.repr x) fun i xi => Finsupp.sum (↑b.repr y) fun j yj => xi • yj • bilin B₂ (↑b i) (↑b j)) =
    bilin B₂ (↑(Finsupp.total ι M₂ R₂ ↑b) (↑b.repr x)) (↑(Finsupp.total ι M₂ R₂ ↑b) (↑b.repr y))
R : Type ?u.810929
M : Type ?u.810932
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.810968
M₁ : Type ?u.810971
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_3
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.811770
M₃ : Type ?u.811773
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.812361
K : Type ?u.812364
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.813578
M₂'' : Type ?u.813581
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
F₂ : BilinForm R₂ M₂
ι : Type u_2
b : Basis ι R₂ M₂
x y : M₂
⊢ (Finsupp.sum (↑b.repr x) fun i xi => Finsupp.sum (↑b.repr y) fun j yj => xi • yj • bilin B₂ (↑b i) (↑b j)) =
    bilin B₂ x y
conv_rhs => rw [← b.total_repr x, ← b.total_repr y]
no goals
R : Type ?u.810929
M : Type ?u.810932
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.810968
M₁ : Type ?u.810971
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_3
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.811770
M₃ : Type ?u.811773
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.812361
K : Type ?u.812364
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.813578
M₂'' : Type ?u.813581
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
F₂ : BilinForm R₂ M₂
ι : Type u_2
b : Basis ι R₂ M₂
x y : M₂
⊢ (Finsupp.sum (↑b.repr x) fun i xi => Finsupp.sum (↑b.repr y) fun j yj => xi • yj • bilin B₂ (↑b i) (↑b j)) =
    bilin B₂ (↑(Finsupp.total ι M₂ R₂ ↑b) (↑b.repr x)) (↑(Finsupp.total ι M₂ R₂ ↑b) (↑b.repr y))
simp_rw [Finsupp.total_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right,
  smul_eq_mul]