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
f : Dual R M
p : P
⊢ prodMap (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) 0 =
    ↑(dualTensorHom R (M × N) (P × Q)) (comp f (fst R M N) ⊗ₜ[R] ↑(inl R P Q) p)
ext <;>
  simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
    fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]