-- 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]
⊢ SatisfiesM
    ((fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑⟨i, hi⟩ + 1))
    (arr.push <$> f as[⟨i, hi⟩])

Tactic:
refine (hs _ ih₁).map fun ⟨h₁, h₂⟩ => ⟨h₂, by simp [eq], fun j 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.push a✝).size
⊢ p j (arr.push a✝)[↑j]

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)
⊢ (arr.push a✝).size = ↑⟨i, hi⟩ + 1

Tactic:
simp [eq]

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])
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✝)

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 α
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✝