no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Monoid α
x : Holor α []
y : Holor α ds
⊢ x ⊗ y = x { val := [], property := (_ : Forall₂ (fun x x_1 => x < x_1) [] []) } • y
simp [mul, SMul.smul, HolorIndex.take, HolorIndex.drop, HSMul.hSMul]