-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b

Proof state:
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
⊢ (if hlt : i < as.size then do
      let __do_lift ← f as[i]
      mapM.map f as (i + 1) (b.push __do_lift)
    else pure b) =
    foldl (fun r a => r.push (f a)) b as i

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ (do
      let __do_lift ← f as[i]
      mapM.map f as (i + 1) (b.push __do_lift)) =
    foldl (fun r a => r.push (f a)) b as i

case isFalse
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ pure b = foldl (fun r a => r.push (f a)) b as i

Proof state:
case isFalse
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ pure b = foldl (fun r a => r.push (f a)) b as i

Tactic:
dsimp [foldl, Id.run, foldlM]

Result:
case isFalse
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ b =
    if h : as.size ≤ as.size then foldlM.loop (fun r a => r.push (f a)) as as.size h (as.size - i) i b
    else foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ (as.size - i) i b

Proof state:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ mapM.map f as (i + 1) (b.push (f as[i])) =
    if h : as.size ≤ as.size then foldlM.loop (fun r a => r.push (f a)) as as.size h (as.size - i) i b
    else foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ (as.size - i) i b

Tactic:
rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]

Result:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ foldl (fun r a => r.push (f a)) (b.push (f as[i])) as (i + 1) =
    match as.size - i with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← b.push (f as[i])
      foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ i' (i + 1) __do_lift

Proof state:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ foldl (fun r a => r.push (f a)) (b.push (f as[i])) as (i + 1) =
    match as.size - i with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← b.push (f as[i])
      foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ i' (i + 1) __do_lift

Tactic:
have : size as - i = Nat.succ (size as - i - 1) := by omega

Result:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
this : as.size - i = (as.size - i - 1).succ
⊢ foldl (fun r a => r.push (f a)) (b.push (f as[i])) as (i + 1) =
    match as.size - i with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← b.push (f as[i])
      foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ i' (i + 1) __do_lift

Proof state:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
this : as.size - i = (as.size - i - 1).succ
⊢ foldl (fun r a => r.push (f a)) (b.push (f as[i])) as (i + 1) =
    match (as.size - i - 1).succ with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← b.push (f as[i])
      foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ i' (i + 1) __do_lift

Tactic:
simp [foldl, foldlM, Id.run, Nat.sub_add_eq]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ b =
    if h : as.size ≤ as.size then foldlM.loop (fun r a => r.push (f a)) as as.size h (as.size - i) i b
    else foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ (as.size - i) i b

Tactic:
rw [dif_pos (by omega), foldlM.loop, dif_neg h]

Result:
case isFalse
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ b = pure b

Proof state:
case isFalse
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ b = pure b

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ (do
      let __do_lift ← f as[i]
      mapM.map f as (i + 1) (b.push __do_lift)) =
    foldl (fun r a => r.push (f a)) b as i

Tactic:
simp only [Id.bind_eq]

Result:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ mapM.map f as (i + 1) (b.push (f as[i])) = foldl (fun r a => r.push (f a)) b as i

Proof state:
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ as.size - i = (as.size - i - 1).succ

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
this : as.size - i = (as.size - i - 1).succ
⊢ foldl (fun r a => r.push (f a)) (b.push (f as[i])) as (i + 1) =
    match as.size - i with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← b.push (f as[i])
      foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ i' (i + 1) __do_lift

Tactic:
rw [this]

Result:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
this : as.size - i = (as.size - i - 1).succ
⊢ foldl (fun r a => r.push (f a)) (b.push (f as[i])) as (i + 1) =
    match (as.size - i - 1).succ with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← b.push (f as[i])
      foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ i' (i + 1) __do_lift

Proof state:
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : ¬i < as.size
⊢ as.size ≤ as.size

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ mapM.map f as (i + 1) (b.push (f as[i])) = foldl (fun r a => r.push (f a)) b as i

Tactic:
dsimp [foldl, Id.run, foldlM]

Result:
case isTrue
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ mapM.map f as (i + 1) (b.push (f as[i])) =
    if h : as.size ≤ as.size then foldlM.loop (fun r a => r.push (f a)) as as.size h (as.size - i) i b
    else foldlM.loop (fun r a => r.push (f a)) as as.size ⋯ (as.size - i) i b

Proof state:
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
⊢ mapM.map f as i b = foldl (fun r a => r.push (f a)) b as i

Tactic:
unfold mapM.map

Result:
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
⊢ (if hlt : i < as.size then do
      let __do_lift ← f as[i]
      mapM.map f as (i + 1) (b.push __do_lift)
    else pure b) =
    foldl (fun r a => r.push (f a)) b as i

Proof state:
α : Type u_1
β : Type u_2
b : Array β
as : Array α
f : α → β
i : Nat
h : i < as.size
⊢ as.size ≤ as.size

Tactic:
omega

Result:
no goals