-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m]
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → m β}
    (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → SatisfiesM (motive (i.1 + 1)) (f b as[i])) :
    SatisfiesM (motive as.size) (as.foldlM f init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
⊢ SatisfiesM (motive as.size) (foldlM f init as)

Tactic:
simp [foldlM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
⊢ SatisfiesM (motive as.size) (foldlM.loop f as as.size ⋯ as.size 0 init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
j : Nat
b : β
h₁ : j ≤ as.size
H : motive j b
hj : j < as.size
i✝ i'✝ : Nat
h₂ : as.size ≤ i'✝.succ + j
x✝ : β
⊢ as.size ≤ i'✝ + (↑⟨j, hj⟩ + 1)

Tactic:
rwa [Nat.succ_add] at h₂

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
hj : ¬j < as.size
⊢ SatisfiesM (motive as.size) (pure b)

Tactic:
exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ .pure H

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
⊢ SatisfiesM (motive as.size) (foldlM.loop f as as.size ⋯ as.size 0 init)

Tactic:
exact go (Nat.zero_le _) (Nat.le_refl _) h0

Result:
no goals

Proof state:
case h_1
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
j : Nat
b : β
h₁ : j ≤ as.size
H : motive j b
hj : j < as.size
i✝ : Nat
h₂ : as.size ≤ 0 + j
⊢ SatisfiesM (motive as.size) (pure b)

Tactic:
cases Nat.not_le_of_gt (by simp [hj]) h₂

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
⊢ SatisfiesM (motive as.size)
    (if hlt : j < as.size then
      match i with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[j]
        foldlM.loop f as as.size ⋯ i' (j + 1) __do_lift
    else pure b)

Tactic:
split

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
h✝ : j < as.size
⊢ SatisfiesM (motive as.size)
    (match i with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[j]
      foldlM.loop f as as.size ⋯ i' (j + 1) __do_lift)

case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
h✝ : ¬j < as.size
⊢ SatisfiesM (motive as.size) (pure b)

Proof state:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
h✝ : ¬j < as.size
⊢ SatisfiesM (motive as.size) (pure b)

Tactic:
next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ .pure H

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
j : Nat
b : β
h₁ : j ≤ as.size
H : motive j b
hj : j < as.size
i✝ : Nat
h₂ : as.size ≤ 0 + j
⊢ as.size > 0 + j

Tactic:
simp [hj]

Result:
no goals

Proof state:
case h_2
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
j : Nat
b : β
h₁ : j ≤ as.size
H : motive j b
hj : j < as.size
i✝ i'✝ : Nat
h₂ : as.size ≤ i'✝.succ + j
⊢ SatisfiesM (motive as.size)
    (let_fun this := ⋯;
    do
    let __do_lift ← f b as[j]
    foldlM.loop f as as.size ⋯ i'✝ (j + 1) __do_lift)

Tactic:
exact (hf ⟨j, hj⟩ b H).bind fun _ => go hj (by rwa [Nat.succ_add] at h₂)

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
⊢ SatisfiesM (motive as.size) (foldlM.loop f as as.size ⋯ i j b)

Tactic:
unfold foldlM.loop

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
⊢ SatisfiesM (motive as.size)
    (if hlt : j < as.size then
      match i with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[j]
        foldlM.loop f as as.size ⋯ i' (j + 1) __do_lift
    else pure b)