α : Type u_1
β : Type u_2
as : Array α
f : Fin (size as) → α → β
motive : Nat → Prop
h0 : motive 0
p : Fin (size as) → β → Prop
hs : ∀ (i : Fin (size as)), motive i.val → p i (f i as[i]) ∧ motive (i.val + 1)
this :
  ∀ (p : Fin (size as) → β → Prop),
    (∀ (i : Fin (size as)), motive i.val → SatisfiesM (fun x => p i x ∧ motive (i.val + 1)) (f i as[i])) →
      SatisfiesM (fun arr => motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } arr[i])
        (mapIdxM as f)
⊢ motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdx as f)[i]
α : Type u_1
β : Type u_2
as : Array α
f : Fin (size as) → α → β
motive : Nat → Prop
h0 : motive 0
p : Fin (size as) → β → Prop
hs : ∀ (i : Fin (size as)), motive i.val → p i (f i as[i]) ∧ motive (i.val + 1)
⊢ motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdx as f)[i]
have := SatisfiesM_mapIdxM (m := Id) (as := as) (f := f) motive h0
α : Type u_1
β : Type u_2
as : Array α
f : Fin (size as) → α → β
motive : Nat → Prop
h0 : motive 0
p : Fin (size as) → β → Prop
hs : ∀ (i : Fin (size as)), motive i.val → p i (f i as[i]) ∧ motive (i.val + 1)
this :
  ∀ (p : Fin (size as) → β → Prop),
    (∀ (i : Fin (size as)), motive i.val → p i (f i as[i.val]) ∧ motive (i.val + 1)) →
      motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdxM as f)[i]
⊢ motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdx as f)[i]
α : Type u_1
β : Type u_2
as : Array α
f : Fin (size as) → α → β
motive : Nat → Prop
h0 : motive 0
p : Fin (size as) → β → Prop
hs : ∀ (i : Fin (size as)), motive i.val → p i (f i as[i]) ∧ motive (i.val + 1)
this :
  ∀ (p : Fin (size as) → β → Prop),
    (∀ (i : Fin (size as)), motive i.val → SatisfiesM (fun x => p i x ∧ motive (i.val + 1)) (f i as[i])) →
      SatisfiesM (fun arr => motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } arr[i])
        (mapIdxM as f)
⊢ motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdx as f)[i]
simp [SatisfiesM_Id_eq] at this
no goals
α : Type u_1
β : Type u_2
as : Array α
f : Fin (size as) → α → β
motive : Nat → Prop
h0 : motive 0
p : Fin (size as) → β → Prop
hs : ∀ (i : Fin (size as)), motive i.val → p i (f i as[i]) ∧ motive (i.val + 1)
this :
  ∀ (p : Fin (size as) → β → Prop),
    (∀ (i : Fin (size as)), motive i.val → p i (f i as[i.val]) ∧ motive (i.val + 1)) →
      motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdxM as f)[i]
⊢ motive (size as) ∧ ∃ eq, ∀ (i : Nat) (h : i < size as), p { val := i, isLt := h } (mapIdx as f)[i]
exact this _ hs