ι₁ : Type u_8
ι₂ : Type u_9
R : Type u_1
R₂ : Type u_2
S : Type u_6
S₂ : Type u_7
M : Type u_3
N : Type u_5
P : Type u_4
Mₗ : Type ?u.19146
Nₗ : Type ?u.19149
Pₗ : Type ?u.19152
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ (Finsupp.sum (↑b₁.repr x) fun i xi =>
      Finsupp.sum (↑b₂.repr y) fun j yj => ↑ρ₁₂ xi • ↑σ₁₂ yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ↑(↑B (↑(Finsupp.total ι₁ M R ↑b₁) (↑b₁.repr x))) (↑(Finsupp.total ι₂ N S ↑b₂) (↑b₂.repr y))
ι₁ : Type u_8
ι₂ : Type u_9
R : Type u_1
R₂ : Type u_2
S : Type u_6
S₂ : Type u_7
M : Type u_3
N : Type u_5
P : Type u_4
Mₗ : Type ?u.19146
Nₗ : Type ?u.19149
Pₗ : Type ?u.19152
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ (Finsupp.sum (↑b₁.repr x) fun i xi =>
      Finsupp.sum (↑b₂.repr y) fun j yj => ↑ρ₁₂ xi • ↑σ₁₂ yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ↑(↑B x) y
conv_rhs => rw [← b₁.total_repr x, ← b₂.total_repr y]
no goals
ι₁ : Type u_8
ι₂ : Type u_9
R : Type u_1
R₂ : Type u_2
S : Type u_6
S₂ : Type u_7
M : Type u_3
N : Type u_5
P : Type u_4
Mₗ : Type ?u.19146
Nₗ : Type ?u.19149
Pₗ : Type ?u.19152
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring S₂
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Mₗ
inst✝⁹ : AddCommMonoid Nₗ
inst✝⁸ : AddCommMonoid Pₗ
inst✝⁷ : Module R M
inst✝⁶ : Module S N
inst✝⁵ : Module R₂ P
inst✝⁴ : Module S₂ P
inst✝³ : Module R Mₗ
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
b₁' : Basis ι₁ R Mₗ
b₂' : Basis ι₂ R Nₗ
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ (Finsupp.sum (↑b₁.repr x) fun i xi =>
      Finsupp.sum (↑b₂.repr y) fun j yj => ↑ρ₁₂ xi • ↑σ₁₂ yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ↑(↑B (↑(Finsupp.total ι₁ M R ↑b₁) (↑b₁.repr x))) (↑(Finsupp.total ι₂ N S ↑b₂) (↑b₂.repr y))
simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smulₛₗ₂,
  LinearMap.map_smulₛₗ]