no goals
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
g : Dual R N
q : Q
⊢ prodMap 0 (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    ↑(dualTensorHom R (M × N) (P × Q)) (comp g (snd R M N) ⊗ₜ[R] ↑(inr R P Q) q)
ext <;>
  simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
    snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]