Mathlib irreducible_def vs @[irreducible] def: which unfolding tactics work

Tested on Lean/Mathlib v4.35.0 and v4.36.0-rc2 with irreducible_def foo : ℕ := 5 and @[irreducible] def bar : ℕ := 5. For irreducible_def, use rw [foo_def] (it generates foo_def : foo = 5) or simp [foo]. These all FAIL on it: rfl, with_unfolding_all rfl, delta foo; rfl, decide, and unfold foo, which leaves ⊢ wrapped✝.1 = 5 because the body sits behind an opaque wrapper, so no transparency setting reaches it. For @[irreducible] def, plain rfl and decide fail, but unfold bar; rfl, simp [bar], rw [bar], with_unfolding_all rfl, and unseal bar in before the declaration followed by rfl all work. So @[irreducible] is only a transparency hint, while irreducible_def is real opacity. Pick irreducible_def when you want downstream proofs to go through the _def lemma only, e.g. to stop defeq checks from unfolding a big body. Expect any rfl-based proof about it to need rewriting.