R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ ∀ (i : ι × κ),
    ↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) i) =
      ↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) i)
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ comp (dualDistrib R M N) (dualDistribInvOfBasis b c) = LinearMap.id
apply (b.tensorProduct c).dualBasis.ext
case mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)) =
    ↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ ∀ (i : ι × κ),
    ↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) i) =
      ↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) i)
rintro ⟨i, j⟩
case mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (i_1 : ι × κ),
    ↑(↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)))
        (↑(Basis.tensorProduct b c) i_1) =
      ↑(↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))) (↑(Basis.tensorProduct b c) i_1)
case mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)) =
    ↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))
apply (b.tensorProduct c).ext
case mk.mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ↑(↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)))
      (↑(Basis.tensorProduct b c) (i', j')) =
    ↑(↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))) (↑(Basis.tensorProduct b c) (i', j'))
case mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (i_1 : ι × κ),
    ↑(↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)))
        (↑(Basis.tensorProduct b c) i_1) =
      ↑(↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))) (↑(Basis.tensorProduct b c) i_1)
rintro ⟨i', j'⟩
case mk.mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∑ x : ι,
      ∑ x_1 : κ,
        ↑(Finsupp.single x 1) i * ↑(Finsupp.single x_1 1) j * (↑(Finsupp.single i' 1) x * ↑(Finsupp.single j' 1) x_1) =
    ↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j
case mk.mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ↑(↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)))
      (↑(Basis.tensorProduct b c) (i', j')) =
    ↑(↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))) (↑(Basis.tensorProduct b c) (i', j'))
simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
  dualDistribInvOfBasis_apply, Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply,
  Basis.repr_self, ne_eq, LinearMap.map_sum, map_smul, homTensorHomMap_apply, compRight_apply,
  Basis.tensorProduct_apply, coeFn_sum, Finset.sum_apply, smul_apply, LinearEquiv.coe_coe,
  map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]
case mk.mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) =
    ↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j

case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0

case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
case mk.mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∑ x : ι,
      ∑ x_1 : κ,
        ↑(Finsupp.single x 1) i * ↑(Finsupp.single x_1 1) j * (↑(Finsupp.single i' 1) x * ↑(Finsupp.single j' 1) x_1) =
    ↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0

case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
case mk.mk
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) =
    ↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j

case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0

case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
simp
no goals
case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0

case mk.mk.h₀
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0

case mk.mk.h₁
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
all_goals { intros; simp [*] at * }