Theorem: MLIR.AST.TensorElem.flatten_size (MLIR/Semantics/TensorElem.lean)

State before:
τ : MLIRTy
e : TensorElem
shape : List ℕ
⊢ hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
Tactic:
revert shape
State after:
τ : MLIRTy
e : TensorElem
⊢ ∀ (shape : List ℕ), hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape

State before:
τ : MLIRTy
e : TensorElem
⊢ ∀ (shape : List ℕ), hasShape e shape = true → ∀ (h : hasType e τ = true), List.length (flatten e h) = shapeProd shape
Tactic:
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
State after:
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

State before:
τ : MLIRTy
⊢ ∀ (a : ℤ) (s : List ℕ),
    hasShape (int a) s = true → ∀ (h : hasType (int a) τ = true), List.length (flatten (int a) h) = shapeProd s
Tactic:
case int =>
  intros i s Hshape Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
State after:
no goals

State before:
τ : MLIRTy
⊢ ∀ (a : Float) (s : List ℕ),
    hasShape (float a) s = true → ∀ (h : hasType (float a) τ = true), List.length (flatten (float a) h) = shapeProd s
Tactic:
case float =>
  intros i s Hshape Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
State after:
no goals

State before:
τ : 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
Tactic:
case bool =>
  constructor;
  intros s;
  intros Hshape;
  intros Htype;
  cases τ <;> simp [hasType] at Htype
  cases s <;> simp [flatten, hasShape] at *
  sorry
State after:
no goals

State before:
τ : 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
Tactic:
case nested =>
  intros l motive_2 s Hshape Htype
  cases s <;> simp [hasShape] at Hshape
  case cons s_head s_tail =>
  simp [TensorElem.flatten_list, shapeProd, List.foldr]
  simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
  simp [shapeProd, Nat.mul_comm, Hshape.1]
State after:
no goals

State before:
τ : MLIRTy
⊢ ∀ (s : List ℕ), hasShape empty s = true → ∀ (h : hasType empty τ = true), List.length (flatten empty h) = shapeProd s
Tactic:
case empty =>
  intros s Hshape Htype
  simp [hasType] at Htype
State after:
no goals

State before:
τ : 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
Tactic:
case cons =>
  intros head tail motive_1 IH2 s Hshape1 Hshape2 Htype1
  simp [List.map, List.join]
  rw [Nat.add_comm]
  simp [Nat.succ_eq_add_one, Nat.right_distrib]
  simp [List.all_cons] at Hshape1
  simp [List.all_cons] at Htype1
  sorry
State after:
no goals

State before:
τ : MLIRTy
⊢ ∀ (a : ℤ) (s : List ℕ),
    hasShape (int a) s = true → ∀ (h : hasType (int a) τ = true), List.length (flatten (int a) h) = shapeProd s
Tactic:
intros i s Hshape Htype
State after:
τ : MLIRTy
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
Htype : hasType (int i) τ = true
⊢ List.length (flatten (int i) Htype) = shapeProd s

State before:
τ : MLIRTy
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
Htype : hasType (int i) τ = true
⊢ List.length (flatten (int i) Htype) = shapeProd s
Tactic:
cases τ <;> simp [hasType] at Htype
State after:
case int
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype✝ : hasType (int i) (MLIRType.int a✝¹ a✝) = true
Htype : FinInt.isInBounds a✝¹ a✝ i = true
⊢ List.length (flatten (int i) Htype✝) = shapeProd s

State before:
case int
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype✝ : hasType (int i) (MLIRType.int a✝¹ a✝) = true
Htype : FinInt.isInBounds a✝¹ a✝ i = true
⊢ List.length (flatten (int i) Htype✝) = shapeProd s
Tactic:
cases s <;> simp [flatten, hasShape] at *
State after:
no goals

State before:
τ : MLIRTy
⊢ ∀ (a : Float) (s : List ℕ),
    hasShape (float a) s = true → ∀ (h : hasType (float a) τ = true), List.length (flatten (float a) h) = shapeProd s
Tactic:
intros i s Hshape Htype
State after:
τ : MLIRTy
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
Htype : hasType (float i) τ = true
⊢ List.length (flatten (float i) Htype) = shapeProd s

State before:
τ : MLIRTy
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
Htype : hasType (float i) τ = true
⊢ List.length (flatten (float i) Htype) = shapeProd s
Tactic:
cases τ <;> simp [hasType] at Htype
State after:
case float
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
a✝ : ℕ
Htype✝ : hasType (float i) (MLIRType.float a✝) = true
Htype : True
⊢ List.length (flatten (float i) Htype✝) = shapeProd s

