Theorem: SizedArray.mapMIdx_push (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ mapMIdx f (push empty a) = do
    let y ← mapMIdx (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
unfold mapMIdx
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ mapMIdx.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let y ← mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty 0 (_ : 0 ≤ 0) (mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ mapMIdx.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let y ← mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty 0 (_ : 0 ≤ 0) (mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
unfold mapMIdx.loop
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (if h : 0 = 0 + 1 then pure (h ▸ mkEmpty (0 + 1))
    else
      let_fun this := (_ : 0 < 0 + 1);
      do
      let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ←
      if h : 0 = 0 then pure (h ▸ mkEmpty 0)
        else
          let_fun this := (_ : 0 < 0);
          do
          let __do_lift ←
            f { val := ↑{ val := 0, isLt := this }, isLt := (_ : ↑{ val := 0, isLt := this } < Nat.succ 0) } empty[0]
          let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
          mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty (0 + 1) this r
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (if h : 0 = 0 + 1 then pure (h ▸ mkEmpty (0 + 1))
    else
      let_fun this := (_ : 0 < 0 + 1);
      do
      let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ←
      if h : 0 = 0 then pure (h ▸ mkEmpty 0)
        else
          let_fun this := (_ : 0 < 0);
          do
          let __do_lift ←
            f { val := ↑{ val := 0, isLt := this }, isLt := (_ : ↑{ val := 0, isLt := this } < Nat.succ 0) } empty[0]
          let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
          mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty (0 + 1) this r
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
rw [dif_neg (c:=0=0+1) (by decide), dif_pos rfl]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (let_fun this := (_ : 0 < 0 + 1);
    do
    let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
    let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
    mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ← pure ((_ : 0 = 0) ▸ mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (let_fun this := (_ : 0 < 0 + 1);
    do
    let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
    let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
    mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ← pure ((_ : 0 = 0) ▸ mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
Tactic:
dsimp
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let y ← pure (mkEmpty 0)
    let b ← f 0 a
    pure (push y b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let y ← pure (mkEmpty 0)
    let b ← f 0 a
    pure (push y b)
Tactic:
rw [pure_bind]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f 0 a
    pure (push (mkEmpty 0) b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (do
      let __do_lift ← f 0 (push empty a)[0]
      mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f 0 a
    pure (push (mkEmpty 0) b)
Tactic:
apply bind_congr
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) a_1) = pure (push (mkEmpty 0) a_1)

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) a_1) = pure (push (mkEmpty 0) a_1)
Tactic:
intro b
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ mapMIdx.loop f (push empty a) (0 + 1) (_ : 0 < 0 + 1) (push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)
Tactic:
unfold mapMIdx.loop
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ (if h : 0 + 1 = 0 + 1 then pure (h ▸ push (mkEmpty (0 + 1)) b)
    else
      let_fun this := (_ : 0 + 1 < 0 + 1);
      do
      let __do_lift ← f { val := 0 + 1, isLt := this } (push empty a)[0 + 1]
      let r : SizedArray β (0 + 1 + 1) := push (push (mkEmpty (0 + 1)) b) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1 + 1) this r) =
    pure (push (mkEmpty 0) b)

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ (if h : 0 + 1 = 0 + 1 then pure (h ▸ push (mkEmpty (0 + 1)) b)
    else
      let_fun this := (_ : 0 + 1 < 0 + 1);
      do
      let __do_lift ← f { val := 0 + 1, isLt := this } (push empty a)[0 + 1]
      let r : SizedArray β (0 + 1 + 1) := push (push (mkEmpty (0 + 1)) b) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1 + 1) this r) =
    pure (push (mkEmpty 0) b)
Tactic:
rw [dif_pos rfl]
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ pure ((_ : 0 + 1 = 0 + 1) ▸ push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
b : β
⊢ pure ((_ : 0 + 1 = 0 + 1) ▸ push (mkEmpty (0 + 1)) b) = pure (push (mkEmpty 0) b)
Tactic:
rfl
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ ¬0 = 0 + 1
Tactic:
decide
State after:
no goals

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ mapMIdx f (push (cons a x) a✝) = do
    let y ← mapMIdx (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) (cons a x)
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (push y b)
Tactic:
simp only [push_cons_eq_cons_push, mapMIdx_cons, bind_assoc, pure_bind]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ (do
      let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (n✝ + 1)) } a
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f { val := 0, isLt := (_ : ↑{ val := 0, isLt := (_ : 0 < Nat.succ n✝) } < Nat.succ (n✝ + 1)) } a
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons x_1 (push x b))

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ (do
      let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (n✝ + 1)) } a
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f { val := 0, isLt := (_ : ↑{ val := 0, isLt := (_ : 0 < Nat.succ n✝) } < Nat.succ (n✝ + 1)) } a
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons x_1 (push x b))
Tactic:
apply bind_congr
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ ∀ (a : β),
    (do
        let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
      let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
      pure (cons a (push x b))

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
⊢ ∀ (a : β),
    (do
        let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
      let b ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
      pure (cons a (push x b))
Tactic:
intro b
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ← mapMIdx (f ∘ Fin.succ) (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Tactic:
rw [IH]
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ←
        do
          let y ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
          let b ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let y ←
        do
          let y ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
          let b ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Tactic:
simp only [bind_assoc, pure_bind]
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let x ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let x_1 ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  ∀ (x_1 : Fin (n✝ + 1) → α → m β),
    mapMIdx x_1 (push x a✝) = do
      let y ← mapMIdx (fun i => x_1 { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let b ← x_1 { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (push y b)
f : Fin (n✝ + 1 + 1) → α → m β
b : β
⊢ (do
      let x ← mapMIdx (fun i => (f ∘ Fin.succ) { val := ↑i, isLt := (_ : ↑i < Nat.succ n✝) }) x
      let x_1 ← (f ∘ Fin.succ) { val := n✝, isLt := (_ : n✝ < Nat.succ n✝) } a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapMIdx ((fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ (n✝ + 1)) }) ∘ Fin.succ) x
    let b_1 ← f { val := n✝ + 1, isLt := (_ : n✝ + 1 < Nat.succ (n✝ + 1)) } a✝
    pure (cons b (push x b_1))
Tactic:
rfl
State after:
no goals