Theorem: List.getElem_mem (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l : List α
i : Nat
hi : i < length l
⊢ l[i] ∈ l
Tactic:
rewrite [getElem_eq_get]
State after:
α : Type u
β : Type v
l : List α
i : Nat
hi : i < length l
⊢ get l { val := i, isLt := hi } ∈ l

State before:
α : Type u
β : Type v
l : List α
i : Nat
hi : i < length l
⊢ get l { val := i, isLt := hi } ∈ l
Tactic:
exact l.get_mem i hi
State after:
no goals