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

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      let y ← mapM f #[]
      pure (cons b y)) =
    do
    let y ← mapM f #[]
    let b ← f a
    pure (push y b)
Tactic:
simp only [mapM_empty, pure_bind]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      pure (cons b #[])) =
    do
    let b ← f a
    pure (push #[] b)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      pure (cons b #[])) =
    do
    let b ← f a
    pure (push #[] b)
Tactic:
rfl
State after:
no goals

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
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:
show mapM f (cons a (push x _)) = _
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (cons a (push x a✝)) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ mapM f (cons a (push x a✝)) = do
    let y ← mapM f (cons a x)
    let b ← f a✝
    pure (push y b)
Tactic:
simp only [mapM_cons f, bind_assoc]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ (do
      let b ← f a
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f a
    let x ← mapM f x
    let y ← pure (cons x_1 x)
    let b ← f a✝
    pure (push y b)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ (do
      let b ← f a
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x_1 ← f a
    let x ← mapM f x
    let y ← pure (cons x_1 x)
    let b ← f a✝
    pure (push y b)
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 β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ ∀ (a : β),
    (do
        let y ← mapM f (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapM f x
      let y ← pure (cons a x)
      let b ← f a✝
      pure (push y b)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
⊢ ∀ (a : β),
    (do
        let y ← mapM f (push x a✝)
        pure (cons a y)) =
      do
      let x ← mapM f x
      let y ← pure (cons a x)
      let b ← f a✝
      pure (push y b)
Tactic:
intro b
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ← mapM f (push x a✝)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)
Tactic:
rw [IH]
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ←
        do
          let y ← mapM f x
          let b ← f a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let y ←
        do
          let y ← mapM f x
          let b ← f a✝
          pure (push y b)
      pure (cons b y)) =
    do
    let x ← mapM f x
    let y ← pure (cons b x)
    let b ← f a✝
    pure (push y b)
Tactic:
simp only [bind_assoc, pure_bind]
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let x ← mapM f x
      let x_1 ← f a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapM f x
    let b_1 ← f a✝
    pure (push (cons b x) b_1)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝ : Array α
a✝ a : α
x : Array α
IH :
  mapM f (push x a✝) = do
    let y ← mapM f x
    let b ← f a✝
    pure (push y b)
b : β
⊢ (do
      let x ← mapM f x
      let x_1 ← f a✝
      pure (cons b (push x x_1))) =
    do
    let x ← mapM f x
    let b_1 ← f a✝
    pure (push (cons b x) b_1)
Tactic:
rfl
State after:
no goals