-- 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✝ : α✝
⊢ (do
      let x ← g✝
      x <$> pure x✝) =
    (fun h => h x✝) <$> g✝

Tactic:
simp [map_pure, bind_pure_comp]

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
x : m α✝
y : m β✝
⊢ (do
      let _ ← x
      y) =
    do
    let x ← x
    let x ← pure (const α✝ id x)
    x <$> y

Tactic:
simp [pure_bind, id_map]

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

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✝ : α✝ → β✝
x✝ : m α✝
⊢ (do
      let x ← pure g✝
      x <$> 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✝
α β : Type u
g : α → β
x : α
⊢ (do
      let y ← pure x
      pure (g y)) =
    pure (g x)

Tactic:
simp [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✝ : α✝ → β✝
x✝ : m α✝
⊢ (do
      let x ← pure g✝
      x <$> x✝) =
    g✝ <$> x✝

Tactic:
simp [pure_bind]

Result:
no goals