[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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
[PROOFSTEP]
conv_rhs => rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁.total_repr x, ← b₂.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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))
[PROOFSTEP]
simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smulₛₗ₂, LinearMap.map_smulₛₗ]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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ₗ →ₗ[R] Nₗ →ₗ[R] 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
[PROOFSTEP]
conv_rhs => rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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ₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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ₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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ₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x : Mₗ
y : Nₗ
| ↑(↑B x) y
[PROOFSTEP]
rw [← b₁'.total_repr x, ← b₂'.total_repr y]
[GOAL]
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Mₗ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
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ₗ →ₗ[R] Nₗ →ₗ[R] 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ₗ R ↑b₂') (↑b₂'.repr y))
[PROOFSTEP]
simp_rw [Finsupp.total_apply, Finsupp.sum, map_sum₂, map_sum, LinearMap.map_smul₂, LinearMap.map_smul]
