Theorem: SizedArray.mapM_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 : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let y ← mapM f empty
    let b ← f a
    pure (push y b)
Tactic:
rw [mapM_empty, pure_bind]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let b ← f a
    pure (push empty b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM f (push empty a) = do
    let b ← f a
    pure (push empty b)
Tactic:
unfold mapM
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ mapM.loop f (push empty a) 0 (_ : 0 ≤ 0 + 1) (mkEmpty (0 + 1)) = do
    let b ← f a
    pure (push empty b)

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

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

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (if h : 0 < 0 + 1 then do
      let __do_lift ← f (push empty a)[0]
      if hlt : 0 + 1 < 0 + 1 then do
          let __do_lift_1 ← f (push empty a)[0 + 1]
          mapM.loop f (push empty a) (0 + 1 + 1) hlt (push (push (mkEmpty (0 + 1)) __do_lift) __do_lift_1)
        else
          let_fun this := (_ : 0 + 1 = 0 + 1);
          pure (this ▸ push (mkEmpty (0 + 1)) __do_lift)
    else
      let_fun this := (_ : 0 = 0 + 1);
      pure (this ▸ mkEmpty (0 + 1))) =
    do
    let b ← f a
    pure (push empty b)
Tactic:
simp only [(by decide : 0 < 0+1), (by decide : ¬ (0 + 1 < 0+1)), dif_pos, dif_neg]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (do
      let __do_lift ← f (push empty a)[0]
      pure (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f a
    pure (push empty b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x : SizedArray α n
a : α
⊢ (do
      let __do_lift ← f (push empty a)[0]
      pure (push (mkEmpty (0 + 1)) __do_lift)) =
    do
    let b ← f a
    pure (push empty 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 : α → m β
x : SizedArray α n
a : α
⊢ 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 : α → m β
x : SizedArray α n
a : α
⊢ ¬0 + 1 < 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 : α → m β
x✝ : SizedArray α n
a✝ : α
n✝ : Nat
a : α
x : SizedArray α n✝
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (push (cons a x) a✝) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)
Tactic:
simp only [push_cons_eq_cons_push, mapM_cons, bind_assoc, IH, pure_bind]
State after:
no goals