-- Mathlib/Data/List/Indexes.lean
theorem mapIdxMGo_eq_mapIdxMAuxSpec
    [LawfulMonad m] {β} (f : ℕ → α → m β) (arr : Array β) (as : List α) :
    mapIdxM.go f as arr = (arr.toList ++ ·) <$> mapIdxMAuxSpec f arr.size as

Proof state:
case e_a
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ (fun __do_lift => mapIdxM.go f tail (arr.push __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Tactic:
conv => { lhs; intro x; rw [ih _ _ h]; }

Result:
case e_a
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ (fun x => (fun x_1 => (arr.push x).toList ++ x_1) <$> mapIdxMAuxSpec f (arr.push x).size tail) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Proof state:
case succ
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
h : as.length = len + 1
⊢ mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

Tactic:
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.push_toList, append_assoc, singleton_append, Array.size_push,
    map_eq_pure_bind]

Result:
no goals

Proof state:
case e_a
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ (fun x => (fun x_1 => (arr.push x).toList ++ x_1) <$> mapIdxMAuxSpec f (arr.push x).size tail) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Tactic:
funext x

Result:
case e_a.h
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
x : β
⊢ (fun x_1 => (arr.push x).toList ++ x_1) <$> mapIdxMAuxSpec f (arr.push x).size tail = do
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Proof state:
case zero
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : as.length = 0
this : as = []
⊢ mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

Tactic:
simp only [this, mapIdxM.go, mapIdxMAuxSpec, enumFrom_nil, List.traverse, map_pure, append_nil]

Result:
no goals

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
h : [].length = len + 1
⊢ mapIdxM.go f [] arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size []

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
⊢ mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

Tactic:
generalize e : as.length = len

Result:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
len : ℕ
e : as.length = len
⊢ mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

Proof state:
case cons
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = 0
⊢ head✝ :: tail✝ = []

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
len : ℕ
e : as.length = len
⊢ mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

Tactic:
revert as arr

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

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : (head :: tail).length = len + 1
⊢ mapIdxM.go f (head :: tail) arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size (head :: tail)

Tactic:
simp only [length_cons, Nat.succ.injEq] at h

Result:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
⊢ mapIdxM.go f (head :: tail) arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size (head :: tail)

Proof state:
case e_a.h
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as
arr : Array β
as : List α
head : α
tail : List α
h : tail.length = len
x : β
⊢ (fun x_1 => (arr.push x).toList ++ x_1) <$> mapIdxMAuxSpec f (arr.push x).size tail = do
    let x_1 ← mapIdxMAuxSpec f (arr.size + 1) tail
    pure (arr.toList ++ x :: x_1)

Tactic:
simp only [Array.push_toList, append_assoc, singleton_append, Array.size_push,
  map_eq_pure_bind]

Result:
no goals

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
len : ℕ
⊢ ∀ (arr : Array β) (as : List α),
    as.length = len → mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

Tactic:
induction' len with len ih <;> intro arr as h

Result:
case zero
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : as.length = 0
⊢ mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

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