Let X, f, U and V be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f (U ∪ V).
We will prove x ∈ (preimage_of X f U) ∪ (preimage_of X f V).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ U ∪ V) x Hx).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∪ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ U ∪ V) x Hx).
Apply (binunionE U V (apply_fun f x) HfxUV) to the current goal.
Assume HfxU: apply_fun f x ∈ U.
We prove the intermediate claim HxPreU: x ∈ preimage_of X f U.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U) x HxX HfxU).
An exact proof term for the current goal is (binunionI1 (preimage_of X f U) (preimage_of X f V) x HxPreU).
Assume HfxV: apply_fun f x ∈ V.
We prove the intermediate claim HxPreV: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxX HfxV).
An exact proof term for the current goal is (binunionI2 (preimage_of X f U) (preimage_of X f V) x HxPreV).
Let x be given.
Assume Hx: x ∈ (preimage_of X f U) ∪ (preimage_of X f V).
We will prove x ∈ preimage_of X f (U ∪ V).
Apply (binunionE (preimage_of X f U) (preimage_of X f V) x Hx) to the current goal.
Assume HxPreU: x ∈ preimage_of X f U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ U) x HxPreU).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ U) x HxPreU).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∪ V.
An exact proof term for the current goal is (binunionI1 U V (apply_fun f x) HfxU).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U ∪ V) x HxX HfxUV).
Assume HxPreV: x ∈ preimage_of X f V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPreV).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPreV).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∪ V.
An exact proof term for the current goal is (binunionI2 U V (apply_fun f x) HfxV).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U ∪ V) x HxX HfxUV).
∎