Disjoint Sets proof

Stream: mathlib4

[Rosie Baish]

I'm trying to do a proof on Partial Functions who's domains are disjoint.
I'm proving that p1 ∪ p2 = p2 ∪ p1 if p1 and p2 have disjoint domains.
I'm attempting to do it by cases, with the 4 options being both combinations of x being in and not in the domain of each of p1 and p2. The case where x is in the domain of p1 and p2 means they're not disjoint, which is a contradiction.
The problem is I can't work out how to demonstrate that contradiction.
I've got to disjoint_proof: ∀ ⦃a : A⦄, a ∈ PFun.Dom p1 → ¬a ∈ PFun.Dom p2 and x: A, but I can't work out how to instantiate the forall with the value of x I want. The double-braces are messing me up and I don't know how to handle them.
Can anyone offer any advice, or point me in the direction of what tactics I need?

Thanks, Rosie

[Eric Wieser]

Can you post a #mwe?

[Eric Wieser]

have := @disjoint_proof x should solve your immediate issue

[Yaël Dillies]

Hi Rosie! Nice seeing you here.

[Yaël Dillies]

The answer is that those double curly braces are semi-implicit argument. They behave like explicit arguments (they don't get instantiated by a metavariable when they're the outer binder) until a later argument is provided (and there they behave as if they were implicit). So here the next argument disjoint_proof expects is a in PFun.Dom p1, not a (and Lean will figure out what a is from the a in PFun.Dom p1 argument).