-- 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 : α → β) (x : m α), pure g <*> x = g <$> x

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✝ : α✝ → β✝
x✝ : m α✝
⊢ pure g✝ <*> x✝ = 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
g✝ : m (α✝ → β✝)
x✝ : α✝
⊢ g✝ <*> pure x✝ = (fun h => h x✝) <$> g✝

Tactic:
rw [← bind_map]

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✝ : α✝
⊢ (do
      let x ← g✝
      x <$> 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✝
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
⊢ ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x

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

Result:
no goals

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 : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
simp [← bind_pure_comp, bind_assoc, pure_bind]

Result:
no goals