α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
revert arr
case nil
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) [] = SeqRight.seqRight (mapIdxM.go f [] arr) fun x => pure PUnit.unit

case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) (head :: tail) =
    SeqRight.seqRight (mapIdxM.go f (head :: tail) arr) fun x => pure PUnit.unit
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
induction' as with head tail ih <;> intro arr
no goals
case nil
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) [] = SeqRight.seqRight (mapIdxM.go f [] arr) fun x => pure PUnit.unit
simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ (do
      f (Array.size arr) head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← f (Array.size arr) head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) (head :: tail) =
    SeqRight.seqRight (mapIdxM.go f (head :: tail) arr) fun x => pure PUnit.unit
simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind, bind_pure_unit,
  LawfulMonad.bind_assoc, pure_bind, mapIdxM.go, seq_pure]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ (do
      f (Array.size arr) head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← f (Array.size arr) head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
generalize (f (Array.size arr) head) = head
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
let arr_1 := arr.push ⟨⟩
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
have : arr_1.size = arr.size + 1 := Array.size_push arr ⟨⟩
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      SeqRight.seqRight (mapIdxM.go f tail arr_1) fun x => pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
rw [← this, ih arr_1]
no goals
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      SeqRight.seqRight (mapIdxM.go f tail arr_1) fun x => pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]