Theorem: Array.mapIdxM_cons (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ mapIdxM (cons a x) f = do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM x (f ∘ Fin.succ)
    pure (cons b y)
Tactic:
unfold mapIdxM
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ mapIdxM.map (cons a x) f (size (cons a x)) 0 (_ : size (cons a x) + 0 = size (cons a x) + 0)
      (mkEmpty (size (cons a x))) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ mapIdxM.map (cons a x) f (size (cons a x)) 0 (_ : size (cons a x) + 0 = size (cons a x) + 0)
      (mkEmpty (size (cons a x))) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
conv => lhs; unfold mapIdxM.map; dsimp [cons]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ (match size { data := a :: x.data }, (_ : size { data := a :: x.data } + 0 = size { data := a :: x.data } + 0) with
    | 0, x => pure #[]
    | Nat.succ i, inv => do
      let __do_lift ← f 0 { data := a :: x.data }[0]
      mapIdxM.map { data := a :: x.data } f i (0 + 1) (_ : i + (0 + 1) = size { data := a :: x.data })
          (push #[] __do_lift)) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ (match size { data := a :: x.data }, (_ : size { data := a :: x.data } + 0 = size { data := a :: x.data } + 0) with
    | 0, x => pure #[]
    | Nat.succ i, inv => do
      let __do_lift ← f 0 { data := a :: x.data }[0]
      mapIdxM.map { data := a :: x.data } f i (0 + 1) (_ : i + (0 + 1) = size { data := a :: x.data })
          (push #[] __do_lift)) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
apply bind_congr
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
        (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] a_1) =
      do
      let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
      pure (cons a_1 y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
        (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] a_1) =
      do
      let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
      pure (cons a_1 y)
Tactic:
intro b
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
      (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] b) =
    do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
      (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] b) =
    do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
show mapIdxM.map (cons a x) f x.size 1 rfl #[b] = _
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map (cons a x) f (size x) 1 (_ : size x + 1 = size x + 1) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map (cons a x) f (size x) 1 (_ : size x + 1 = size x + 1) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
rw [mapIdxM.map_cons]
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
generalize f ∘ Fin.succ = f'
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
clear f
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x) #[b] = do
    let y ← mapIdxM.map x f' (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
Tactic:
suffices ∀ (i j) (h : i + j = x.size) (y : Array β), mapIdxM.map x f' i j h (cons b y) = (mapIdxM.map x f' i j h y >>= λ y => pure (cons b y))
from this x.size 0 rfl #[]
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ ∀ (i j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
⊢ ∀ (i j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
Tactic:
intro i j h y
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i j : Nat
h : i + j = size x
y : Array β
⊢ mapIdxM.map x f' i j h (cons b y) = do
    let y ← mapIdxM.map x f' i j h y
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i j : Nat
h : i + j = size x
y : Array β
⊢ mapIdxM.map x f' i j h (cons b y) = do
    let y ← mapIdxM.map x f' i j h y
    pure (cons b y)
Tactic:
induction i generalizing j y with
| zero => dsimp [mapIdxM.map]; rw [pure_bind]
| succ i IH =>
  dsimp [mapIdxM.map]; simp only [bind_assoc]
  apply bind_congr; intro b'
  dsimp [push, cons, List.concat]
  exact IH ..
State after:
no goals

State before:
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ mapIdxM.map x f' Nat.zero j h (cons b y) = do
    let y ← mapIdxM.map x f' Nat.zero j h y
    pure (cons b y)
Tactic:
dsimp [mapIdxM.map]
State after:
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)

State before:
case h.zero
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
j : Nat
h : Nat.zero + j = size x
y : Array β
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
Tactic:
rw [pure_bind]
State after:
no goals

State before:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ mapIdxM.map x f' (Nat.succ i) j h (cons b y) = do
    let y ← mapIdxM.map x f' (Nat.succ i) j h y
    pure (cons b y)
Tactic:
dsimp [mapIdxM.map]
State after:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
        mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y __do_lift)
    pure (cons b y)

State before:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
        mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y __do_lift)
    pure (cons b y)
Tactic:
simp only [bind_assoc]
State after:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f' { val := j, isLt := (_ : j < size x) } x[j]
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y x_1)
    pure (cons b y)

State before:
case h.succ
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ (do
      let __do_lift ← f' { val := j, isLt := (_ : j < size x) } x[j]
      mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f' { val := j, isLt := (_ : j < size x) } x[j]
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y x_1)
    pure (cons b y)
Tactic:
apply bind_congr
State after:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ ∀ (a : β),
    mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) a) = do
      let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y a)
      pure (cons b y)

State before:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
⊢ ∀ (a : β),
    mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) a) = do
      let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y a)
      pure (cons b y)
Tactic:
intro b'
State after:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) b') = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y b')
    pure (cons b y)

State before:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push (cons b y) b') = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) (push y b')
    pure (cons b y)
Tactic:
dsimp [push, cons, List.concat]
State after:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := b :: List.concat y.data b' } = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := List.concat y.data b' }
    pure { data := b :: y.data }

State before:
case h.succ.h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + j = size x) (y : Array β),
    mapIdxM.map x f' i j h (cons b y) = do
      let y ← mapIdxM.map x f' i j h y
      pure (cons b y)
j : Nat
h : Nat.succ i + j = size x
y : Array β
b' : β
⊢ mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := b :: List.concat y.data b' } = do
    let y ← mapIdxM.map x f' i (j + 1) (_ : i + (j + 1) = size x) { data := List.concat y.data b' }
    pure { data := b :: y.data }
Tactic:
exact IH ..
State after:
no goals