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

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

State before:
head : Dimension
tail✝ : List Dimension
ih : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head :: tail✝)) (head :: tail✝) = true
Tactic:
case cons head _ ih =>
  cases head <;> simp <;> apply ih
State after:
no goals

State before:
head : Dimension
tail✝ : List Dimension
ih : shapeRefines (defaultRefinement tail✝) tail✝ = true
⊢ shapeRefines (defaultRefinement (head :: tail✝)) (head :: tail✝) = true
Tactic:
cases head <;> simp <;> apply ih
State after:
no goals