Theorem: LeanColls.Range.get_mem (LeanColls/Data/Range.lean)

State before:
r : Range
i : Fin r.size
⊢ r.get i ∈ r
Tactic:
rcases i with ⟨i,hi⟩
State after:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r

State before:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r
Tactic:
simp [get, mem_def, nth_lt_stop_iff_lt_size]
State after:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ i < r.size

State before:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ i < r.size
Tactic:
simp [nth, hi]
State after:
no goals