Theorem: Array.mapIdxM.map_cons (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i j : Nat
h : i + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
Tactic:
induction i generalizing j y with
| zero => dsimp [map]
| succ i IH =>
  unfold map; dsimp
  apply bind_congr; intro b
  exact IH (j+1) _ (push y b)
State after:
no goals

State before:
case zero
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
j : Nat
h : Nat.zero + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f Nat.zero (j + 1) h y = map x (f ∘ Fin.succ) Nat.zero j (_ : Nat.zero + j = size x) y
Tactic:
dsimp [map]
State after:
no goals

State before:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f (Nat.succ i) (j + 1) h y = map x (f ∘ Fin.succ) (Nat.succ i) j (_ : Nat.succ i + j = size x) y
Tactic:
unfold map
State after:
case succ
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
⊢ (let_fun this := (_ : j + 1 < size (cons a x));
    let idx := { val := j + 1, isLt := this };
    let_fun this := (_ : i + (j + 1 + 1) = size (cons a x));
    do
    let __do_lift ← f idx (get (cons a x) idx)
    map (cons a x) f i (j + 1 + 1) this (push y __do_lift)) =
    let_fun this := (_ : j < size x);
    let idx := { val := j, isLt := this };
    let_fun this := (_ : i + (j + 1) = size x);
    do
    let __do_lift ← (f ∘ Fin.succ) idx (get x idx)
    map x (f ∘ Fin.succ) i (j + 1) this (push y __do_lift)

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

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

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

State before:
case succ.h
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (j : Nat) (h : i + (j + 1) = size x + 1) (y : Array β),
    map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
b : β
⊢ map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y b) =
    map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y b)
Tactic:
exact IH (j+1) _ (push y b)
State after:
no goals