! vs Bool.not

Stream: mathlib4

[Bolton Bailey]

The first two are two implementations for what I thought would be the same lemma. But changing between them breaks the last lemma. What is the difference here?

import Mathlib.Data.Option.Basic

lemma bnot_isSome (a : Option α) : ! a.isSome = a.isNone := by
  funext
  cases a <;> simp

lemma bnot_isSome' (a : Option α) : a.isSome.not = a.isNone := by
  funext
  cases a <;> simp

@[simp]
lemma not_comp_isSome : Bool.not ∘ @Option.isSome α = Option.isNone := by
  funext
  simp [bnot_isSome] -- unsolved goals
  -- simp [bnot_isSome'] -- succeeds

[Yaël Dillies]

Are you sure ! a.isSome = a.isNone isn't getting parsed as ! (a.isSome = a.isNone)?

[Bolton Bailey]

Never mind, I'm dumb and don't know how tightly ! binds yes

[Kevin Buzzard]

I unfortunately don't have time to dig up the post where I made precisely the same mistake a year or so ago :-)