Let X, d, x and U be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HU: U ∈ metric_topology X d.
Assume HxU: x ∈ U.
Set B0 to be the term famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hdef: metric_topology X d = generated_topology X B0.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B0.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUcond: ∀y ∈ U, ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y : set, y ∈ U0 → ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb0: ∃b0 ∈ B0, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUcond x HxU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B0: b0 ∈ B0.
An exact proof term for the current goal is (andEL (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxinb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
We prove the intermediate claim Hb0sub: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
Apply (famunionE_impred X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}) b0 Hb0B0 (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b0 Hb0In (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d c r0.
We prove the intermediate claim HxinBall: x ∈ open_ball X d c r0.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxinb0.
We prove the intermediate claim HballsubU: open_ball X d c r0 ⊆ U.
We will prove open_ball X d c r0 ⊆ U.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hb0sub.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (open_ball_refine_center X d c x r0 Hm HcX HxX Hr0R Hr0pos HxinBall).
Apply Hexs to the current goal.
Let s be given.
Assume Hs.
We prove the intermediate claim Hs12: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim HsubBall: open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsubU: open_ball X d x s ⊆ U.
An exact proof term for the current goal is (Subq_tra (open_ball X d x s) (open_ball X d c r0) U HsubBall HballsubU).
We use s to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HsR.
Apply andI to the current goal.
An exact proof term for the current goal is Hspos.
An exact proof term for the current goal is HsubU.
∎