-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
    (f : (i : Nat) → α → (h : i < l.length) → m β) :
    l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
x : β
⊢ Array.mapFinIdxM.map l.toArray f k (acc.push x).size ⋯ (acc.push x) =
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push x) ⋯

Tactic:
conv => enter [2, 2, 3]; rw [← Array.size_push _ x]

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
x : β
⊢ Array.mapFinIdxM.map l.toArray f k (acc.push x).size ⋯ (acc.push x) =
    toArray <$> mapFinIdxM.go l f (drop (acc.push x).size l) (acc.push x) ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
inv : i + acc.size = l.length
⊢ (drop acc.size l).length + acc.size = l.length

Tactic:
simp [Nat.sub_add_cancel (Nat.le.intro (Nat.add_comm _ _ ▸ inv))]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f (k + 1) acc.size inv acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯

Tactic:
conv => enter [2, 2, 3]; rw [← getElem_cons_drop l acc.size (by omega)]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f (k + 1) acc.size inv acc =
    toArray <$> mapFinIdxM.go l f (l[acc.size] :: drop (acc.size + 1) l) acc ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f (k + 1) acc.size inv acc =
    toArray <$> mapFinIdxM.go l f (l[acc.size] :: drop (acc.size + 1) l) acc ⋯

Tactic:
simp only [Array.mapFinIdxM.map, mapFinIdxM.go, _root_.map_bind]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ (do
      let __do_lift ← f acc.size l.toArray[acc.size] ⋯
      Array.mapFinIdxM.map l.toArray f k (acc.size + 1) ⋯ (acc.push __do_lift)) =
    do
    let a ← f acc.size l[acc.size] ⋯
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push a) ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
inv✝ : 0 + acc.size = l.length
inv : acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f 0 acc.size inv✝ acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯

Tactic:
simp only [Array.mapFinIdxM.map, inv, drop_length, mapFinIdxM.go, map_pure]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
inv : i + acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f i acc.size inv acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯

Tactic:
match i with
| 0 =>
  rw [Nat.zero_add] at inv
  simp only [Array.mapFinIdxM.map, inv, drop_length, mapFinIdxM.go, map_pure]
| k + 1 =>
  conv => enter [2, 2, 3]; rw [← getElem_cons_drop l acc.size (by omega)]
  simp only [Array.mapFinIdxM.map, mapFinIdxM.go, _root_.map_bind]
  congr; funext x
  conv => enter [1, 4]; rw [← Array.size_push _ x]
  conv => enter [2, 2, 3]; rw [← Array.size_push _ x]
  refine go k (acc.push x) _

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ (do
      let __do_lift ← f acc.size l.toArray[acc.size] ⋯
      Array.mapFinIdxM.map l.toArray f k (acc.size + 1) ⋯ (acc.push __do_lift)) =
    do
    let a ← f acc.size l[acc.size] ⋯
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push a) ⋯

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ (fun __do_lift => Array.mapFinIdxM.map l.toArray f k (acc.size + 1) ⋯ (acc.push __do_lift)) = fun a =>
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push a) ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
⊢ l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f

Tactic:
simp only [Array.mapFinIdxM, mapFinIdxM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
⊢ Array.mapFinIdxM.map l.toArray f l.toArray.size 0 ⋯ (Array.mkEmpty l.toArray.size) =
    toArray <$> mapFinIdxM.go l f l #[] ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
⊢ Array.mapFinIdxM.map l.toArray f l.toArray.size 0 ⋯ (Array.mkEmpty l.toArray.size) =
    toArray <$> mapFinIdxM.go l f l #[] ⋯

Tactic:
exact go _ #[] _

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
inv : 0 + acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f 0 acc.size inv acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯

Tactic:
rw [Nat.zero_add] at inv

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
inv✝ : 0 + acc.size = l.length
inv : acc.size = l.length
⊢ Array.mapFinIdxM.map l.toArray f 0 acc.size inv✝ acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ acc.size < l.length

Tactic:
omega

Result:
no goals

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
x : β
⊢ Array.mapFinIdxM.map l.toArray f k (acc.push x).size ⋯ (acc.push x) =
    toArray <$> mapFinIdxM.go l f (drop (acc.push x).size l) (acc.push x) ⋯

Tactic:
refine go k (acc.push x) _

Result:
no goals