-- Mathlib/Data/List/Indexes.lean
theorem mapIdxMAux'_eq_mapIdxMGo {α} (f : ℕ → α → m PUnit) (as : List α) (arr : Array PUnit) :
    mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Proof state:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
⊢ (do
      f arr.size head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← f arr.size head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Tactic:
generalize (f (Array.size arr) head) = head

Result:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
head : m PUnit.{u + 1}
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Proof state:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
as : List α
arr : Array PUnit.{u + 1}
⊢ mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Tactic:
revert arr

Result:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
as : List α
⊢ ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Proof state:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
head : m PUnit.{u + 1}
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Tactic:
have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push arr ⟨⟩

Result:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
head : m PUnit.{u + 1}
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Proof state:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
⊢ mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit

Tactic:
simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind, bind_pure_unit,
  LawfulMonad.bind_assoc, pure_bind, mapIdxM.go, seq_pure]

Result:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
⊢ (do
      f arr.size head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← f arr.size head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Proof state:
case nil
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
arr : Array PUnit.{u + 1}
⊢ mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit

Tactic:
simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]

Result:
no goals

Proof state:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
head : m PUnit.{u + 1}
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxMAux' f (arr.size + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Tactic:
rw [← this, ih]

Result:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
head : m PUnit.{u + 1}
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Proof state:
case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head✝ : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
head : m PUnit.{u + 1}
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit.{u + 1}) id x PUnit.unit)

Tactic:
simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]

Result:
no goals

Proof state:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
as : List α
⊢ ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Tactic:
induction' as with head tail ih <;> intro arr

Result:
case nil
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
arr : Array PUnit.{u + 1}
⊢ mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit

case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit.{u + 1}
head : α
tail : List α
ih : ∀ (arr : Array PUnit.{u + 1}), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit.{u + 1}
⊢ mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit