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

State before:
l : List TensorElem
head : ℕ
tail : List ℕ
⊢ inferredShape (nested l) = some (head :: tail) →
    head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true
Tactic:
revert head tail
State after:
l : List TensorElem
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested l) = some (head :: tail) →
      head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true

State before:
l : List TensorElem
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested l) = some (head :: tail) →
      head = List.length l ∧ (List.all l fun x => decide (inferredShape x = some tail)) = true
Tactic:
induction l <;> simp
State after:
case nil

⊢ ∀ {head : ℕ} {tail : List ℕ}, inferredShape (nested []) = some (head :: tail) → head = 0

case cons
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested tail✝) = some (head :: tail) →
      head = List.length tail✝ ∧ (List.all tail✝ fun x => decide (inferredShape x = some tail)) = true
⊢ ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested (head✝ :: tail✝)) = some (head :: tail) →
      head = Nat.succ (List.length tail✝) ∧
        inferredShape head✝ = some tail ∧ ∀ (x : TensorElem), x ∈ tail✝ → inferredShape x = some tail

State before:
⊢ ∀ {head : ℕ} {tail : List ℕ}, inferredShape (nested []) = some (head :: tail) → head = 0
Tactic:
case nil =>
  intros head tile H; simp [inferredShape, List.all_nil] at *; simp [H.1]
State after:
no goals

State before:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
⊢ ∀ {head_1 : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (head :: tail)) = some (head_1 :: tail_1) →
      head_1 = Nat.succ (List.length tail) ∧
        inferredShape head = some tail_1 ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some tail_1
Tactic:
case cons head tail ih =>
  intros s_head s_tail H
  cases tail
  case nil =>
    simp [inferredShape, List.all_one]
    simp [inferredShape, bind, Option.bind, List.all_one] at H
    split at H; trivial; simp at H
    case h_2 _ s_mid H' =>
      simp [←H.1, H', H.2]
  case cons mid tail =>
    let H' := inferredShape_cons_inv H
    specialize (ih H'.2.2)
    constructor
    . have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
        sorry
      simp [helper H'.1 ih.1]
    . sorry
State after:
no goals

State before:
⊢ ∀ {head : ℕ} {tail : List ℕ}, inferredShape (nested []) = some (head :: tail) → head = 0
Tactic:
intros head tile H
State after:
head : ℕ
tile : List ℕ
H : inferredShape (nested []) = some (head :: tile)
⊢ head = 0

State before:
head : ℕ
tile : List ℕ
H : inferredShape (nested []) = some (head :: tile)
⊢ head = 0
Tactic:
simp [inferredShape, List.all_nil] at *
State after:
head : ℕ
tile : List ℕ
H : 0 = head ∧ [] = tile
⊢ head = 0

State before:
head : ℕ
tile : List ℕ
H : 0 = head ∧ [] = tile
⊢ head = 0
Tactic:
simp [H.1]
State after:
no goals

State before:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
⊢ ∀ {head_1 : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (head :: tail)) = some (head_1 :: tail_1) →
      head_1 = Nat.succ (List.length tail) ∧
        inferredShape head = some tail_1 ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some tail_1
Tactic:
intros s_head s_tail H
State after:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested (head :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length tail) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s_tail

State before:
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested (head :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length tail) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s_tail
Tactic:
cases tail
State after:
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail

case cons
head : TensorElem
s_head : ℕ
s_tail : List ℕ
head✝ : TensorElem
tail✝ : List TensorElem
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested (head✝ :: tail✝)) = some (head :: tail) →
      head = List.length (head✝ :: tail✝) ∧
        (List.all (head✝ :: tail✝) fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested (head :: head✝ :: tail✝)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length (head✝ :: tail✝)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ head✝ :: tail✝ → inferredShape x = some s_tail

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail
Tactic:
case nil =>
  simp [inferredShape, List.all_one]
  simp [inferredShape, bind, Option.bind, List.all_one] at H
  split at H; trivial; simp at H
  case h_2 _ s_mid H' =>
    simp [←H.1, H', H.2]
State after:
no goals

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (mid :: tail)) = some (head :: tail_1) →
      head = List.length (mid :: tail) ∧ (List.all (mid :: tail) fun x => decide (inferredShape x = some tail_1)) = true
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
case cons mid tail =>
  let H' := inferredShape_cons_inv H
  specialize (ih H'.2.2)
  constructor
  . have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
      sorry
    simp [helper H'.1 ih.1]
  . sorry
State after:
no goals

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail
Tactic:
simp [inferredShape, List.all_one]
State after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
simp [inferredShape, bind, Option.bind, List.all_one] at H
State after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H :
  (match inferredShape head, fun __do_lift => some (1 :: __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H :
  (match inferredShape head, fun __do_lift => some (1 :: __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
split at H
State after:
case h_1
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
heq✝ : inferredShape head = none
H : none = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

State before:
case h_1
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
heq✝ : inferredShape head = none
H : none = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
trivial
State after:
case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

State before:
case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
simp at H
State after:
case h_2
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : 1 = s_head ∧ a✝ = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
s_mid : List ℕ
H' : inferredShape head = some s_mid
H : 1 = s_head ∧ s_mid = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
case h_2 _ s_mid H' =>
  simp [←H.1, H', H.2]
State after:
no goals

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
s_mid : List ℕ
H' : inferredShape head = some s_mid
H : 1 = s_head ∧ s_mid = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
Tactic:
simp [←H.1, H', H.2]
State after:
no goals

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (mid :: tail)) = some (head :: tail_1) →
      head = List.length (mid :: tail) ∧ (List.all (mid :: tail) fun x => decide (inferredShape x = some tail_1)) = true
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
let H' := inferredShape_cons_inv H
State after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (mid :: tail)) = some (head :: tail_1) →
      head = List.length (mid :: tail) ∧ (List.all (mid :: tail) fun x => decide (inferredShape x = some tail_1)) = true
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (mid :: tail)) = some (head :: tail_1) →
      head = List.length (mid :: tail) ∧ (List.all (mid :: tail) fun x => decide (inferredShape x = some tail_1)) = true
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
specialize (ih H'.2.2)
State after:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
constructor
State after:
case left
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail))

case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail

State before:
case left
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail))

case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
. have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
    sorry
  simp [helper H'.1 ih.1]
State after:
case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail

State before:
case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
Tactic:
. sorry
State after:
no goals

State before:
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ ∀ {n m : ℕ}, n > 0 → n - 1 = m → n = m + 1
Tactic:
sorry
State after:
no goals