-- 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:
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:
cases h₁.symm ▸ (Nat.le_or_eq_of_le_succ hi').resolve_left h

Result:
case refl
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_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] 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)
hi : j < as.size
hi'✝ : j < (bs.push b).size
hi' : j < bs.size + 1
h : ¬j < bs.size
⊢ p j 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)
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

Tactic:
exact h₂ _ _ h

Result:
no goals

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
⊢ SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h) (pure bs)

Tactic:
have := (Nat.zero_add _).symm.trans h

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

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_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] 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
⊢ SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] h) do
    let __do_lift ← f j as[j] ⋯
    mapFinIdxM.map as f i (j + 1) ⋯ (bs.push __do_lift)

Tactic:
refine (hs _ _ (by exact hm)).bind fun b hb => ih (by simp [h₁]) (fun i hi hi' => ?_) hb.2

Result:
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
⊢ p i (bs.push b)[i] hi

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

Tactic:
next h => exact h₂ _ _ h

Result:
no goals