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

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
b : β
x✝² : Nat
x✝¹ : x✝² ≤ as.size
x✝ : 0 ≤ as.size
H : motive 0 b
hi : ¬0 = 0
⊢ SatisfiesM (motive 0) (pure b)

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i✝ : Nat
h✝ : i✝ + 1 ≤ as.size
H : motive i✝.succ b
hi : ¬i✝.succ = 0
⊢ SatisfiesM (motive 0) do
    let __do_lift ← f as[i✝] b
    foldrM.fold f as 0 i✝ ⋯ __do_lift

Tactic:
{simp at hi}

Result:
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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i✝ : Nat
h✝ : i✝ + 1 ≤ as.size
H : motive i✝.succ b
hi : ¬i✝.succ = 0
⊢ SatisfiesM (motive 0) do
    let __do_lift ← f as[i✝] b
    foldrM.fold f as 0 i✝ ⋯ __do_lift

Proof state:
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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
h✝ : 0 < as.size
⊢ SatisfiesM (motive 0) (foldrM.fold f as 0 as.size ⋯ init)

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ SatisfiesM (motive 0) (pure init)

Tactic:
{exact go _ h0}

Result:
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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ SatisfiesM (motive 0) (pure 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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
b : β
x✝¹ : Nat
x✝ : x✝¹ ≤ as.size
i : Nat
hi' : i + 1 ≤ as.size
H : motive i.succ b
hi : ¬i.succ = 0
⊢ SatisfiesM (motive 0) do
    let __do_lift ← f as[i] b
    foldrM.fold f as 0 i ⋯ __do_lift

Tactic:
exact (hf ⟨i, hi'⟩ b H).bind fun _ => go _

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
⊢ SatisfiesM (motive 0) (if 0 < as.size then foldrM.fold f as 0 as.size ⋯ init else pure init)

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
h✝ : 0 < as.size
⊢ SatisfiesM (motive 0) (foldrM.fold f as 0 as.size ⋯ init)

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ SatisfiesM (motive 0) (pure 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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
i : Nat
b : β
hi✝ : i ≤ as.size
H : motive i b
hi : i = 0
⊢ SatisfiesM (motive 0) (pure b)

Tactic:
exact .pure (hi ▸ H)

Result:
no goals

Proof state:
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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
i : Nat
b : β
hi : i ≤ as.size
H : motive i b
h✝ : i = 0
⊢ SatisfiesM (motive 0) (pure b)

Tactic:
next hi => exact .pure (hi ▸ H)

Result:
no goals

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 as.size init
f : α → β → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)
h✝ : ¬0 < as.size
⊢ SatisfiesM (motive 0) (pure init)

Tactic:
next h => exact .pure (Nat.eq_zero_of_not_pos h ▸ h0)

Result:
no goals