Apply andI to the current goal.

Let b be given.

Assume Hb: b ∈ B.

We will prove b ∈ 𝒫 X.

Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b Hb (b ∈ 𝒫 X)) to the current goal.

Let x0 be given.

Assume Hx0: x0 ∈ X.

Assume HbIn: b ∈ {open_ball X d x0 r|r ∈ R, Rlt 0 r}.

Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x0 r0) b HbIn (b ∈ 𝒫 X)) to the current goal.

Let r0 be given.

Assume Hr0R: r0 ∈ R.

Assume Hr0pos: Rlt 0 r0.

Assume Hbeq: b = open_ball X d x0 r0.

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

An exact proof term for the current goal is (open_ball_in_Power X d x0 r0).

Let x be given.

Assume Hx: x ∈ X.

We will prove ∃b ∈ B, x ∈ b.

We use (open_ball X d x 1) to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HballIn: open_ball X d x 1 ∈ {open_ball X d x r|r ∈ R, Rlt 0 r}.

An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x r0) 1 real_1 Rlt_0_1).

An exact proof term for the current goal is (famunionI X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) x (open_ball X d x 1) Hx HballIn).

An exact proof term for the current goal is (center_in_open_ball X d x 1 Hd Hx Rlt_0_1).

Let b1 be given.

Assume Hb1: b1 ∈ B.

Let b2 be given.

Assume Hb2: b2 ∈ B.

Let x be given.

Assume Hxb1: x ∈ b1.

Assume Hxb2: x ∈ b2.

We will prove ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.

Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b1 Hb1 (∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Let c1 be given.

Assume Hc1: c1 ∈ X.

Assume Hb1In: b1 ∈ {open_ball X d c1 r|r ∈ R, Rlt 0 r}.

Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c1 r0) b1 Hb1In (∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Let r1 be given.

Assume Hr1R: r1 ∈ R.

Assume Hr1pos: Rlt 0 r1.

Assume Hb1eq: b1 = open_ball X d c1 r1.

Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b2 Hb2 (∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Let c2 be given.

Assume Hc2: c2 ∈ X.

Assume Hb2In: b2 ∈ {open_ball X d c2 r|r ∈ R, Rlt 0 r}.

Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c2 r0) b2 Hb2In (∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.

Let r2 be given.

Assume Hr2R: r2 ∈ R.

Assume Hr2pos: Rlt 0 r2.

Assume Hb2eq: b2 = open_ball X d c2 r2.

We prove the intermediate claim Hxball1: x ∈ open_ball X d c1 r1.

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

An exact proof term for the current goal is Hxb1.

We prove the intermediate claim Hxball2: x ∈ open_ball X d c2 r2.

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

An exact proof term for the current goal is Hxb2.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ Rlt (apply_fun d (c1,y0)) r1) x Hxball1).

We prove the intermediate claim Hexr3: ∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ open_ball X d x r3 ⊆ (open_ball X d c1 r1) ∩ (open_ball X d c2 r2).

An exact proof term for the current goal is (open_ball_refine_intersection X d c1 c2 x r1 r2 Hd Hc1 Hc2 HxX Hr1R Hr2R Hr1pos Hr2pos Hxball1 Hxball2).

Apply Hexr3 to the current goal.

Let r3 be given.

Assume Hr3: r3 ∈ R ∧ Rlt 0 r3 ∧ open_ball X d x r3 ⊆ (open_ball X d c1 r1) ∩ (open_ball X d c2 r2).

We prove the intermediate claim Hr3left: r3 ∈ R ∧ Rlt 0 r3.

An exact proof term for the current goal is (andEL (r3 ∈ R ∧ Rlt 0 r3) (open_ball X d x r3 ⊆ (open_ball X d c1 r1) ∩ (open_ball X d c2 r2)) Hr3).

We prove the intermediate claim Hr3R: r3 ∈ R.

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

We prove the intermediate claim Hr3pos: Rlt 0 r3.

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

We prove the intermediate claim Hr3sub: open_ball X d x r3 ⊆ (open_ball X d c1 r1) ∩ (open_ball X d c2 r2).

An exact proof term for the current goal is (andER (r3 ∈ R ∧ Rlt 0 r3) (open_ball X d x r3 ⊆ (open_ball X d c1 r1) ∩ (open_ball X d c2 r2)) Hr3).

We use (open_ball X d x r3) to witness the existential quantifier.

We will prove open_ball X d x r3 ∈ B ∧ (x ∈ open_ball X d x r3 ∧ open_ball X d x r3 ⊆ b1 ∩ b2).

Apply andI to the current goal.

We prove the intermediate claim HballIn: open_ball X d x r3 ∈ {open_ball X d x r|r ∈ R, Rlt 0 r}.

An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x r0) r3 Hr3R Hr3pos).

An exact proof term for the current goal is (famunionI X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) x (open_ball X d x r3) HxX HballIn).

Apply andI to the current goal.

An exact proof term for the current goal is (center_in_open_ball X d x r3 Hd HxX Hr3pos).

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

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

An exact proof term for the current goal is Hr3sub.