[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α : Type u} (x : WriterT ω M α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [Functor.map, WriterT.mk]
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α β : Type u} (x : α) (f : α → WriterT ω M β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → WriterT ω M β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
simp [Bind.bind, Pure.pure, WriterT.mk]
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α β γ : Type u} (x : WriterT ω M α) (f : α → WriterT ω M β) (g : β → WriterT ω M γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝ : WriterT ω M α✝
f✝ : α✝ → WriterT ω M β✝
g✝ : β✝ → WriterT ω M γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
simp [Bind.bind, mul_assoc, WriterT.mk, ← bind_pure_comp]
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
⊢ ∀ {α β : Type u} (f : α → β) (x : WriterT ω M α),
    (do
        let y ← x
        pure (f y)) =
      f <$> x
[PROOFSTEP]
intros
[GOAL]
M : Type u → Type v
inst✝² : Monad M
ω α β : Type u
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : WriterT ω M α✝
⊢ (do
      let y ← x✝
      pure (f✝ y)) =
    f✝ <$> x✝
[PROOFSTEP]
simp [Bind.bind, Functor.map, Pure.pure, WriterT.mk, bind_pure_comp]
