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

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
i✝ : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i✝ + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h)
            (mapFinIdxM.map as f i✝ j h bs)
bs : Array β
j : Nat
h : i✝ + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
b : β
hb : p j b ⋯ ∧ motive (j + 1)
i : Nat
hi : i < as.size
hi'✝ : i < (bs.push b).size
hi' : i < bs.size + 1
⊢ p i (if h : i < bs.size then bs[i] else b) hi

Tactic:
split

Result:
case succ.isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
i✝ : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i✝ + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h)
            (mapFinIdxM.map as f i✝ j h bs)
bs : Array β
j : Nat
h : i✝ + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
b : β
hb : p j b ⋯ ∧ motive (j + 1)
i : Nat
hi : i < as.size
hi'✝ : i < (bs.push b).size
hi' : i < bs.size + 1
h✝ : i < bs.size
⊢ p i bs[i] hi

case succ.isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
i✝ : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i✝ + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h)
            (mapFinIdxM.map as f i✝ j h bs)
bs : Array β
j : Nat
h : i✝ + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
b : β
hb : p j b ⋯ ∧ motive (j + 1)
i : Nat
hi : i < as.size
hi'✝ : i < (bs.push b).size
hi' : i < bs.size + 1
h✝ : ¬i < bs.size
⊢ p i b 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 : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
⊢ SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h) (as.mapFinIdxM f)

Tactic:
simp [mapFinIdxM]

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

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
bs : Array β
j : Nat
h : 0 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
this : j = as.size
⊢ SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h) (pure bs)

Tactic:
exact .pure ⟨this ▸ hm, h₁ ▸ this, fun _ _ => 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 : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
⊢ SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h)
    (mapFinIdxM.map as f as.size 0 ⋯ #[])

Tactic:
exact go rfl nofun h0

Result:
no goals

Proof state:
case succ.isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
f : (i : Nat) → α → i < as.size → m β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)
i✝ : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i✝ + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h)
            (mapFinIdxM.map as f i✝ j h bs)
bs : Array β
j : Nat
h : i✝ + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
b : β
hb : p j b ⋯ ∧ motive (j + 1)
i : Nat
hi : i < as.size
hi'✝ : i < (bs.push b).size
hi' : i < bs.size + 1
h✝ : ¬i < bs.size
⊢ p i b hi

Tactic:
next h => cases h₁.symm ▸ (Nat.le_or_eq_of_le_succ hi').resolve_left h; exact hb.1

Result:
no goals