Let X, d, x, U and a be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HU: U ∈ metric_topology X d.
Assume HxU: x ∈ U.
Assume HaR: a ∈ R.
Assume Ha0: Rlt 0 a.
We prove the intermediate claim Hexr0: ∃r0 : set, r0 ∈ R ∧ (Rlt 0 r0 ∧ open_ball X d x r0 ⊆ U).
An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball X d x U Hm HxX HU HxU).
Apply Hexr0 to the current goal.
Let r0 be given.
Assume Hr0pack: r0 ∈ R ∧ (Rlt 0 r0 ∧ open_ball X d x r0 ⊆ U).
We prove the intermediate claim Hr0R: r0 ∈ R.
An exact proof term for the current goal is (andEL (r0 ∈ R) (Rlt 0 r0 ∧ open_ball X d x r0 ⊆ U) Hr0pack).
We prove the intermediate claim Hr0pair: Rlt 0 r0 ∧ open_ball X d x r0 ⊆ U.
An exact proof term for the current goal is (andER (r0 ∈ R) (Rlt 0 r0 ∧ open_ball X d x r0 ⊆ U) Hr0pack).
We prove the intermediate claim Hr00: Rlt 0 r0.
An exact proof term for the current goal is (andEL (Rlt 0 r0) (open_ball X d x r0 ⊆ U) Hr0pair).
We prove the intermediate claim Hball0subU: open_ball X d x r0 ⊆ U.
An exact proof term for the current goal is (andER (Rlt 0 r0) (open_ball X d x r0 ⊆ U) Hr0pair).
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ Rlt 0 r ∧ Rlt r r0 ∧ Rlt r a.
An exact proof term for the current goal is (exists_eps_lt_two_pos_Euclid r0 a Hr0R HaR Hr00 Ha0).
Apply Hexr to the current goal.
Let r be given.
Assume Hr4.
We prove the intermediate claim HrR: r ∈ R.
Apply Hr4 to the current goal.
Assume H123 Hra.
Apply H123 to the current goal.
Assume H12 Hr2.
Apply H12 to the current goal.
Assume HrR Hr0.
An exact proof term for the current goal is HrR.
We prove the intermediate claim Hr0r0: Rlt 0 r.
Apply Hr4 to the current goal.
Assume H123 Hra.
Apply H123 to the current goal.
Assume H12 Hr2.
Apply H12 to the current goal.
Assume HrR Hr0.
An exact proof term for the current goal is Hr0.
We prove the intermediate claim Hr2: Rlt r r0.
Apply Hr4 to the current goal.
Assume H123 Hra.
Apply H123 to the current goal.
Assume H12 Hr2.
An exact proof term for the current goal is Hr2.
We prove the intermediate claim Hra: Rlt r a.
Apply Hr4 to the current goal.
Assume H123 Hra.
An exact proof term for the current goal is Hra.
We prove the intermediate claim HsubBall: open_ball X d x r ⊆ open_ball X d x r0.
An exact proof term for the current goal is (open_ball_radius_mono X d x r r0 Hr2).
We prove the intermediate claim HsubU: open_ball X d x r ⊆ U.
An exact proof term for the current goal is (Subq_tra (open_ball X d x r) (open_ball X d x r0) U HsubBall Hball0subU).
We use r to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is HrR.
An exact proof term for the current goal is Hr0r0.
An exact proof term for the current goal is HsubU.
An exact proof term for the current goal is Hra.
∎