ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.627942
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.627951
R₂ : Type ?u.627954
s : ι → Type ?u.627959
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.628278
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.628412
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
a : ι → M
b : ι₂ → M
⊢ (↑(↑(↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R)) fun i => a i) fun i => b i) =
    ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.elim a b i
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.627942
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.627951
R₂ : Type ?u.627954
s : ι → Type ?u.627959
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.628278
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.628412
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
a : ι → M
b : ι₂ → M
⊢ ↑PiTensorProduct.tmul ((⨂ₜ[R] (i : ι), a i) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), b i) = ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.elim a b i
erw [TensorProduct.lift.tmul, PiTensorProduct.lift.tprod, PiTensorProduct.lift.tprod]
no goals
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.627942
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.627951
R₂ : Type ?u.627954
s : ι → Type ?u.627959
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.628278
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.628412
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
a : ι → M
b : ι₂ → M
⊢ (↑(↑(↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R)) fun i => a i) fun i => b i) =
    ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.elim a b i
rfl