-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
    (motive : Nat → Prop) (h0 : motive 0)
    (p : Fin as.size → β → Prop)
    (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f as[i])) :
    SatisfiesM
      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
      (Array.mapM f as)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
j : Fin as.size
hj : ↑j < (arr.push a✝).size
⊢ p j (arr.push a✝)[↑j]

Tactic:
simp [getElem_push] at hj ⊢

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
j : Fin as.size
hj : ↑j < arr.size + 1
⊢ p j (if h : ↑j < arr.size then arr[↑j] else a✝)

Proof state:
case isFalse.mk.refl.refl
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
arr : Array β
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
isLt✝ : arr.toList.length < as.size
hj : ↑⟨arr.toList.length, isLt✝⟩ < arr.size + 1
h✝ : ¬↑⟨arr.toList.length, isLt✝⟩ < arr.size
hi : arr.toList.length < as.size
ih₁ : motive ↑⟨arr.toList.length, hi⟩
x✝ : p ⟨arr.toList.length, hi⟩ a✝ ∧ motive (↑⟨arr.toList.length, hi⟩ + 1)
h₁ : p ⟨arr.toList.length, hi⟩ a✝
h₂ : motive (↑⟨arr.toList.length, hi⟩ + 1)
⊢ p ⟨arr.toList.length, isLt✝⟩ a✝

Tactic:
exact 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 α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
⊢ SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i])
    (foldlM (fun bs a => bs.push <$> f a) #[] as)

Tactic:
refine SatisfiesM_foldlM (m := m) (β := Array β)
  (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i (arr[i.1]'h2)) ?z ?s
  |>.imp fun ⟨h₁, eq, h₂⟩ => ⟨h₁, eq, fun _ _ => h₂ ..⟩

Result:
case z
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
⊢ (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) 0 #[]

case s
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
⊢ ∀ (i : Fin as.size) (b : Array β),
    (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i) b →
      SatisfiesM
        ((fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i + 1))
        (b.push <$> f as[i])

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 α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
j : Fin as.size
hj : ↑j < arr.size + 1
h✝ : ↑j < arr.size
⊢ p j arr[↑j]

case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
j : Fin as.size
hj : ↑j < arr.size + 1
h✝ : ¬↑j < arr.size
⊢ p j a✝

Tactic:
{apply ih₂}

Result:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
j : Fin as.size
hj : ↑j < arr.size + 1
h✝ : ¬↑j < arr.size
⊢ p j a✝

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 α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
j : Fin as.size
hj : ↑j < arr.size + 1
h✝ : ¬↑j < arr.size
⊢ p j a✝

Tactic:
cases j

Result:
case isFalse.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : α → m β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])
i : Nat
hi : i < as.size
arr : Array β
ih₁ : motive ↑⟨i, hi⟩
eq : arr.size = ↑⟨i, hi⟩
ih₂ : ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]
a✝ : β
x✝ : p ⟨i, hi⟩ a✝ ∧ motive (↑⟨i, hi⟩ + 1)
h₁ : p ⟨i, hi⟩ a✝
h₂ : motive (↑⟨i, hi⟩ + 1)
val✝ : Nat
isLt✝ : val✝ < as.size
hj : ↑⟨val✝, isLt✝⟩ < arr.size + 1
h✝ : ¬↑⟨val✝, isLt✝⟩ < arr.size
⊢ p ⟨val✝, isLt✝⟩ a✝