Let X, d, c, x and r be given.
Assume Hm: metric_on X d.
Assume Hc: c ∈ X.
Assume HxX: x ∈ X.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hxin: x ∈ open_ball X d c r.
We prove the intermediate claim Hcenter: x ∈ open_ball X d x r.
An exact proof term for the current goal is (center_in_open_ball X d x r Hm HxX Hrpos).
We prove the intermediate claim Hex: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ (open_ball X d c r) ∩ (open_ball X d x r).
An exact proof term for the current goal is (open_ball_refine_intersection X d c x x r r Hm Hc HxX HxX HrR HrR Hrpos Hrpos Hxin Hcenter).
Apply Hex to the current goal.
Let s be given.
Assume Hs.
We prove the intermediate claim Hs1: 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 r) ∩ (open_ball X d x r)) Hs).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) Hs1).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) Hs1).
We prove the intermediate claim Hsubcap: open_ball X d x s ⊆ (open_ball X d c r) ∩ (open_ball X d x r).
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 r) ∩ (open_ball X d x r)) Hs).
We prove the intermediate claim Hsub: open_ball X d x s ⊆ open_ball X d c r.
An exact proof term for the current goal is (Subq_tra (open_ball X d x s) ((open_ball X d c r) ∩ (open_ball X d x r)) (open_ball X d c r) Hsubcap (binintersect_Subq_1 (open_ball X d c r) (open_ball X d x r))).
We use s to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HsR.
An exact proof term for the current goal is Hspos.
An exact proof term for the current goal is Hsub.
∎