apply @TensorElem.recOn
  (motive_1 := fun e =>
    ∀s, e.hasShape s → (h: e.hasType τ) → (e.flatten h).length = shapeProd s)
  (motive_2 := fun l =>
    ∀s, l.all (TensorElem.hasShape . s) → (h: l.all (hasType . τ)) →
      (mapWithType l flatten (hasType_list_2 h)).join.length = l.length * shapeProd s)
  <;> simp <;> clear e
τ : MLIRTy
e : TensorElem
⊢ ∀ (shape : List ℕ), hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
case int
τ : MLIRTy
⊢ ∀ (a : ℤ) (s : List ℕ),
    hasShape (int a) s = true → ∀ (h : hasType (int a) τ = true), List.length (flatten (int a) h) = shapeProd s

case float
τ : MLIRTy
⊢ ∀ (a : Float) (s : List ℕ),
    hasShape (float a) s = true → ∀ (h : hasType (float a) τ = true), List.length (flatten (float a) h) = shapeProd s

case bool
τ : MLIRTy
⊢ (∀ (s : List ℕ),
      hasShape (bool false) s = true →
        ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s) ∧
    ∀ (s : List ℕ),
      hasShape (bool true) s = true →
        ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s

case nested
τ : MLIRTy
⊢ ∀ (a : List TensorElem),
    (∀ (s : List ℕ),
        (∀ (x : TensorElem), x ∈ a → hasShape x s = true) →
          ∀ (h : (List.all a fun x => hasType x τ) = true),
            List.length (List.join (mapWithType a flatten (_ : hasType (nested a) τ = true))) =
              List.length a * shapeProd s) →
      ∀ (s : List ℕ),
        hasShape (nested a) s = true →
          ∀ (h : hasType (nested a) τ = true), List.length (flatten (nested a) h) = shapeProd s

case empty
τ : MLIRTy
⊢ ∀ (s : List ℕ), hasShape empty s = true → ∀ (h : hasType empty τ = true), List.length (flatten empty h) = shapeProd s

case cons
τ : MLIRTy
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ),
        hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s) →
      (∀ (s : List ℕ),
          (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
            ∀ (h : (List.all tail fun x => hasType x τ) = true),
              List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                List.length tail * shapeProd s) →
        ∀ (s : List ℕ),
          hasShape head s = true →
            (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
              ∀ (h : (List.all (head :: tail) fun x => hasType x τ) = true),
                List.length (flatten head (_ : hasType head τ = true)) +
                    List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                  Nat.succ (List.length tail) * shapeProd s