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

State before:
r : Range
⊢ r.size = 0 ↔ r.isEmpty = true
Tactic:
simp [size, isEmpty]
State after:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step = 0 ↔ r.start = r.stop

State before:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step = 0 ↔ r.start = r.stop
Tactic:
rw [Nat.div_eq_zero_iff r.step_pos,
    Nat.lt_iff_add_one_le,
    Nat.sub_add_cancel]
State after:
r : Range
⊢ r.stop - r.start + r.step ≤ r.step ↔ r.start = r.stop

r : Range
⊢ 1 ≤ r.stop - r.start + r.step

State before:
r : Range
⊢ r.stop - r.start + r.step ≤ r.step ↔ r.start = r.stop
Tactic:
simp
State after:
r : Range
⊢ r.stop - r.start = 0 ↔ r.start = r.stop

State before:
r : Range
⊢ r.stop - r.start = 0 ↔ r.start = r.stop
Tactic:
rw [Nat.sub_eq_zero_iff_le, Nat.le_antisymm_iff]
State after:
r : Range
⊢ r.stop ≤ r.start ↔ r.start ≤ r.stop ∧ r.stop ≤ r.start

State before:
r : Range
⊢ r.stop ≤ r.start ↔ r.start ≤ r.stop ∧ r.stop ≤ r.start
Tactic:
simp only [start_le_stop, true_and]
State after:
no goals

State before:
r : Range
⊢ 1 ≤ r.stop - r.start + r.step
Tactic:
exact le_add_left r.step_pos
State after:
no goals