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

State before:
S : List ℕ
⊢ shapeRefines S (List.map Dimension.Known S) = true
Tactic:
induction S <;> simp
State after:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
⊢ shapeRefines tail✝ (List.map Dimension.Known tail✝) = true

State before:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
⊢ shapeRefines tail✝ (List.map Dimension.Known tail✝) = true
Tactic:
assumption
State after:
no goals