α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = cast (_ : Holor α (ds₁ ++ (ds₂ ++ ds₃)) = Holor α (ds₁ ++ ds₂ ++ ds₃)) (x ⊗ (y ⊗ z)) t
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = assocLeft (x ⊗ (y ⊗ z)) t
rw [assocLeft]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x (HolorIndex.take (HolorIndex.take t)) * y (HolorIndex.drop (HolorIndex.take t)) * z (HolorIndex.drop t) =
    cast (_ : Holor α (ds₁ ++ (ds₂ ++ ds₃)) = Holor α (ds₁ ++ ds₂ ++ ds₃))
      (fun t =>
        x (HolorIndex.take t) * (y (HolorIndex.take (HolorIndex.drop t)) * z (HolorIndex.drop (HolorIndex.drop t))))
      t
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = cast (_ : Holor α (ds₁ ++ (ds₂ ++ ds₃)) = Holor α (ds₁ ++ ds₂ ++ ds₃)) (x ⊗ (y ⊗ z)) t
unfold mul
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x (HolorIndex.take (HolorIndex.assocRight t)) *
      (y (HolorIndex.take (HolorIndex.drop (HolorIndex.assocRight t))) *
        z (HolorIndex.drop (HolorIndex.drop (HolorIndex.assocRight t)))) =
    (fun t =>
        x (HolorIndex.take (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t)) *
          (y
              (HolorIndex.take
                (HolorIndex.drop (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t))) *
            z
              (HolorIndex.drop
                (HolorIndex.drop (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t)))))
      t

case eq
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x (HolorIndex.take (HolorIndex.take t)) * y (HolorIndex.drop (HolorIndex.take t)) * z (HolorIndex.drop t) =
    cast (_ : Holor α (ds₁ ++ (ds₂ ++ ds₃)) = Holor α (ds₁ ++ ds₂ ++ ds₃))
      (fun t =>
        x (HolorIndex.take t) * (y (HolorIndex.take (HolorIndex.drop t)) * z (HolorIndex.drop (HolorIndex.drop t))))
      t
rw [mul_assoc, ←HolorIndex.take_take, ←HolorIndex.drop_take, ←HolorIndex.drop_drop, cast_type]
case eq
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x (HolorIndex.take (HolorIndex.assocRight t)) *
      (y (HolorIndex.take (HolorIndex.drop (HolorIndex.assocRight t))) *
        z (HolorIndex.drop (HolorIndex.drop (HolorIndex.assocRight t)))) =
    (fun t =>
        x (HolorIndex.take (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t)) *
          (y
              (HolorIndex.take
                (HolorIndex.drop (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t))) *
            z
              (HolorIndex.drop
                (HolorIndex.drop (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t)))))
      t

case eq
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
rfl
no goals
case eq
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
rw [append_assoc]