-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_fold_empty [Monad m] (f : α → β → m β) (init : β) (i j : Nat) (h) :
    foldrM.fold f #[] i j h init = pure init

Proof state:
case isFalse.h_2
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i x✝¹ : Nat
x✝ : x✝¹ ≤ #[].size
i✝ : Nat
h₂ : i✝ + 1 ≤ #[].size
h₁ : ¬(i✝.succ == i) = true
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f #[][i✝] init
    foldrM.fold f #[] i i✝ ⋯ __do_lift) =
    pure init

Tactic:
simp at h₂

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
⊢ (if (j == i) = true then pure init
    else
      match j, h with
      | 0, x => pure init
      | i_1.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f #[][i_1] init
        foldrM.fold f #[] i i_1 ⋯ __do_lift) =
    pure init

Tactic:
split <;> rename_i h₁

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
h₁ : (j == i) = true
⊢ pure init = pure init

case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
h₁ : ¬(j == i) = true
⊢ (match j, h with
    | 0, x => pure init
    | i_1.succ, h =>
      let_fun this := ⋯;
      do
      let __do_lift ← f #[][i_1] init
      foldrM.fold f #[] i i_1 ⋯ __do_lift) =
    pure init

Proof state:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
h₁ : ¬(j == i) = true
⊢ (match j, h with
    | 0, x => pure init
    | i_1.succ, h =>
      let_fun this := ⋯;
      do
      let __do_lift ← f #[][i_1] init
      foldrM.fold f #[] i i_1 ⋯ __do_lift) =
    pure init

Tactic:
split <;> rename_i h₂

Result:
case isFalse.h_1
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i x✝¹ : Nat
x✝ : x✝¹ ≤ #[].size
h₂ : 0 ≤ #[].size
h₁ : ¬(0 == i) = true
⊢ pure init = pure init

case isFalse.h_2
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i x✝¹ : Nat
x✝ : x✝¹ ≤ #[].size
i✝ : Nat
h₂ : i✝ + 1 ≤ #[].size
h₁ : ¬(i✝.succ == i) = true
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f #[][i✝] init
    foldrM.fold f #[] i i✝ ⋯ __do_lift) =
    pure init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
⊢ foldrM.fold f #[] i j h init = pure init

Tactic:
unfold foldrM.fold

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
⊢ (if (j == i) = true then pure init
    else
      match j, h with
      | 0, x => pure init
      | i_1.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f #[][i_1] init
        foldrM.fold f #[] i i_1 ⋯ __do_lift) =
    pure init

Proof state:
case isFalse.h_1
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i x✝¹ : Nat
x✝ : x✝¹ ≤ #[].size
h₂ : 0 ≤ #[].size
h₁ : ¬(0 == i) = true
⊢ pure init = pure init

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
i j : Nat
h : j ≤ #[].size
h₁ : (j == i) = true
⊢ pure init = pure init

Tactic:
rfl

Result:
no goals