Theorem: DimList.dim_known_project_refines (MLIR/Semantics/TensorElem.lean)

State before:
D : DimList
⊢ known D = true → shapeRefines (project D) D = true
Tactic:
intros h <;> induction D <;> simp
State after:
case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → shapeRefines (project tail✝) tail✝ = true
h : known (head✝ :: tail✝) = true
⊢ shapeRefines (project (head✝ :: tail✝)) (head✝ :: tail✝) = true

State before:
head : Dimension
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
h : known (head :: tail) = true
⊢ shapeRefines (project (head :: tail)) (head :: tail) = true
Tactic:
case cons head tail ih =>
  cases head <;> simp at *; apply (ih h)
State after:
no goals

State before:
head : Dimension
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
h : known (head :: tail) = true
⊢ shapeRefines (project (head :: tail)) (head :: tail) = true
Tactic:
cases head <;> simp at *
State after:
case Known
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
a✝ : ℕ
h : known tail = true
⊢ shapeRefines (project tail) tail = true

State before:
case Known
tail : List Dimension
ih : known tail = true → shapeRefines (project tail) tail = true
a✝ : ℕ
h : known tail = true
⊢ shapeRefines (project tail) tail = true
Tactic:
apply (ih h)
State after:
no goals