-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_induction
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β}
    (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → motive (i.1 + 1) (f b as[i])) :
    motive as.size (as.foldl f init)

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ 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)

Tactic:
split

Result:
case h_1
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ motive as.size (pure b)

case h_2
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ 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)

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ motive as.size (pure b)

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

Result:
no goals

Proof state:
case h_2
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ 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 go hj (by rwa [Nat.succ_add] at h₂) (hf ⟨j, hj⟩ b H)

Result:
no goals

Proof state:
case h_1
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ motive as.size (pure b)

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

Result:
no goals

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

Tactic:
unfold foldlM.loop

Result:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
⊢ 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)

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
⊢ 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
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ 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
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ motive as.size (pure b)

Proof state:
case isFalse
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ motive as.size (pure b)

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

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → 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
⊢ as.size ≤ i'✝ + (j + 1)

Tactic:
rwa [Nat.succ_add] at h₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])
⊢ motive as.size (foldl f init as)

Tactic:
simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0

Result:
no goals