Let p be given.

Assume Hp: p ∈ W.

We will prove ∃b ∈ product_subbasis Y Ty Y Ty, p ∈ b ∧ b ⊆ W.

We prove the intermediate claim HpDom: p ∈ setprod Y Y.

An exact proof term for the current goal is (SepE1 (setprod Y Y) (λq : set ⇒ apply_fun d q ∈ open_ray_upper R a) p Hp).

We prove the intermediate claim Hp0Y: p 0 ∈ Y.

An exact proof term for the current goal is (ap0_Sigma Y (λ_ : set ⇒ Y) p HpDom).

We prove the intermediate claim Hp1Y: p 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma Y (λ_ : set ⇒ Y) p HpDom).

We prove the intermediate claim Hm: metric_on Y d.

An exact proof term for the current goal is (metric_on_total_imp_metric_on Y d Hd).

We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ Rlt 0 r ∧ rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) ⊆ W.

An exact proof term for the current goal is (metric_distance_above_has_product_ball Y d a p Hd HaR Hp).

Apply Hexr to the current goal.

Let r be given.

Assume Hr.

We prove the intermediate claim HrPack: (r ∈ R ∧ Rlt 0 r) ∧ rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) ⊆ W.

An exact proof term for the current goal is Hr.

We prove the intermediate claim Hr1: r ∈ R ∧ Rlt 0 r.

An exact proof term for the current goal is (andEL (r ∈ R ∧ Rlt 0 r) (rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) ⊆ W) HrPack).

We prove the intermediate claim HrR: r ∈ R.

An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r) Hr1).

We prove the intermediate claim HrPos: Rlt 0 r.

An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r) Hr1).

We prove the intermediate claim Hbsub: rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) ⊆ W.

An exact proof term for the current goal is (andER (r ∈ R ∧ Rlt 0 r) (rectangle_set (open_ball Y d (p 0) r) (open_ball Y d (p 1) r) ⊆ W) HrPack).

Set U to be the term open_ball Y d (p 0) r.

Set V to be the term open_ball Y d (p 1) r.

Set b to be the term rectangle_set U V.

We use b to witness the existential quantifier.

Apply andI to the current goal.

We will prove b ∈ product_subbasis Y Ty Y Ty.

We will prove b ∈ ⋃_{U0 ∈ Ty}{rectangle_set U0 V0|V0 ∈ Ty}.

We prove the intermediate claim HUinTy: U ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y d (p 0) r Hm Hp0Y HrPos).

We prove the intermediate claim HVinTy: V ∈ Ty.

An exact proof term for the current goal is (open_ball_in_metric_topology Y d (p 1) r Hm Hp1Y HrPos).

We prove the intermediate claim HbInFam: b ∈ {rectangle_set U V0|V0 ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set U V0) V HVinTy).

An exact proof term for the current goal is (famunionI Ty (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) U b HUinTy HbInFam).

Apply andI to the current goal.

We will prove p ∈ b.

We prove the intermediate claim HbEq0: b = rectangle_set U V.

Use reflexivity.

rewrite the current goal using HbEq0 (from left to right).

rewrite the current goal using rectangle_set_def (from left to right).

We prove the intermediate claim HpEta0: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta Y Y p HpDom).

rewrite the current goal using HpEta0 (from left to right) at position 1.

We prove the intermediate claim Hp0In: p 0 ∈ U.

An exact proof term for the current goal is (center_in_open_ball Y d (p 0) r Hm Hp0Y HrPos).

We prove the intermediate claim Hp1In: p 1 ∈ V.

An exact proof term for the current goal is (center_in_open_ball Y d (p 1) r Hm Hp1Y HrPos).

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U V (p 0) (p 1) Hp0In Hp1In).

We will prove b ⊆ W.

We prove the intermediate claim HbEq: b = rectangle_set U V.

Use reflexivity.

rewrite the current goal using HbEq (from left to right).

An exact proof term for the current goal is Hbsub.