simp without unpacking my own definitions

Stream: lean4

[Connor Gordon]

I've been working on a proof that requires me to define a function B₀, and then I proved a convenience lemma about B₀ so I can use its properties without having to refer to its definition down the line. I'm now trying to use it to prove something else, and I've narrowed my goal down to something that should be fairly easy to do with simp and a little extra. In particular I have in the context

hx: x ∈ ⋃ (C : Set α) (_ : C ∈ F ∪ {V n, W n}), B₀ n C
⊢ x ∈ ⋃ (C : Set α) (_ : C ∈ F ∪ {V n, W n}), (fun C => ⋃ (n : ℕ), B₀ n C) C

I would like to use simp to simplify what it means to be in this union and also the fun C => blah to simply ⋃ (n : ℕ), B₀ n C, but whenever I do so, it also unpacks the definition of B₀, making things borderline unreadable. Is there any way to use simp that won't unpack the definition of B₀?

For convenience, here's a MWE in Lem1.lean, with the relevant sorry identified.