case H.h.h
ι : 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
g : Dual R N
q : Q
m : M
n : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R M N)
              (TensorProduct.map (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))))
          m)
      n =
    ↑(↑(compr₂ (TensorProduct.mk R M N)
              (↑(dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) (↑(dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)))
          m)
      n
ι : 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
g : Dual R N
q : Q
⊢ TensorProduct.map (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    ↑(dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) (↑(dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)
ext (m n)
no goals
case H.h.h
ι : 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
g : Dual R N
q : Q
m : M
n : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R M N)
              (TensorProduct.map (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))))
          m)
      n =
    ↑(↑(compr₂ (TensorProduct.mk R M N)
              (↑(dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) (↑(dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)))
          m)
      n
simp only [compr₂_apply, mk_apply, map_tmul, dualTensorHom_apply, dualDistrib_apply, ←
  smul_tmul_smul]