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

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

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

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

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

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

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

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

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

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

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

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