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

State before:
x : ℕ
r : Range
⊢ x ∈ r ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
Tactic:
simp [Membership.mem, contains]
State after:
x : ℕ
r : Range
⊢ (r.start ≤ x ∧ x < r.stop) ∧ r.step ∣ x - r.start ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start

State before:
x : ℕ
r : Range
⊢ (r.start ≤ x ∧ x < r.stop) ∧ r.step ∣ x - r.start ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
Tactic:
exact and_assoc
State after:
no goals