## Stream: new members

### Topic: simp and do notation

#### Miguel Negrão (Apr 01 2023 at 15:53):

Hi again,

Sometimes after calling simp the result is in do notation. At least for me, this make is it a bit more difficult to visualize what I need to prove. Is there a way to force simp not to display do notation and show me instead >>= and lambdas ?

#### Kevin Buzzard (Apr 01 2023 at 20:13):

Can you give a #mwe ?

#### Miguel Negrão (Apr 03 2023 at 10:48):

I think the do notation appeared in my goal from a function definition. So let's say what we are trying to prove is in do notation, but during proof, we would like to change into desugared form, to make it easier to see which theorems apply, how would one do that ? A very simple mwe below.

universe u v w
variable {m : Type u → Type v} [Monad m] [LawfulMonad m]
variable {α β γ : Type u}
theorem map_bind2 (x : m α) {g : α → m β} {f : β → γ} :
f <$> (x >>= g) = (do let a <- x f <$> g a) := by
_

unsolved goals
m: Type u → Type v
x: m α
g: α → m β
f: β → γ
⊢ f <$> (x >>= g) = do let a ← x f <$> g a


#### Alex J. Best (Apr 03 2023 at 11:10):

Does

attribute [-delab] Lean.PrettyPrinter.Delaborator.delabDo


do what you want?

#### Eric Wieser (Apr 03 2023 at 11:12):

What import does that need, Alex?

#### Eric Wieser (Apr 03 2023 at 11:12):

docs4#Lean.PrettyPrinter.Delaborator.delabDo

#### Alex J. Best (Apr 03 2023 at 11:12):

I would think nothing?

#### Eric Wieser (Apr 03 2023 at 11:13):

It doesn't work for me without import Lean.PrettyPrinter.Delaborator.Builtins

#### Alex J. Best (Apr 03 2023 at 11:14):

Hmm interesting, not sure I understand how that works to be honest

#### Eric Wieser (Apr 03 2023 at 11:15):

I think it's because it's builtin

#### Miguel Negrão (Apr 03 2023 at 11:23):

Alex J. Best disse:

Does

attribute [-delab] Lean.PrettyPrinter.Delaborator.delabDo


do what you want?

Yup, that does the trick !!! Great ! Indeed l report the same as @Eric Wieser , I need that import to make it work. Thanks all !

#### Eric Wieser (Apr 03 2023 at 11:24):

FWIW, I was able to prove your lemma with simp only [map_eq_pure_bind, bind_assoc]

#### Miguel Negrão (Apr 03 2023 at 11:28):

Thanks, but my example is from mathlib4. Just needed something to illustrate the point. :-)

theorem map_bind (x : m α) {g : α → m β} {f : β → γ} :
f <$> (x >>= g) = x >>= fun a => f <$> g a := by
rw [← bind_pure_comp, bind_assoc] <;> simp [bind_pure_comp]


Last updated: Dec 20 2023 at 11:08 UTC