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

State before:
τ : MLIRTy
l : List TensorElem
h : hasType (nested l) τ = true
⊢ flatten (nested l) h = List.join (mapWithType l flatten h)
Tactic:
revert h
State after:
τ : MLIRTy
l : List TensorElem
⊢ ∀ (h : hasType (nested l) τ = true), flatten (nested l) h = List.join (mapWithType l flatten h)

State before:
τ : MLIRTy
l : List TensorElem
⊢ ∀ (h : hasType (nested l) τ = true), flatten (nested l) h = List.join (mapWithType l flatten h)
Tactic:
induction l <;> intros h
State after:
case nil
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)

State before:
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)
Tactic:
case nil =>
  simp [flatten, mapWithType, List.join]
State after:
no goals

State before:
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
ih : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)
Tactic:
case cons _ _ ih =>
  simp [flatten, mapWithType, List.join, ih]
State after:
no goals

State before:
τ : MLIRTy
h : hasType (nested []) τ = true
⊢ flatten (nested []) h = List.join (mapWithType [] flatten h)
Tactic:
simp [flatten, mapWithType, List.join]
State after:
no goals

State before:
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
ih : ∀ (h : hasType (nested tail✝) τ = true), flatten (nested tail✝) h = List.join (mapWithType tail✝ flatten h)
h : hasType (nested (head✝ :: tail✝)) τ = true
⊢ flatten (nested (head✝ :: tail✝)) h = List.join (mapWithType (head✝ :: tail✝) flatten h)
Tactic:
simp [flatten, mapWithType, List.join, ih]
State after:
no goals