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

Tactic:
simp [getElem_push]

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
hi' : i < bs.size + 1
⊢ p i (if h : i < bs.size then bs[i] else b) hi

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

Tactic:
simp at hi'

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
hi' : i < bs.size + 1
⊢ p i (bs.push b)[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 : (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)
⊢ j + 1 = (bs.push b).size

Tactic:
simp [h₁]

Result:
no goals

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

Tactic:
exact hb.1

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)
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
⊢ motive j

Tactic:
exact hm

Result:
no goals