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

State before:
l : List TensorElem
τ : MLIRTy
⊢ hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
Tactic:
induction l
State after:
case nil
τ : MLIRTy
⊢ hasType (nested []) τ = true → (List.all [] fun x => hasType x τ) = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : hasType (nested tail✝) τ = true → (List.all tail✝ fun x => hasType x τ) = true
⊢ hasType (nested (head✝ :: tail✝)) τ = true → (List.all (head✝ :: tail✝) fun x => hasType x τ) = true

State before:
case nil
τ : MLIRTy
⊢ hasType (nested []) τ = true → (List.all [] fun x => hasType x τ) = true

case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : hasType (nested tail✝) τ = true → (List.all tail✝ fun x => hasType x τ) = true
⊢ hasType (nested (head✝ :: tail✝)) τ = true → (List.all (head✝ :: tail✝) fun x => hasType x τ) = true
Tactic:
simp
State after:
case cons
τ : MLIRTy
head✝ : TensorElem
tail✝ : List TensorElem
tail_ih✝ : hasType (nested tail✝) τ = true → (List.all tail✝ fun x => hasType x τ) = true
⊢ hasType (nested (head✝ :: tail✝)) τ = true → (List.all (head✝ :: tail✝) fun x => hasType x τ) = true

State before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType (nested (e :: l)) τ = true → (List.all (e :: l) fun x => hasType x τ) = true
Tactic:
case cons e l ih' =>
  simp [hasType, List.all_cons]
  intro h' h
  constructor <;> simp
  assumption
  simp[h, h']
  sorry
State after:
no goals

State before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType (nested (e :: l)) τ = true → (List.all (e :: l) fun x => hasType x τ) = true
Tactic:
simp [hasType, List.all_cons]
State after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType e τ = true → hasType (nested l) τ = true → hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true

State before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
⊢ hasType e τ = true → hasType (nested l) τ = true → hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
intro h' h
State after:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true

State before:
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true ∧ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
constructor <;> simp
State after:
case left
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true

case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true

State before:
case left
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ hasType e τ = true

case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
assumption
State after:
case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true

State before:
case right
τ : MLIRTy
e : TensorElem
l : List TensorElem
ih' : hasType (nested l) τ = true → (List.all l fun x => hasType x τ) = true
h' : hasType e τ = true
h : hasType (nested l) τ = true
⊢ ∀ (x : TensorElem), x ∈ l → hasType x τ = true
Tactic:
sorry
State after:
no goals