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

State before:
r : Range
⊢ r.nth r.size < r.stop + r.step
Tactic:
simp [nth, size]
State after:
r : Range
⊢ r.start + (r.stop - r.start + r.step - 1) / r.step * r.step < r.stop + r.step

State before:
r : Range
⊢ r.start + (r.stop - r.start + r.step - 1) / r.step * r.step < r.stop + r.step
Tactic:
rw [Nat.add_comm, Nat.lt_iff_add_one_le, Nat.add_assoc]
State after:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step + (r.start + 1) ≤ r.stop + r.step

State before:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step + (r.start + 1) ≤ r.stop + r.step
Tactic:
apply Nat.add_le_of_le_sub
State after:
case hle
r : Range
⊢ r.start + 1 ≤ r.stop + r.step

case h
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step ≤ r.stop + r.step - (r.start + 1)

State before:
case h
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step ≤ r.stop + r.step - (r.start + 1)
Tactic:
convert Nat.div_mul_le_self _ _ using 1
State after:
case h.e'_4
r : Range
⊢ r.stop + r.step - (r.start + 1) = r.stop - r.start + r.step - 1

State before:
case h.e'_4
r : Range
⊢ r.stop + r.step - (r.start + 1) = r.stop - r.start + r.step - 1
Tactic:
rw [Nat.add_comm, Nat.sub_add_eq,
    Nat.add_sub_assoc r.start_le_stop,
    Nat.add_comm,
    Nat.add_sub_assoc r.step_pos]
State after:
no goals

State before:
case hle
r : Range
⊢ r.start + 1 ≤ r.stop + r.step
Tactic:
apply Nat.add_le_add
State after:
case hle.h₁
r : Range
⊢ r.start ≤ r.stop

case hle.h₂
r : Range
⊢ 1 ≤ r.step

State before:
case hle.h₁
r : Range
⊢ r.start ≤ r.stop

case hle.h₂
r : Range
⊢ 1 ≤ r.step
Tactic:
simp
State after:
case hle.h₂
r : Range
⊢ 1 ≤ r.step

State before:
case hle.h₂
r : Range
⊢ 1 ≤ r.step
Tactic:
apply r.step_pos
State after:
no goals