Let X, d and B be given.
Assume Hm: metric_on X d.
Assume HBcov: open_cover X (metric_topology X d) B.
Assume HBballs: ∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r.
We will prove ∃V : set, open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V ∧ refine_of V B.
Set Tx to be the term metric_topology X d.
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (metric_spaces_regular X d Hm).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
We prove the intermediate claim Hcond1: Michael_cond41_3_1 X Tx.
Let U be given.
Assume HUcov: open_cover X Tx U.
We will prove ∃V : set, open_cover X Tx V ∧ sigma_locally_finite_family X Tx V ∧ refine_of V U.
We prove the intermediate claim HexB: ∃B0 : set, open_cover X Tx B0 ∧ (∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) ∧ refine_of B0 U.
An exact proof term for the current goal is (metric_open_cover_refine_by_balls X d U Hm HUcov).
Apply HexB to the current goal.
Let B0 be given.
Assume HB0pack.
We prove the intermediate claim HB0left: open_cover X Tx B0 ∧ (∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r).
An exact proof term for the current goal is (andEL (open_cover X Tx B0 ∧ (∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r)) (refine_of B0 U) HB0pack).
We prove the intermediate claim HB0cov: open_cover X Tx B0.
An exact proof term for the current goal is (andEL (open_cover X Tx B0) (∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) HB0left).
We prove the intermediate claim HB0balls: ∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r.
An exact proof term for the current goal is (andER (open_cover X Tx B0) (∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) HB0left).
We prove the intermediate claim HB0ref: refine_of B0 U.
An exact proof term for the current goal is (andER (open_cover X Tx B0 ∧ (∀b : set, b ∈ B0 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r)) (refine_of B0 U) HB0pack).
We prove the intermediate claim HexV0: ∃V0 : set, open_cover X Tx V0 ∧ sigma_locally_finite_family X Tx V0 ∧ refine_of V0 B0.
An exact proof term for the current goal is (metric_ball_open_cover_has_sigma_locally_finite_refinement X d B0 Hm HB0cov HB0balls).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pack.
We use V0 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 (andEL (open_cover X Tx V0) (sigma_locally_finite_family X Tx V0) (andEL (open_cover X Tx V0 ∧ sigma_locally_finite_family X Tx V0) (refine_of V0 B0) HV0pack)).
An exact proof term for the current goal is (andER (open_cover X Tx V0) (sigma_locally_finite_family X Tx V0) (andEL (open_cover X Tx V0 ∧ sigma_locally_finite_family X Tx V0) (refine_of V0 B0) HV0pack)).
We prove the intermediate claim HV0ref: refine_of V0 B0.
An exact proof term for the current goal is (andER (open_cover X Tx V0 ∧ sigma_locally_finite_family X Tx V0) (refine_of V0 B0) HV0pack).
An exact proof term for the current goal is (refine_trans U B0 V0 HV0ref HB0ref).
We prove the intermediate claim HimpPack: (Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx) ∧ (Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx) ∧ (Michael_cond41_3_3 X Tx → Michael_cond41_3_4 X Tx) ∧ (Michael_cond41_3_4 X Tx → Michael_cond41_3_1 X Tx).
An exact proof term for the current goal is (Michael_lemma_41_3 X Tx Hreg).
Set I12 to be the term Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx.
Set I23 to be the term Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx.
Set I34 to be the term Michael_cond41_3_3 X Tx → Michael_cond41_3_4 X Tx.
Set I41 to be the term Michael_cond41_3_4 X Tx → Michael_cond41_3_1 X Tx.
We prove the intermediate claim HimpL: ((I12 ∧ I23) ∧ I34).
An exact proof term for the current goal is (andEL ((I12 ∧ I23) ∧ I34) I41 HimpPack).
We prove the intermediate claim Himp41: I41.
An exact proof term for the current goal is (andER ((I12 ∧ I23) ∧ I34) I41 HimpPack).
We prove the intermediate claim HimpL2: (I12 ∧ I23).
An exact proof term for the current goal is (andEL (I12 ∧ I23) I34 HimpL).
We prove the intermediate claim Himp34: I34.
An exact proof term for the current goal is (andER (I12 ∧ I23) I34 HimpL).
We prove the intermediate claim Himp12: I12.
An exact proof term for the current goal is (andEL I12 I23 HimpL2).
We prove the intermediate claim Himp23: I23.
An exact proof term for the current goal is (andER I12 I23 HimpL2).
We prove the intermediate claim Hcond2: Michael_cond41_3_2 X Tx.
An exact proof term for the current goal is (Himp12 Hcond1).
We prove the intermediate claim Hcond3: Michael_cond41_3_3 X Tx.
An exact proof term for the current goal is (Himp23 Hcond2).
We prove the intermediate claim Hcond4: Michael_cond41_3_4 X Tx.
An exact proof term for the current goal is (Himp34 Hcond3).
Apply (Hcond4 B HBcov) to the current goal.
∎