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

State before:
r : Range
x : ℕ
h : x ∈ r
⊢ r.nth (r.ofNth x) = x
Tactic:
simp [mem_def] at h
State after:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.nth (r.ofNth x) = x

State before:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.nth (r.ofNth x) = x
Tactic:
simp [nth, ofNth]
State after:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) / r.step * r.step = x

State before:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) / r.step * r.step = x
Tactic:
rw [Nat.div_mul_cancel h.2.2]
State after:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) = x

State before:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) = x
Tactic:
simp only [*, ge_iff_le, add_tsub_cancel_of_le]
State after:
no goals