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

State before:
x : ℕ
r : Range
⊢ x ∈ r ↔ ∃ i, x = r.get i
Tactic:
constructor
State after:
case mp
x : ℕ
r : Range
⊢ x ∈ r → ∃ i, x = r.get i

case mpr
x : ℕ
r : Range
⊢ (∃ i, x = r.get i) → x ∈ r

State before:
case mp
x : ℕ
r : Range
⊢ x ∈ r → ∃ i, x = r.get i
Tactic:
intro h
State after:
case mp
x : ℕ
r : Range
h : x ∈ r
⊢ ∃ i, x = r.get i

State before:
case mp
x : ℕ
r : Range
h : x ∈ r
⊢ ∃ i, x = r.get i
Tactic:
have := nth_ofNth h
State after:
case mp
x : ℕ
r : Range
h : x ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, x = r.get i

State before:
case mp
x : ℕ
r : Range
h : x ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, x = r.get i
Tactic:
rw [← this] at h ⊢
State after:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, r.nth (r.ofNth x) = r.get i

State before:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
this : r.nth (r.ofNth x) = x
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Tactic:
clear this
State after:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
⊢ ∃ i, r.nth (r.ofNth x) = r.get i

State before:
case mp
x : ℕ
r : Range
h : r.nth (r.ofNth x) ∈ r
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Tactic:
simp at h
State after:
case mp
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ ∃ i, r.nth (r.ofNth x) = r.get i

State before:
case mp
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ ∃ i, r.nth (r.ofNth x) = r.get i
Tactic:
use ⟨_,h⟩
State after:
case h
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ r.nth (r.ofNth x) = r.get ⟨r.ofNth x, h⟩

State before:
case h
x : ℕ
r : Range
h : r.ofNth x < r.size
⊢ r.nth (r.ofNth x) = r.get ⟨r.ofNth x, h⟩
Tactic:
rfl
State after:
no goals

State before:
case mpr
x : ℕ
r : Range
⊢ (∃ i, x = r.get i) → x ∈ r
Tactic:
rintro ⟨⟨i,hi⟩,rfl⟩
State after:
case mpr.intro.mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r

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