Let X, d, U and x be given.
Assume Hm: metric_on X d.
Assume HUopen: open_in X (metric_topology X d) U.
Assume HxU: x ∈ U.
Set B to be the term famunion X (λx : set ⇒ {open_ball X d x r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (open_balls_form_basis X d Hm).
We prove the intermediate claim Hmtdef: metric_topology X d = generated_topology X B.
Use reflexivity.
We prove the intermediate claim HUtop: U ∈ metric_topology X d.
An exact proof term for the current goal is (andER (topology_on X (metric_topology X d)) (U ∈ metric_topology X d) HUopen).
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using Hmtdef (from right to left).
An exact proof term for the current goal is HUtop.
We prove the intermediate claim HUinChar: U ∈ {U0 ∈ 𝒫 X|∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0}.
rewrite the current goal using (lemma_generated_topology_characterization X B HBasis) (from right to left).
An exact proof term for the current goal is HUgen.
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HUinChar).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HUinChar).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUpow).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b HbB (∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hbin: b ∈ {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) b Hbin (∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ U)) to the current goal.
Let r be given.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hbeq: b = open_ball X d c r.
We prove the intermediate claim Hxball: x ∈ open_ball X d c r.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ open_ball X d c r.
An exact proof term for the current goal is (open_ball_refine_center_eps X d c x r Hm HcX HxX HrR Hrpos Hxball).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (open_ball X d x (eps_ N) ⊆ open_ball X d c r) HNpack).
We prove the intermediate claim HsubBall: open_ball X d x (eps_ N) ⊆ open_ball X d c r.
An exact proof term for the current goal is (andER (N ∈ ω) (open_ball X d x (eps_ N) ⊆ open_ball X d c r) HNpack).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNomega.
We prove the intermediate claim Hsubb: open_ball X d x (eps_ N) ⊆ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HsubBall.
An exact proof term for the current goal is (Subq_tra (open_ball X d x (eps_ N)) b U Hsubb HbsubU).
∎