case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ↑(toMatrix₂ b₁' b₂') (compl₁₂ B l r) i j = ((↑(toMatrix b₁' b₁) l)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂' b₂) r) i j
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
⊢ ↑(toMatrix₂ b₁' b₂') (compl₁₂ B l r) = (↑(toMatrix b₁' b₁) l)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂' b₂) r
ext (i j)
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ↑(↑B (↑l (↑b₁' i))) (↑r (↑b₂' j)) =
    ∑ x : m, ∑ x_1 : n, ↑(↑b₁.repr (↑l (↑b₁' i))) x_1 * ↑(↑B (↑b₁ x_1)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ↑(toMatrix₂ b₁' b₂') (compl₁₂ B l r) i j = ((↑(toMatrix b₁' b₁) l)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂' b₂) r) i j
simp only [LinearMap.toMatrix₂_apply, compl₁₂_apply, transpose_apply, Matrix.mul_apply,
  LinearMap.toMatrix_apply, LinearEquiv.coe_mk, sum_mul]
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ↑(↑B (↑l (↑b₁' i))) (↑r (↑b₂' j)) =
    ∑ y : n, ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) y * ↑(↑B (↑b₁ y)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ↑(↑B (↑l (↑b₁' i))) (↑r (↑b₂' j)) =
    ∑ x : m, ∑ x_1 : n, ↑(↑b₁.repr (↑l (↑b₁' i))) x_1 * ↑(↑B (↑b₁ x_1)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
rw [sum_comm]
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (Finsupp.sum (↑b₁.repr (↑l (↑b₁' i))) fun i xi =>
      Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => xi • yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ∑ y : n, ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) y * ↑(↑B (↑b₁ y)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ↑(↑B (↑l (↑b₁' i))) (↑r (↑b₂' j)) =
    ∑ y : n, ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) y * ↑(↑B (↑b₁ y)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul b₁ b₂]
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (∑ i_1 : n,
      Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => ↑(↑b₁.repr (↑l (↑b₁' i))) i_1 • yj • ↑(↑B (↑b₁ i_1)) (↑b₂ j)) =
    ∑ y : n, ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) y * ↑(↑B (↑b₁ y)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x

case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ∀ (i : n), (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => 0 • yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) = 0
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (Finsupp.sum (↑b₁.repr (↑l (↑b₁' i))) fun i xi =>
      Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => xi • yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) =
    ∑ y : n, ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) y * ↑(↑B (↑b₁ y)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
rw [Finsupp.sum_fintype]
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ∀ (x : n),
    x ∈ univ →
      (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => ↑(↑b₁.repr (↑l (↑b₁' i))) x • yj • ↑(↑B (↑b₁ x)) (↑b₂ j)) =
        ∑ x_1 : m, ↑(↑b₁.repr (↑l (↑b₁' i))) x * ↑(↑B (↑b₁ x)) (↑b₂ x_1) * ↑(↑b₂.repr (↑r (↑b₂' j))) x_1
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (∑ i_1 : n,
      Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => ↑(↑b₁.repr (↑l (↑b₁' i))) i_1 • yj • ↑(↑B (↑b₁ i_1)) (↑b₂ j)) =
    ∑ y : n, ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) y * ↑(↑B (↑b₁ y)) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
apply sum_congr rfl
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => ↑(↑b₁.repr (↑l (↑b₁' i))) i' • yj • ↑(↑B (↑b₁ i')) (↑b₂ j)) =
    ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ∀ (x : n),
    x ∈ univ →
      (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => ↑(↑b₁.repr (↑l (↑b₁' i))) x • yj • ↑(↑B (↑b₁ x)) (↑b₂ j)) =
        ∑ x_1 : m, ↑(↑b₁.repr (↑l (↑b₁' i))) x * ↑(↑B (↑b₁ x)) (↑b₂ x_1) * ↑(↑b₂.repr (↑r (↑b₂' j))) x_1
rintro i' -
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∑ i_1 : m, ↑(↑b₁.repr (↑l (↑b₁' i))) i' • ↑(↑b₂.repr (↑r (↑b₂' j))) i_1 • ↑(↑B (↑b₁ i')) (↑b₂ i_1) =
    ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x

case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m), ↑(↑b₁.repr (↑l (↑b₁' i))) i' • 0 • ↑(↑B (↑b₁ i')) (↑b₂ i_1) = 0
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => ↑(↑b₁.repr (↑l (↑b₁' i))) i' • yj • ↑(↑B (↑b₁ i')) (↑b₂ j)) =
    ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
rw [Finsupp.sum_fintype]
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (x : m),
    x ∈ univ →
      ↑(↑b₁.repr (↑l (↑b₁' i))) i' • ↑(↑b₂.repr (↑r (↑b₂' j))) x • ↑(↑B (↑b₁ i')) (↑b₂ x) =
        ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∑ i_1 : m, ↑(↑b₁.repr (↑l (↑b₁' i))) i' • ↑(↑b₂.repr (↑r (↑b₂' j))) i_1 • ↑(↑B (↑b₁ i')) (↑b₂ i_1) =
    ∑ x : m, ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
apply sum_congr rfl
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
j' : m
⊢ ↑(↑b₁.repr (↑l (↑b₁' i))) i' • ↑(↑b₂.repr (↑r (↑b₂' j))) j' • ↑(↑B (↑b₁ i')) (↑b₂ j') =
    ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ j') * ↑(↑b₂.repr (↑r (↑b₂' j))) j'
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (x : m),
    x ∈ univ →
      ↑(↑b₁.repr (↑l (↑b₁' i))) i' • ↑(↑b₂.repr (↑r (↑b₂' j))) x • ↑(↑B (↑b₁ i')) (↑b₂ x) =
        ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ x) * ↑(↑b₂.repr (↑r (↑b₂' j))) x
rintro j' -
no goals
case a.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
j' : m
⊢ ↑(↑b₁.repr (↑l (↑b₁' i))) i' • ↑(↑b₂.repr (↑r (↑b₂' j))) j' • ↑(↑B (↑b₁ i')) (↑b₂ j') =
    ↑(↑b₁.repr (↑l (↑b₁' i))) i' * ↑(↑B (↑b₁ i')) (↑b₂ j') * ↑(↑b₂.repr (↑r (↑b₂' j))) j'
simp only [smul_eq_mul, LinearMap.toMatrix_apply, Basis.equivFun_apply, mul_assoc, mul_comm,
  mul_left_comm]
case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
i✝ : m
⊢ ↑(↑b₁.repr (↑l (↑b₁' i))) i' • 0 • ↑(↑B (↑b₁ i')) (↑b₂ i✝) = 0
case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m), ↑(↑b₁.repr (↑l (↑b₁' i))) i' • 0 • ↑(↑B (↑b₁ i')) (↑b₂ i_1) = 0
intros
no goals
case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
i✝ : m
⊢ ↑(↑b₁.repr (↑l (↑b₁' i))) i' • 0 • ↑(↑B (↑b₁ i')) (↑b₂ i✝) = 0
simp only [zero_smul, smul_zero]
case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i✝ : n
⊢ (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => 0 • yj • ↑(↑B (↑b₁ i✝)) (↑b₂ j)) = 0
case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ∀ (i : n), (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => 0 • yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) = 0
intros
no goals
case a.h.h
R : Type u_1
R₁ : Type ?u.1503183
R₂ : Type ?u.1503186
M : Type ?u.1503189
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type u_5
n : Type u_9
m : Type u_8
n' : Type u_6
m' : Type u_7
ι : Type ?u.1503216
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i✝ : n
⊢ (Finsupp.sum (↑b₂.repr (↑r (↑b₂' j))) fun j yj => 0 • yj • ↑(↑B (↑b₁ i✝)) (↑b₂ j)) = 0
simp only [zero_smul, Finsupp.sum_zero]