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

Tactic:
case s =>
intro ⟨i, hi⟩ arr ⟨ih₁, eq, ih₂⟩
refine (hs _ ih₁).map fun ⟨h₁, h₂⟩ => ⟨h₂, by simp [eq], fun j hj => ?_⟩
simp [getElem_push] at hj ⊢; split; {apply ih₂}
cases j; cases (Nat.le_or_eq_of_le_succ hj).resolve_left ‹_›; cases eq; exact 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 α
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]

Tactic:
apply ih₂

Result:
no goals

Proof state:
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 #[]

Tactic:
case z => exact ⟨h0, rfl, nofun⟩

Result:
no goals

Proof state:
case isFalse.mk.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])
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)
isLt✝ : arr.toList.length < as.size
hj : ↑⟨arr.toList.length, isLt✝⟩ < arr.size + 1
h✝ : ¬↑⟨arr.toList.length, isLt✝⟩ < arr.size
⊢ p ⟨arr.toList.length, isLt✝⟩ a✝

Tactic:
cases eq

Result:
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✝

Proof state:
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✝

Tactic:
cases (Nat.le_or_eq_of_le_succ hj).resolve_left ‹_›

Result:
case isFalse.mk.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])
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)
isLt✝ : arr.toList.length < as.size
hj : ↑⟨arr.toList.length, isLt✝⟩ < arr.size + 1
h✝ : ¬↑⟨arr.toList.length, isLt✝⟩ < arr.size
⊢ p ⟨arr.toList.length, isLt✝⟩ a✝

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]) (mapM f as)

Tactic:
rw [mapM_eq_foldlM]

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

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

Tactic:
intro ⟨i, hi⟩ arr ⟨ih₁, eq, ih₂⟩

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]
⊢ 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⟩])

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])
⊢ (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) 0 #[]

Tactic:
exact ⟨h0, rfl, nofun⟩

Result:
no goals