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

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ mapM f (cons a x) = do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Tactic:
unfold mapM
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ mapM.map f (cons a x) 0 (mkEmpty (size (cons a x))) = do
    let b ← f a
    let y ← mapM.map f 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
f : α → m β
a : α
x : Array α
⊢ mapM.map f (cons a x) 0 (mkEmpty (size (cons a x))) = do
    let b ← f a
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold mapM.map; simp only [size_cons]
  rw [dif_pos x.size.zero_lt_succ]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
⊢ (do
      let __do_lift ← f (cons a x)[0]
      mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) __do_lift)) =
    do
    let b ← f a
    let y ← mapM.map f 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
f : α → m β
a : α
x : Array α
⊢ (do
      let __do_lift ← f (cons a x)[0]
      mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) __do_lift)) =
    do
    let b ← f a
    let y ← mapM.map f 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
f : α → m β
a : α
x : Array α
⊢ ∀ (a_1 : β),
    mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) a_1) = do
      let y ← mapM.map f 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
f : α → m β
a : α
x : Array α
⊢ ∀ (a_1 : β),
    mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) a_1) = do
      let y ← mapM.map f 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
f : α → m β
a : α
x : Array α
b : β
⊢ mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) b) = do
    let y ← mapM.map f 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
f : α → m β
a : α
x : Array α
b : β
⊢ mapM.map f (cons a x) (0 + 1) (push (mkEmpty (Nat.succ (size x))) b) = do
    let y ← mapM.map f x 0 (mkEmpty (size x))
    pure (cons b y)
Tactic:
exact mapM.map_cons_succ f a x 0 b #[]
State after:
no goals