-- 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 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

Tactic:
congr 1

Result:
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

Proof state:
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

Tactic:
simp

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
⊢ (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 ⋯

Tactic:
split <;> rename_i h

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 =>
          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 ⋯

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 ⋯

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
⊢ 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:
have w := r.step_pos

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
⊢ 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 ⋯