case intro.intro
r : Range
i : Nat
h' : i < numElems r
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
⊢ r.start + r.step * i ∈ r
x : Nat
r : Range
h : x ∈ List.range' r.start (numElems r) r.step
⊢ x ∈ r
obtain ⟨i, h', rfl⟩ := List.mem_range'.1 h
case intro.intro
r : Range
i : Nat
h' : i < numElems r
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
⊢ r.start + r.step * i < r.stop
case intro.intro
r : Range
i : Nat
h' : i < numElems r
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
⊢ r.start + r.step * i ∈ r
refine ⟨Nat.le_add_right .., ?_⟩
case intro.intro
r : Range
i : Nat
h' : i < if r.step = 0 then if r.stop ≤ r.start then 0 else r.stop else (r.stop - r.start + r.step - 1) / r.step
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
⊢ r.start + r.step * i < r.stop
case intro.intro
r : Range
i : Nat
h' : i < numElems r
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
⊢ r.start + r.step * i < r.stop
unfold numElems at h'
case intro.intro.inl
r : Range
i : Nat
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
h✝ : r.step = 0
h' : i < if r.stop ≤ r.start then 0 else r.stop
⊢ r.start + r.step * i < r.stop

case intro.intro.inr
r : Range
i : Nat
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
h✝ : ¬r.step = 0
h' : i < (r.stop - r.start + r.step - 1) / r.step
⊢ r.start + r.step * i < r.stop
case intro.intro
r : Range
i : Nat
h' : i < if r.step = 0 then if r.stop ≤ r.start then 0 else r.stop else (r.stop - r.start + r.step - 1) / r.step
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
⊢ r.start + r.step * i < r.stop
split at h'
no goals
case intro.intro.inl
r : Range
i : Nat
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
h✝ : r.step = 0
h' : i < if r.stop ≤ r.start then 0 else r.stop
⊢ r.start + r.step * i < r.stop
split at h' <;> [cases h'; simp_all]
no goals
case intro.intro.inr
r : Range
i : Nat
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
h✝ : ¬r.step = 0
h' : i < (r.stop - r.start + r.step - 1) / r.step
⊢ r.start + r.step * i < r.stop
next step0 =>
refine Nat.not_le.1 fun h =>
  Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h
no goals
r : Range
i : Nat
h : r.start + r.step * i ∈ List.range' r.start (numElems r) r.step
step0 : ¬r.step = 0
h' : i < (r.stop - r.start + r.step - 1) / r.step
⊢ r.start + r.step * i < r.stop
refine Nat.not_le.1 fun h =>
  Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h