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

State before:
S : List ℕ
D : DimList
⊢ known D = true → shapeRefines S D = true → project D = S
Tactic:
intros Hknown Hrefines
State after:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project D = S

State before:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project D = S
Tactic:
rw [dim_known_refines_inv Hknown Hrefines]
State after:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project (List.map Dimension.Known S) = S

State before:
S : List ℕ
D : DimList
Hknown : known D = true
Hrefines : shapeRefines S D = true
⊢ project (List.map Dimension.Known S) = S
Tactic:
clear D Hknown Hrefines
State after:
S : List ℕ
⊢ project (List.map Dimension.Known S) = S

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

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