-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
    forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Proof state:
case isFalse
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : ¬i < r.stop
⊢ pure PUnit.unit = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

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
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : ¬i < r.stop
this : (r.stop - i + r.step - 1) / r.step = 0
⊢ pure PUnit.unit = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Proof state:
case isTrue
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
⊢ (do
      f i
      have this : 0 < r.step := ⋯
      forM.loop r f (i + r.step)) =
    forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Tactic:
simp [size_eq r h, List.range'_succ, List.forM_cons]

Result:
case isTrue
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
⊢ (do
      f i
      forM.loop r f (i + r.step)) =
    do
    f i
    forM (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) f

Proof state:
case isFalse
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : ¬i < r.stop
this : (r.stop - i + r.step - 1) / r.step = 0
⊢ pure PUnit.unit = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Tactic:
simp [this]

Result:
no goals

Proof state:
case isTrue
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
⊢ (do
      f i
      forM.loop r f (i + r.step)) =
    do
    f i
    forM (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) f

Tactic:
congr 1

Result:
case isTrue.e_a
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
⊢ (fun x => forM.loop r f (i + r.step)) = fun x =>
    forM (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) f

Proof state:
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
⊢ (if i < r.stop then do
      f i
      have this : 0 < r.step := ⋯
      forM.loop r f (i + r.step)
    else pure PUnit.unit) =
    forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Tactic:
split <;> rename_i h

Result:
case isTrue
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
⊢ (do
      f i
      have this : 0 < r.step := ⋯
      forM.loop r f (i + r.step)) =
    forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

case isFalse
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : ¬i < r.stop
⊢ pure PUnit.unit = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Proof state:
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
⊢ forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Tactic:
have w := r.step_pos

Result:
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
⊢ forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Proof state:
case isTrue.e_a.h
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
x✝ : PUnit
⊢ forM.loop r f (i + r.step) = forM (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) f

Tactic:
rw [forM_loop_eq_forM_range']

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
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
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
⊢ (fun x => forM.loop r f (i + r.step)) = fun x =>
    forM (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) f

Tactic:
funext

Result:
case isTrue.e_a.h
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
h : i < r.stop
x✝ : PUnit
⊢ forM.loop r f (i + r.step) = forM (List.range' (i + r.step) ((r.stop - (i + r.step) + r.step - 1) / r.step) r.step) f

Proof state:
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
⊢ forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f

Tactic:
rw [forM.loop]

Result:
m : Type u_1 → Type u_2
i : Nat
inst✝ : Monad m
r : Range
f : Nat → m PUnit
w : 0 < r.step
⊢ (if i < r.stop then do
      f i
      have this : 0 < r.step := ⋯
      forM.loop r f (i + r.step)
    else pure PUnit.unit) =
    forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f