ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.440725
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.440734
R₂ : Type ?u.440737
s : ι → Type ?u.440742
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_5
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.441195
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
⊢ LinearMap.compMultilinearMap (LinearMap.comp (↑lift φ) ↑(reindex R M e)) (tprod R) =
    LinearMap.compMultilinearMap (↑lift (domDomCongr e.symm φ)) (tprod R)
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.440725
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.440734
R₂ : Type ?u.440737
s : ι → Type ?u.440742
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_5
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.441195
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
⊢ LinearMap.comp (↑lift φ) ↑(reindex R M e) = ↑lift (domDomCongr e.symm φ)
refine ext ?_
case H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.440725
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.440734
R₂ : Type ?u.440737
s : ι → Type ?u.440742
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_5
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.441195
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
x✝ : ι → M
⊢ ↑(LinearMap.compMultilinearMap (LinearMap.comp (↑lift φ) ↑(reindex R M e)) (tprod R)) x✝ =
    ↑(LinearMap.compMultilinearMap (↑lift (domDomCongr e.symm φ)) (tprod R)) x✝
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.440725
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.440734
R₂ : Type ?u.440737
s : ι → Type ?u.440742
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_5
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.441195
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
⊢ LinearMap.compMultilinearMap (LinearMap.comp (↑lift φ) ↑(reindex R M e)) (tprod R) =
    LinearMap.compMultilinearMap (↑lift (domDomCongr e.symm φ)) (tprod R)
ext
no goals
case H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type ?u.440725
R : Type u_3
inst✝⁷ : CommSemiring R
R₁ : Type ?u.440734
R₂ : Type ?u.440737
s : ι → Type ?u.440742
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_5
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.441195
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
x✝ : ι → M
⊢ ↑(LinearMap.compMultilinearMap (LinearMap.comp (↑lift φ) ↑(reindex R M e)) (tprod R)) x✝ =
    ↑(LinearMap.compMultilinearMap (↑lift (domDomCongr e.symm φ)) (tprod R)) x✝
simp