-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem mem_of_mem_range'_aux {r : Range} {a : Nat} (w₁ : (i - r.start) % r.step = 0)
    (w₂ : r.start ≤ i)
    (h : a ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) : a ∈ r

Proof state:
i : Nat
r : Range
a : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
h : a ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ a ∈ r

Tactic:
obtain ⟨j, h', rfl⟩ := List.mem_range'.1 h

Result:
case intro.intro
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : j < (r.stop - i + r.step - 1) / r.step
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j ∈ r

Proof state:
case intro.intro
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : r.step * j < r.stop - i + r.step - 1 - (r.step - 1)
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j < r.stop ∧ (i + r.step * j - r.start) % r.step = 0

Tactic:
constructor

Result:
case intro.intro.left
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : r.step * j < r.stop - i + r.step - 1 - (r.step - 1)
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j < r.stop

case intro.intro.right
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : r.step * j < r.stop - i + r.step - 1 - (r.step - 1)
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ (i + r.step * j - r.start) % r.step = 0

Proof state:
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : j < (r.stop - i + r.step - 1) / r.step
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ r.start ≤ i + r.step * j

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : j < (r.stop - i + r.step - 1) / r.step
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j < r.stop ∧ (i + r.step * j - r.start) % r.step = 0

Tactic:
rw [Nat.lt_div_iff_mul_lt r.step_pos, Nat.mul_comm] at h'

Result:
case intro.intro
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : r.step * j < r.stop - i + r.step - 1 - (r.step - 1)
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j < r.stop ∧ (i + r.step * j - r.start) % r.step = 0

Proof state:
case intro.intro
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : j < (r.stop - i + r.step - 1) / r.step
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j ∈ r

Tactic:
refine ⟨by omega, ?_⟩

Result:
case intro.intro
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : j < (r.stop - i + r.step - 1) / r.step
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j < r.stop ∧ (i + r.step * j - r.start) % r.step = 0

Proof state:
case intro.intro.left
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : r.step * j < r.stop - i + r.step - 1 - (r.step - 1)
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ i + r.step * j < r.stop

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro.right
i : Nat
r : Range
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
j : Nat
h' : r.step * j < r.stop - i + r.step - 1 - (r.step - 1)
h : i + r.step * j ∈ List.range' i ((r.stop - i + r.step - 1) / r.step) r.step
⊢ (i + r.step * j - r.start) % r.step = 0

Tactic:
rwa [Nat.add_comm, Nat.add_sub_assoc w₂, Nat.mul_add_mod_self_left]

Result:
no goals