Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ famunion EuclidPlane (λc : set ⇒ {open_ball EuclidPlane EuclidPlane_metric c r|r ∈ R, Rlt 0 r}).
We will prove U ∈ circular_regions.
Apply (famunionE_impred EuclidPlane (λc0 : set ⇒ {open_ball EuclidPlane EuclidPlane_metric c0 r|r ∈ R, Rlt 0 r}) U HU (U ∈ circular_regions)) to the current goal.
Let c be given.
Assume Hc: c ∈ EuclidPlane.
Assume HUIn: U ∈ {open_ball EuclidPlane EuclidPlane_metric c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball EuclidPlane EuclidPlane_metric c r0) U HUIn (U ∈ circular_regions)) to the current goal.
Let r be given.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume HUeq: U = open_ball EuclidPlane EuclidPlane_metric c r.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (open_ball_EuclidPlane_metric_in_circular_regions c r Hc HrR Hrpos).
Let U be given.
Assume HU: U ∈ circular_regions.
We will prove U ∈ famunion EuclidPlane (λc0 : set ⇒ {open_ball EuclidPlane EuclidPlane_metric c0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HUdesc: ∃c : set, ∃r : set, c ∈ EuclidPlane ∧ Rlt 0 r ∧ U = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}.
An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∃c0 : set, ∃r0 : set, c0 ∈ EuclidPlane ∧ Rlt 0 r0 ∧ U0 = {p ∈ EuclidPlane|Rlt (distance_R2 p c0) r0}) U HU).
Apply HUdesc to the current goal.
Let c be given.
Assume HrEx: ∃r : set, c ∈ EuclidPlane ∧ Rlt 0 r ∧ U = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}.
Apply HrEx to the current goal.
Let r be given.
Assume Hcore: c ∈ EuclidPlane ∧ Rlt 0 r ∧ U = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}.
We prove the intermediate claim Hcr: c ∈ EuclidPlane ∧ Rlt 0 r.
An exact proof term for the current goal is (andEL (c ∈ EuclidPlane ∧ Rlt 0 r) (U = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}) Hcore).
We prove the intermediate claim HUeq0: U = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}.
An exact proof term for the current goal is (andER (c ∈ EuclidPlane ∧ Rlt 0 r) (U = {p ∈ EuclidPlane|Rlt (distance_R2 p c) r}) Hcore).
We prove the intermediate claim Hc: c ∈ EuclidPlane.
An exact proof term for the current goal is (andEL (c ∈ EuclidPlane) (Rlt 0 r) Hcr).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andER (c ∈ EuclidPlane) (Rlt 0 r) Hcr).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (RltE_right 0 r Hrpos).
We prove the intermediate claim HUeqBall: U = open_ball EuclidPlane EuclidPlane_metric c r.
rewrite the current goal using HUeq0 (from left to right).
rewrite the current goal using (open_ball_EuclidPlane_metric_eq c r Hc) (from right to left).
Use reflexivity.
We prove the intermediate claim HballIn: open_ball EuclidPlane EuclidPlane_metric c r ∈ {open_ball EuclidPlane EuclidPlane_metric c rr|rr ∈ R, Rlt 0 rr}.
An exact proof term for the current goal is (ReplSepI R (λrr : set ⇒ Rlt 0 rr) (λrr : set ⇒ open_ball EuclidPlane EuclidPlane_metric c rr) r HrR Hrpos).
We prove the intermediate claim HUIn: U ∈ {open_ball EuclidPlane EuclidPlane_metric c rr|rr ∈ R, Rlt 0 rr}.
rewrite the current goal using HUeqBall (from left to right).
An exact proof term for the current goal is HballIn.
An exact proof term for the current goal is (famunionI EuclidPlane (λc0 : set ⇒ {open_ball EuclidPlane EuclidPlane_metric c0 rr|rr ∈ R, Rlt 0 rr}) c U Hc HUIn).
∎