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

State before:
r : Range
i : ℕ
⊢ r.nth i < r.stop ↔ i < r.size
Tactic:
simp [nth, size, Nat.lt_iff_add_one_le,
      Nat.le_div_iff_mul_le r.step_pos]
State after:
r : Range
i : ℕ
⊢ r.start + i * r.step + 1 ≤ r.stop ↔ (i + 1) * r.step ≤ r.stop - r.start + r.step - 1

State before:
r : Range
i : ℕ
⊢ r.start + i * r.step + 1 ≤ r.stop ↔ (i + 1) * r.step ≤ r.stop - r.start + r.step - 1
Tactic:
zify
State after:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑(r.stop - r.start + r.step - 1)

State before:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑(r.stop - r.start + r.step - 1)
Tactic:
simp
State after:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑r.stop - ↑r.start + ↑r.step - 1

State before:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑r.stop - ↑r.start + ↑r.step - 1
Tactic:
constructor <;> intro h <;> linarith
State after:
no goals