α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
len : ℕ
e : length as = len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
generalize e : as.length = len
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
⊢ ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
len : ℕ
e : length as = len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
revert as arr
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as

case succ
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length as = Nat.succ len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
⊢ ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
induction' len with len ih <;> intro arr as h
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
this : as = []
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
have : as = [] := by cases as; rfl; contradiction
no goals
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
this : as = []
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
simp only [this, mapIdxM.go, mapIdxMAuxSpec, List.traverse, map_pure, append_nil]
case nil
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
h : length [] = Nat.zero
⊢ [] = []

case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ as = []
cases as
case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
case nil
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
h : length [] = Nat.zero
⊢ [] = []

case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
rfl
no goals
case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
contradiction
no goals
case succ
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length as = Nat.succ len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
match as with
| nil => contradiction
| cons head tail =>
  simp only [length_cons, Nat.succ.injEq] at h
  simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map,
    LawfulMonad.bind_assoc, pure_bind]
  congr
  conv => { lhs; intro x; rw [ih _ _ h]; }
  funext x
  simp only [Array.toList_eq, Array.push_data, append_assoc, singleton_append, Array.size_push,
    map_eq_pure_bind]
no goals
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length [] = Nat.succ len
⊢ mapIdxM.go f [] arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) []
contradiction
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length (head :: tail) = Nat.succ len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
simp only [length_cons, Nat.succ.injEq] at h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (do
      let __do_lift ← f (Array.size arr) head
      mapIdxM.go f tail (Array.push arr __do_lift)) =
    do
    let x ← f (Array.size arr) head
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map,
  LawfulMonad.bind_assoc, pure_bind]
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (do
      let __do_lift ← f (Array.size arr) head
      mapIdxM.go f tail (Array.push arr __do_lift)) =
    do
    let x ← f (Array.size arr) head
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
congr
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun x =>
      (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail) =
    fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
conv => { lhs; intro x; rw [ih _ _ h]; }
case e_a.h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
x : β
⊢ (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail = do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun x =>
      (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail) =
    fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
funext x
no goals
case e_a.h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
x : β
⊢ (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail = do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
simp only [Array.toList_eq, Array.push_data, append_assoc, singleton_append, Array.size_push,
  map_eq_pure_bind]