no goals
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
f : Dual R (M ⊗[R] N)
⊢ ↑(dualDistribInvOfBasis b c) f =
    ∑ i : ι, ∑ j : κ, ↑f (↑b i ⊗ₜ[R] ↑c j) • ↑(Basis.dualBasis b) i ⊗ₜ[R] ↑(Basis.dualBasis c) j
simp [dualDistribInvOfBasis]