Let X and Tx be given.
Assume Hreg: regular_space X Tx.
Assume HL: Lindelof_space X Tx.
We will prove paracompact_space X Tx.
We will prove topology_on X Tx ∧ ∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U.
Apply andI to the current goal.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
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 Hmichael: (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).
We prove the intermediate claim H123: (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).
An exact proof term for the current goal is (andEL ((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) Hmichael).
We prove the intermediate claim H12and23: (Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx) ∧ (Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx).
An exact proof term for the current goal is (andEL ((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) H123).
We prove the intermediate claim H34: Michael_cond41_3_3 X Tx → Michael_cond41_3_4 X Tx.
An exact proof term for the current goal is (andER ((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) H123).
We prove the intermediate claim H12: Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx.
An exact proof term for the current goal is (andEL (Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx) (Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx) H12and23).
We prove the intermediate claim H23: Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx.
An exact proof term for the current goal is (andER (Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx) (Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx) H12and23).
We prove the intermediate claim Hcond1: Michael_cond41_3_1 X Tx.
Let U0 be given.
Assume HU0: open_cover X Tx U0.
We will prove ∃V : set, open_cover X Tx V ∧ sigma_locally_finite_family X Tx V ∧ refine_of V U0.
We prove the intermediate claim HLprop: ∀U1 : set, open_cover X Tx U1 → ∃V : set, countable_subcollection V U1 ∧ covers X V.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U1 : set, open_cover X Tx U1 → ∃V : set, countable_subcollection V U1 ∧ covers X V) HL).
Apply (HLprop U0 HU0) to the current goal.
Let V0 be given.
Assume HV0: countable_subcollection V0 U0 ∧ covers X V0.
We prove the intermediate claim HV0subc: countable_subcollection V0 U0.
An exact proof term for the current goal is (andEL (countable_subcollection V0 U0) (covers X V0) HV0).
We prove the intermediate claim HV0cov: covers X V0.
An exact proof term for the current goal is (andER (countable_subcollection V0 U0) (covers X V0) HV0).
We prove the intermediate claim HV0sub: V0 ⊆ U0.
An exact proof term for the current goal is (andEL (V0 ⊆ U0) (countable_set V0) HV0subc).
We prove the intermediate claim HV0count: countable_set V0.
An exact proof term for the current goal is (andER (V0 ⊆ U0) (countable_set V0) HV0subc).
We prove the intermediate claim HU0Tx: ∀u : set, u ∈ U0 → u ∈ Tx.
An exact proof term for the current goal is (andEL (∀u : set, u ∈ U0 → u ∈ Tx) (covers X U0) HU0).
We prove the intermediate claim HopenV0: open_cover X Tx V0.
We will prove (∀v : set, v ∈ V0 → v ∈ Tx) ∧ covers X V0.
Apply andI to the current goal.
Let v be given.
Assume Hv: v ∈ V0.
We will prove v ∈ Tx.
We prove the intermediate claim HvU0: v ∈ U0.
An exact proof term for the current goal is (HV0sub v Hv).
An exact proof term for the current goal is (HU0Tx v HvU0).
An exact proof term for the current goal is HV0cov.
We prove the intermediate claim HsigmaV0: sigma_locally_finite_family X Tx V0.
An exact proof term for the current goal is (countable_open_cover_sigma_locally_finite_family X Tx V0 HTx HopenV0 HV0count).
We prove the intermediate claim HrefV0: refine_of V0 U0.
Let v be given.
Assume Hv: v ∈ V0.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HV0sub v Hv).
An exact proof term for the current goal is (Subq_ref v).
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 HopenV0.
An exact proof term for the current goal is HsigmaV0.
An exact proof term for the current goal is HrefV0.
We prove the intermediate claim Hcond2: Michael_cond41_3_2 X Tx.
An exact proof term for the current goal is (H12 Hcond1).
We prove the intermediate claim Hcond3: Michael_cond41_3_3 X Tx.
An exact proof term for the current goal is (H23 Hcond2).
We prove the intermediate claim Hcond4: Michael_cond41_3_4 X Tx.
An exact proof term for the current goal is (H34 Hcond3).
Let U be given.
Assume HU: open_cover X Tx U.
An exact proof term for the current goal is (Hcond4 U HU).
∎