-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
    (id_map : ∀ {α} (x : m α), id <$> x = x)
    (pure_bind : ∀ {α β} (x : α) (f : α → m β), pure x >>= f = f x)
    (bind_assoc : ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ),
      x >>= f >>= g = x >>= fun x => f x >>= g)
    (map_const : ∀ {α β} (x : α) (y : m β),
      Functor.mapConst x y = Function.const β x <$> y

Proof state:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
⊢ ∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g

Tactic:
intros

Result:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
α✝ β✝ : Type u
g✝ : m (α✝ → β✝)
x✝ : α✝
⊢ g✝ <*> pure x✝ = (fun h => h x✝) <$> g✝

Proof state:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
α β : Type u
g : α → β
x : α
⊢ g <$> pure x = pure (g x)

Tactic:
rw [← bind_pure_comp]

Result:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
α β : Type u
g : α → β
x : α
⊢ (do
      let y ← pure x
      pure (g y)) =
    pure (g x)

Proof state:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
⊢ ∀ {α β : Type u} (x : m α) (y : m β), x <* y = const β <$> x <*> y

Tactic:
simp [seqLeft_eq, ← bind_map, ← bind_pure_comp, pure_bind, bind_assoc]

Result:
no goals