-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) :
    forIn'.loop r f init i w₁ w₂ =
      forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init
        fun a h => f a (mem_of_mem_range'_aux w₁ w₂ h)

Proof state:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : ¬i < r.stop
⊢ pure init = forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Tactic:
have : (r.stop - i + r.step - 1) / r.step = 0 := by
  rw [Nat.div_eq_iff] <;> omega

Result:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : ¬i < r.stop
this : (r.stop - i + r.step - 1) / r.step = 0
⊢ pure init = forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Proof state:
case isTrue.e_a.h
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
step : ForInStep β
⊢ (match step with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop r f b (i + r.step) ⋯ ⋯) =
    match step with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b => f a' ⋯ b

Tactic:
split

Result:
case isTrue.e_a.h.h_1
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
__do_lift✝ : ForInStep β
b✝ : β
⊢ pure b✝ =
    match ForInStep.done b✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b => f a' ⋯ b

case isTrue.e_a.h.h_2
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
__do_lift✝ : ForInStep β
b✝ : β
⊢ forIn'.loop r f b✝ (i + r.step) ⋯ ⋯ =
    match ForInStep.yield b✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b => f a' ⋯ b

Proof state:
case isTrue
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
⊢ (do
      let __do_lift ← f i ⋯ init
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          let_fun this := ⋯;
          forIn'.loop r f b (i + r.step) ⋯ ⋯) =
    forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Tactic:
simp only [size_eq r h, List.range'_succ, List.forIn'_cons]

Result:
case isTrue
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
⊢ (do
      let __do_lift ← f i ⋯ init
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn'.loop r f b (i + r.step) ⋯ ⋯) =
    do
    let x ← f i ⋯ init
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b =>
        forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b =>
          f a' ⋯ b

Proof state:
case isFalse
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : ¬i < r.stop
this : (r.stop - i + r.step - 1) / r.step = 0
⊢ pure init = forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Tactic:
simp [this]

Result:
no goals

Proof state:
case isTrue.e_a.h.h_2
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
__do_lift✝ : ForInStep β
b✝ : β
⊢ forIn'.loop r f b✝ (i + r.step) ⋯ ⋯ =
    match ForInStep.yield b✝ with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b => f a' ⋯ b

Tactic:
rw [forIn'_loop_eq_forIn'_range']

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : ¬i < r.stop
⊢ (r.stop - i + r.step - 1) / r.step = 0

Tactic:
rw [Nat.div_eq_iff] <;> omega

Result:
no goals

Proof state:
case isTrue.e_a
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop r f b (i + r.step) ⋯ ⋯) =
    fun x =>
    match x with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b => f a' ⋯ b

Tactic:
funext step

Result:
case isTrue.e_a.h
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
h : i < r.stop
step : ForInStep β
⊢ (match step with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop r f b (i + r.step) ⋯ ⋯) =
    match step with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      forIn' (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) b fun a' m b => f a' ⋯ b

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
⊢ forIn'.loop r f init i w₁ w₂ =
    forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯

Tactic:
rw [forIn'.loop]

Result:
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
r : Range
init : β
f : (a : Nat) → a ∈ r → β → m (ForInStep β)
i : Nat
w₁ : (i - r.start) % r.step = 0
w₂ : r.start ≤ i
w : 0 < r.step
⊢ (if h : i < r.stop then do
      let __do_lift ← f i ⋯ init
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          let_fun this := ⋯;
          forIn'.loop r f b (i + r.step) ⋯ ⋯
    else pure init) =
    forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