State before:
case float
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
a✝ : ℕ
Htype✝ : hasType (float i) (MLIRType.float a✝) = true
Htype : True
⊢ List.length (flatten (float i) Htype✝) = shapeProd s
Tactic:
cases s <;> simp [flatten, hasShape] at *
State after:
no goals

State before:
τ : 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
Tactic:
constructor
State after:
case left
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool false) s = true →
      ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

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

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

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
intros s
State after:
case left
τ : MLIRTy
s : List ℕ
⊢ hasShape (bool false) s = true →
    ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

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

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

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
intros Hshape
State after:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
⊢ ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

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

State before:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
⊢ ∀ (h : hasType (bool false) τ = true), List.length (flatten (bool false) h) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
intros Htype
State after:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
Htype : hasType (bool false) τ = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

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

State before:
case left
τ : MLIRTy
s : List ℕ
Hshape : hasShape (bool false) s = true
Htype : hasType (bool false) τ = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
cases τ <;> simp [hasType] at Htype
State after:
case left.int
s : List ℕ
Hshape : hasShape (bool false) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype : hasType (bool false) (MLIRType.int a✝¹ a✝) = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

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

State before:
case left.int
s : List ℕ
Hshape : hasShape (bool false) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype : hasType (bool false) (MLIRType.int a✝¹ a✝) = true
⊢ List.length (flatten (bool false) Htype) = shapeProd s

case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
cases s <;> simp [flatten, hasShape] at *
State after:
case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s

State before:
case right
τ : MLIRTy
⊢ ∀ (s : List ℕ),
    hasShape (bool true) s = true →
      ∀ (h : hasType (bool true) τ = true), List.length (flatten (bool true) h) = shapeProd s
Tactic:
sorry
State after:
no goals

State before:
τ : 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
Tactic:
intros l motive_2 s Hshape Htype
State after:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
s : List ℕ
Hshape : hasShape (nested l) s = true
Htype : hasType (nested l) τ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd s

State before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
s : List ℕ
Hshape : hasShape (nested l) s = true
Htype : hasType (nested l) τ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd s
Tactic:
cases s <;> simp [hasShape] at Hshape
State after:
case cons
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
head✝ : ℕ
tail✝ : List ℕ
Hshape : List.length l = head✝ ∧ ∀ (x : TensorElem), x ∈ l → hasShape x tail✝ = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (head✝ :: tail✝)

State before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (s_head :: s_tail)
Tactic:
case cons s_head s_tail =>
simp [TensorElem.flatten_list, shapeProd, List.foldr]
simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
simp [shapeProd, Nat.mul_comm, Hshape.1]
State after:
no goals

State before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (s_head :: s_tail)
Tactic:
simp [TensorElem.flatten_list, shapeProd, List.foldr]
State after:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (List.join (mapWithType l flatten Htype)) = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail

State before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (List.join (mapWithType l flatten Htype)) = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail
Tactic:
simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
State after:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length l * shapeProd s_tail = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail

State before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length l * shapeProd s_tail = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail
Tactic:
simp [shapeProd, Nat.mul_comm, Hshape.1]
State after:
no goals

State before:
τ : MLIRTy
⊢ ∀ (s : List ℕ), hasShape empty s = true → ∀ (h : hasType empty τ = true), List.length (flatten empty h) = shapeProd s
Tactic:
intros s Hshape Htype
State after:
τ : MLIRTy
s : List ℕ
Hshape : hasShape empty s = true
Htype : hasType empty τ = true
⊢ List.length (flatten empty Htype) = shapeProd s

State before:
τ : MLIRTy
s : List ℕ
Hshape : hasShape empty s = true
Htype : hasType empty τ = true
⊢ List.length (flatten empty Htype) = shapeProd s
Tactic:
simp [hasType] at Htype
State after:
no goals

State before:
τ : 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
Tactic:
intros head tail motive_1 IH2 s Hshape1 Hshape2 Htype1
State after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (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

State before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (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
Tactic:
rw [Nat.add_comm]
State after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    Nat.succ (List.length tail) * shapeProd s

State before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    Nat.succ (List.length tail) * shapeProd s
Tactic:
simp [Nat.succ_eq_add_one, Nat.right_distrib]
State after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s

State before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s
Tactic:
simp [List.all_cons] at Htype1
State after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1✝ : (List.all (head :: tail) fun x => hasType x τ) = true
Htype1 : hasType head τ = true ∧ ∀ (x : TensorElem), x ∈ tail → hasType x τ = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s

State before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (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 ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1✝ : (List.all (head :: tail) fun x => hasType x τ) = true
Htype1 : hasType head τ = true ∧ ∀ (x : TensorElem), x ∈ tail → hasType x τ = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s
Tactic:
sorry
State after:
no goals