Let Fam be given.

Assume HFam: open_cover_of (setprod X Y) (product_topology X Tx Y Ty) Fam.

We will prove has_finite_subcover (setprod X Y) (product_topology X Tx Y Ty) Fam.

Set UFam to be the term {U ∈ Tx|∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H}.

We prove the intermediate claim HcovUFam: open_cover_of X Tx UFam.

We will prove topology_on X Tx ∧ UFam ⊆ 𝒫 X ∧ X ⊆ ⋃ UFam ∧ (∀U : set, U ∈ UFam → U ∈ Tx).

We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.

Let U be given.

Assume HU: U ∈ UFam.

An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U0 Y ⊆ ⋃ H) U HU).

We prove the intermediate claim HTxPow: Tx ⊆ 𝒫 X.

An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).

We prove the intermediate claim HUFamPow: UFam ⊆ 𝒫 X.

Let U be given.

Assume HU: U ∈ UFam.

We prove the intermediate claim HUTx: U ∈ Tx.

An exact proof term for the current goal is (HUFamSubTx U HU).

An exact proof term for the current goal is (HTxPow U HUTx).

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HUFamPow.

We will prove X ⊆ ⋃ UFam.

Let x be given.

Assume Hx: x ∈ X.

We will prove x ∈ ⋃ UFam.

We prove the intermediate claim HexTube: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H.

We prove the intermediate claim HFamOpen: ∀U0 : set, U0 ∈ Fam → U0 ∈ product_topology X Tx Y Ty.

Let U0 be given.

Assume HU0: U0 ∈ Fam.

An exact proof term for the current goal is (open_cover_of_members_open (setprod X Y) (product_topology X Tx Y Ty) Fam U0 HFam HU0).

We prove the intermediate claim HexSlice: ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod {x} Y ⊆ ⋃ H.

We prove the intermediate claim HcovXY: setprod X Y ⊆ ⋃ Fam.

An exact proof term for the current goal is (open_cover_of_covers (setprod X Y) (product_topology X Tx Y Ty) Fam HFam).

Set B to be the term product_subbasis X Tx Y Ty.

We prove the intermediate claim HBasis: basis_on (setprod X Y) B.

An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).

Set VFam to be the term {V ∈ Ty|∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U0 V ⊆ N0}.

We prove the intermediate claim HVFamSubTy: VFam ⊆ Ty.

Let V be given.

Assume HV: V ∈ VFam.

An exact proof term for the current goal is (SepE1 Ty (λV0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U0 V0 ⊆ N0) V HV).

We prove the intermediate claim HTyPow: Ty ⊆ 𝒫 Y.

An exact proof term for the current goal is (topology_subset_axiom Y Ty HTy).

We prove the intermediate claim HVFamPow: VFam ⊆ 𝒫 Y.

Let V be given.

Assume HV: V ∈ VFam.

We prove the intermediate claim HVTy: V ∈ Ty.

An exact proof term for the current goal is (HVFamSubTy V HV).

An exact proof term for the current goal is (HTyPow V HVTy).

We prove the intermediate claim HYcovV: Y ⊆ ⋃ VFam.

Let y be given.

Assume Hy: y ∈ Y.

We will prove y ∈ ⋃ VFam.

Set p to be the term (x,y).

We prove the intermediate claim HpXY: p ∈ setprod X Y.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y x y Hx Hy).

We prove the intermediate claim HpInUnion: p ∈ ⋃ Fam.

An exact proof term for the current goal is (HcovXY p HpXY).

Apply (UnionE_impred Fam p HpInUnion) to the current goal.

Let N0 be given.

Assume HpN0: p ∈ N0.

Assume HN0Fam: N0 ∈ Fam.

We prove the intermediate claim HN0Top: N0 ∈ generated_topology (setprod X Y) B.

An exact proof term for the current goal is (HFamOpen N0 HN0Fam).

We prove the intermediate claim HN0refine: ∀q ∈ N0, ∃b ∈ B, q ∈ b ∧ b ⊆ N0.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λU0 : set ⇒ ∀q ∈ U0, ∃b ∈ B, q ∈ b ∧ b ⊆ U0) N0 HN0Top).

We prove the intermediate claim Hexb: ∃b ∈ B, p ∈ b ∧ b ⊆ N0.

An exact proof term for the current goal is (HN0refine p HpN0).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

We prove the intermediate claim HbB: b ∈ B.

An exact proof term for the current goal is (andEL (b ∈ B) (p ∈ b ∧ b ⊆ N0) Hbpair).

We prove the intermediate claim Hbprop: p ∈ b ∧ b ⊆ N0.

An exact proof term for the current goal is (andER (b ∈ B) (p ∈ b ∧ b ⊆ N0) Hbpair).

We prove the intermediate claim Hpb: p ∈ b.

An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ N0) Hbprop).

We prove the intermediate claim HbsubN0: b ⊆ N0.

An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ N0) Hbprop).

Apply (famunionE_impred Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) b HbB) to the current goal.

Let U0 be given.

Assume HU0Tx: U0 ∈ Tx.

Assume HbIn: b ∈ {rectangle_set U0 V0|V0 ∈ Ty}.

Apply (ReplE_impred Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbIn) to the current goal.

Let V0 be given.

Assume HV0Ty: V0 ∈ Ty.

Assume HbEq: b = rectangle_set U0 V0.

We prove the intermediate claim HpUV: p ∈ setprod U0 V0.

We will prove p ∈ rectangle_set U0 V0.

rewrite the current goal using HbEq (from right to left) at position 1.

An exact proof term for the current goal is Hpb.

We prove the intermediate claim HpXY0: p ∈ setprod {x} {y}.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x} {y} x y (SingI x) (SingI y)).

We prove the intermediate claim Hcoords: x ∈ U0 ∧ y ∈ V0.

An exact proof term for the current goal is (setprod_coords_in x y U0 V0 p HpXY0 HpUV).

We prove the intermediate claim HxU0: x ∈ U0.

An exact proof term for the current goal is (andEL (x ∈ U0) (y ∈ V0) Hcoords).

We prove the intermediate claim HyV0: y ∈ V0.

An exact proof term for the current goal is (andER (x ∈ U0) (y ∈ V0) Hcoords).

We prove the intermediate claim HrectSub: setprod U0 V0 ⊆ N0.

rewrite the current goal using HbEq (from right to left) at position 1.

An exact proof term for the current goal is HbsubN0.

We prove the intermediate claim HV0Fam: V0 ∈ VFam.

Apply (SepI Ty (λV1 : set ⇒ ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ ∃N1 : set, N1 ∈ Fam ∧ setprod U1 V1 ⊆ N1) V0 HV0Ty) to the current goal.

We use U0 to witness the existential quantifier.

We will prove U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N1 : set, N1 ∈ Fam ∧ setprod U0 V0 ⊆ N1.

Apply andI to the current goal.

An exact proof term for the current goal is (andI (U0 ∈ Tx) (x ∈ U0) HU0Tx HxU0).

We use N0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (N0 ∈ Fam) (setprod U0 V0 ⊆ N0) HN0Fam HrectSub).

An exact proof term for the current goal is (UnionI VFam y V0 HyV0 HV0Fam).

We prove the intermediate claim HVFamCover: open_cover_of Y Ty VFam.

We will prove topology_on Y Ty ∧ VFam ⊆ 𝒫 Y ∧ Y ⊆ ⋃ VFam ∧ (∀U0 : set, U0 ∈ VFam → U0 ∈ Ty).

Apply andI to the current goal.

An exact proof term for the current goal is HTy.

An exact proof term for the current goal is HVFamPow.

An exact proof term for the current goal is HYcovV.

Let V be given.

Assume HV: V ∈ VFam.

An exact proof term for the current goal is (HVFamSubTy V HV).

We prove the intermediate claim HfinV: has_finite_subcover Y Ty VFam.

An exact proof term for the current goal is (Heine_Borel_subcover Y Ty VFam HY HVFamCover).

Apply HfinV to the current goal.

Let G be given.

Assume HG: G ⊆ VFam ∧ finite G ∧ Y ⊆ ⋃ G.

We prove the intermediate claim HGsub: G ⊆ VFam.

An exact proof term for the current goal is (andEL (G ⊆ VFam) (finite G) (andEL (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HG)).

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (andER (G ⊆ VFam) (finite G) (andEL (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HG)).

We prove the intermediate claim HYcovG: Y ⊆ ⋃ G.

An exact proof term for the current goal is (andER (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HG).

Set pickU to be the term λV : set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U0 V ⊆ N0).

We prove the intermediate claim HpickU: ∀V : set, V ∈ VFam → pickU V ∈ Tx ∧ x ∈ pickU V ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0.

Let V be given.

Assume HV: V ∈ VFam.

We prove the intermediate claim Hex: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U0 V ⊆ N0.

An exact proof term for the current goal is (SepE2 Ty (λV0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U0 V0 ⊆ N0) V HV).

Apply Hex to the current goal.

Let U0 be given.

Assume HU0: U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U0 V ⊆ N0.

An exact proof term for the current goal is (Eps_i_ax (λU1 : set ⇒ U1 ∈ Tx ∧ x ∈ U1 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod U1 V ⊆ N0) U0 HU0).

Set pickN to be the term λV : set ⇒ Eps_i (λN0 : set ⇒ N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0).

We prove the intermediate claim HpickN: ∀V : set, V ∈ VFam → pickN V ∈ Fam ∧ setprod (pickU V) V ⊆ pickN V.

Let V be given.

Assume HV: V ∈ VFam.

We prove the intermediate claim Hprop: pickU V ∈ Tx ∧ x ∈ pickU V ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0.

An exact proof term for the current goal is (HpickU V HV).

We prove the intermediate claim HpropAB: pickU V ∈ Tx ∧ x ∈ pickU V.

An exact proof term for the current goal is (andEL (pickU V ∈ Tx ∧ x ∈ pickU V) (∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0) Hprop).

We prove the intermediate claim HexN: ∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0.

An exact proof term for the current goal is (andER (pickU V ∈ Tx ∧ x ∈ pickU V) (∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0) Hprop).

Apply HexN to the current goal.

Let N0 be given.

Assume HN0: N0 ∈ Fam ∧ setprod (pickU V) V ⊆ N0.

An exact proof term for the current goal is (Eps_i_ax (λN1 : set ⇒ N1 ∈ Fam ∧ setprod (pickU V) V ⊆ N1) N0 HN0).

Set H to be the term {pickN V|V ∈ G}.

We use H to witness the existential quantifier.

Apply andI to the current goal.

We will prove H ⊆ Fam.

Let N0 be given.

Assume HN0: N0 ∈ H.

Apply (ReplE_impred G (λV0 : set ⇒ pickN V0) N0 HN0) to the current goal.

Let V0 be given.

Assume HV0G: V0 ∈ G.

Assume HN0Eq: N0 = pickN V0.

We prove the intermediate claim HV0Fam: V0 ∈ VFam.

An exact proof term for the current goal is (HGsub V0 HV0G).

We prove the intermediate claim HNprop: pickN V0 ∈ Fam ∧ setprod (pickU V0) V0 ⊆ pickN V0.

An exact proof term for the current goal is (HpickN V0 HV0Fam).

We prove the intermediate claim HN0Fam: pickN V0 ∈ Fam.

An exact proof term for the current goal is (andEL (pickN V0 ∈ Fam) (setprod (pickU V0) V0 ⊆ pickN V0) HNprop).

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

An exact proof term for the current goal is HN0Fam.

An exact proof term for the current goal is (Repl_finite (λV0 : set ⇒ pickN V0) G HGfin).

We will prove setprod {x} Y ⊆ ⋃ H.

Let p be given.

Assume Hp: p ∈ setprod {x} Y.

We will prove p ∈ ⋃ H.

We prove the intermediate claim Hp0: p 0 ∈ {x}.

An exact proof term for the current goal is (ap0_Sigma {x} (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim Hp1: p 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma {x} (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim Hp0eq: p 0 = x.

An exact proof term for the current goal is (SingE x (p 0) Hp0).

We prove the intermediate claim HpEta: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta {x} Y p Hp).

We prove the intermediate claim Hp1InUnion: p 1 ∈ ⋃ G.

An exact proof term for the current goal is (HYcovG (p 1) Hp1).

Apply (UnionE_impred G (p 1) Hp1InUnion) to the current goal.

Let V0 be given.

Assume Hp1V0: p 1 ∈ V0.

Assume HV0G: V0 ∈ G.

We prove the intermediate claim HV0Fam: V0 ∈ VFam.

An exact proof term for the current goal is (HGsub V0 HV0G).

We prove the intermediate claim HUN: pickU V0 ∈ Tx ∧ x ∈ pickU V0 ∧ ∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V0) V0 ⊆ N0.

An exact proof term for the current goal is (HpickU V0 HV0Fam).

We prove the intermediate claim HUNAB: pickU V0 ∈ Tx ∧ x ∈ pickU V0.

An exact proof term for the current goal is (andEL (pickU V0 ∈ Tx ∧ x ∈ pickU V0) (∃N0 : set, N0 ∈ Fam ∧ setprod (pickU V0) V0 ⊆ N0) HUN).

We prove the intermediate claim HxPick: x ∈ pickU V0.

An exact proof term for the current goal is (andER (pickU V0 ∈ Tx) (x ∈ pickU V0) HUNAB).

We prove the intermediate claim HNprop: pickN V0 ∈ Fam ∧ setprod (pickU V0) V0 ⊆ pickN V0.

An exact proof term for the current goal is (HpickN V0 HV0Fam).

We prove the intermediate claim HrectSub: setprod (pickU V0) V0 ⊆ pickN V0.

An exact proof term for the current goal is (andER (pickN V0 ∈ Fam) (setprod (pickU V0) V0 ⊆ pickN V0) HNprop).

We prove the intermediate claim HpInRect: (x,p 1) ∈ setprod (pickU V0) V0.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (pickU V0) V0 x (p 1) HxPick Hp1V0).

We prove the intermediate claim HpInN: (x,p 1) ∈ pickN V0.

An exact proof term for the current goal is (HrectSub (x,p 1) HpInRect).

We prove the intermediate claim HNinH: pickN V0 ∈ H.

An exact proof term for the current goal is (ReplI G (λV1 : set ⇒ pickN V1) V0 HV0G).

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

rewrite the current goal using Hp0eq (from left to right) at position 1.

An exact proof term for the current goal is (UnionI H (x,p 1) (pickN V0) HpInN HNinH).

Apply HexSlice to the current goal.

Let H be given.

Assume HH: H ⊆ Fam ∧ finite H ∧ setprod {x} Y ⊆ ⋃ H.

We prove the intermediate claim HHsub: H ⊆ Fam.

An exact proof term for the current goal is (andEL (H ⊆ Fam) (finite H) (andEL (H ⊆ Fam ∧ finite H) (setprod {x} Y ⊆ ⋃ H) HH)).

We prove the intermediate claim HHfin: finite H.

An exact proof term for the current goal is (andER (H ⊆ Fam) (finite H) (andEL (H ⊆ Fam ∧ finite H) (setprod {x} Y ⊆ ⋃ H) HH)).

We prove the intermediate claim HHcov: setprod {x} Y ⊆ ⋃ H.

An exact proof term for the current goal is (andER (H ⊆ Fam ∧ finite H) (setprod {x} Y ⊆ ⋃ H) HH).

We prove the intermediate claim HHsubTop: H ⊆ product_topology X Tx Y Ty.

Let N0 be given.

Assume HN0: N0 ∈ H.

We prove the intermediate claim HN0Fam: N0 ∈ Fam.

An exact proof term for the current goal is (HHsub N0 HN0).

An exact proof term for the current goal is (HFamOpen N0 HN0Fam).

We prove the intermediate claim HtopProd: topology_on (setprod X Y) (product_topology X Tx Y Ty).

An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).

We prove the intermediate claim HNtop: ⋃ H ∈ product_topology X Tx Y Ty.

An exact proof term for the current goal is (topology_union_closed (setprod X Y) (product_topology X Tx Y Ty) H HtopProd HHsubTop).

We prove the intermediate claim Htube: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ setprod U Y ⊆ ⋃ H.

An exact proof term for the current goal is (tube_lemma X Tx Y Ty HTx HTy HY x Hx (⋃ H) (andI ((⋃ H) ∈ product_topology X Tx Y Ty) (setprod {x} Y ⊆ ⋃ H) HNtop HHcov)).

Apply Htube to the current goal.

Let U be given.

Assume HU: U ∈ Tx ∧ x ∈ U ∧ setprod U Y ⊆ ⋃ H.

We prove the intermediate claim HUAB0: U ∈ Tx ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (setprod U Y ⊆ ⋃ H) HU).

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HUAB0.

We use H to witness the existential quantifier.

An exact proof term for the current goal is (andI (H ⊆ Fam ∧ finite H) (setprod U Y ⊆ ⋃ H) (andI (H ⊆ Fam) (finite H) HHsub HHfin) (andER (U ∈ Tx ∧ x ∈ U) (setprod U Y ⊆ ⋃ H) HU)).

Apply HexTube to the current goal.

Let U be given.

Assume HU: U ∈ Tx ∧ x ∈ U ∧ ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H.

We prove the intermediate claim HUAB: U ∈ Tx ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H) HU).

We prove the intermediate claim HUtx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HUAB).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HUAB).

We prove the intermediate claim HexH: ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H) HU).

We prove the intermediate claim HUinUFam: U ∈ UFam.

Apply (SepI Tx (λU0 : set ⇒ ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U0 Y ⊆ ⋃ H) U HUtx) to the current goal.

An exact proof term for the current goal is HexH.

An exact proof term for the current goal is (UnionI UFam x U HxU HUinUFam).

Let U be given.

Assume HU: U ∈ UFam.

An exact proof term for the current goal is (HUFamSubTx U HU).

We prove the intermediate claim HfinUFam: has_finite_subcover X Tx UFam.

An exact proof term for the current goal is (Heine_Borel_subcover X Tx UFam HX HcovUFam).

Apply HfinUFam to the current goal.

Let K be given.

Assume HK: K ⊆ UFam ∧ finite K ∧ X ⊆ ⋃ K.

We prove the intermediate claim HKsub: K ⊆ UFam.

An exact proof term for the current goal is (andEL (K ⊆ UFam) (finite K) (andEL (K ⊆ UFam ∧ finite K) (X ⊆ ⋃ K) HK)).

We prove the intermediate claim HKfin: finite K.

An exact proof term for the current goal is (andER (K ⊆ UFam) (finite K) (andEL (K ⊆ UFam ∧ finite K) (X ⊆ ⋃ K) HK)).

We prove the intermediate claim HXcovK: X ⊆ ⋃ K.

An exact proof term for the current goal is (andER (K ⊆ UFam ∧ finite K) (X ⊆ ⋃ K) HK).

Set pickH to be the term λU : set ⇒ Eps_i (λH : set ⇒ H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H).

We prove the intermediate claim HpickH: ∀U : set, U ∈ UFam → pickH U ⊆ Fam ∧ finite (pickH U) ∧ setprod U Y ⊆ ⋃ (pickH U).

Let U be given.

Assume HU: U ∈ UFam.

We prove the intermediate claim Hex: ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H.

An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃H : set, H ⊆ Fam ∧ finite H ∧ setprod U0 Y ⊆ ⋃ H) U HU).

Apply Hex to the current goal.

Let H0 be given.

Assume HH0: H0 ⊆ Fam ∧ finite H0 ∧ setprod U Y ⊆ ⋃ H0.

An exact proof term for the current goal is (Eps_i_ax (λH : set ⇒ H ⊆ Fam ∧ finite H ∧ setprod U Y ⊆ ⋃ H) H0 HH0).

Set G to be the term ⋃_{U ∈ K}pickH U.

We will prove has_finite_subcover (setprod X Y) (product_topology X Tx Y Ty) Fam.

We will prove ∃G0 : set, G0 ⊆ Fam ∧ finite G0 ∧ setprod X Y ⊆ ⋃ G0.

We use G to witness the existential quantifier.

Apply andI to the current goal.

We will prove G ⊆ Fam ∧ finite G.

Apply andI to the current goal.

We will prove G ⊆ Fam.

Let N be given.

Assume HN: N ∈ G.

We will prove N ∈ Fam.

Apply (famunionE_impred K (λU0 : set ⇒ pickH U0) N HN) to the current goal.

Let U0 be given.

Assume HU0K: U0 ∈ K.

Assume HNin: N ∈ pickH U0.

We prove the intermediate claim HU0UFam: U0 ∈ UFam.

An exact proof term for the current goal is (HKsub U0 HU0K).

We prove the intermediate claim Hprop: pickH U0 ⊆ Fam ∧ finite (pickH U0) ∧ setprod U0 Y ⊆ ⋃ (pickH U0).

An exact proof term for the current goal is (HpickH U0 HU0UFam).

We prove the intermediate claim HpropAB: pickH U0 ⊆ Fam ∧ finite (pickH U0).

An exact proof term for the current goal is (andEL (pickH U0 ⊆ Fam ∧ finite (pickH U0)) (setprod U0 Y ⊆ ⋃ (pickH U0)) Hprop).

We prove the intermediate claim HsubFam: pickH U0 ⊆ Fam.

An exact proof term for the current goal is (andEL (pickH U0 ⊆ Fam) (finite (pickH U0)) HpropAB).

An exact proof term for the current goal is (HsubFam N HNin).

We will prove finite G.

We prove the intermediate claim HpEmpty: Empty ⊆ UFam → finite (⋃_{U ∈ Empty}pickH U).

Assume _.

rewrite the current goal using (famunion_Empty (λU : set ⇒ pickH U)) (from left to right).

An exact proof term for the current goal is finite_Empty.

We prove the intermediate claim HpStep: ∀K0 y : set, finite K0 → y ∉ K0 → (K0 ⊆ UFam → finite (⋃_{U ∈ K0}pickH U)) → ((K0 ∪ {y}) ⊆ UFam → finite (⋃_{U ∈ (K0 ∪ {y})}pickH U)).

Let K0 and y be given.

Assume HK0fin HyNotin IH.

Assume Hsub: (K0 ∪ {y}) ⊆ UFam.

We prove the intermediate claim HK0sub: K0 ⊆ UFam.

Let U be given.

Assume HU: U ∈ K0.

An exact proof term for the current goal is (Hsub U (binunionI1 K0 {y} U HU)).

We prove the intermediate claim HyUFam: y ∈ UFam.

An exact proof term for the current goal is (Hsub y (binunionI2 K0 {y} y (SingI y))).

We prove the intermediate claim Hfin0: finite (⋃_{U ∈ K0}pickH U).

An exact proof term for the current goal is (IH HK0sub).

We prove the intermediate claim HpropY: pickH y ⊆ Fam ∧ finite (pickH y) ∧ setprod y Y ⊆ ⋃ (pickH y).

An exact proof term for the current goal is (HpickH y HyUFam).

We prove the intermediate claim HpropYAB: pickH y ⊆ Fam ∧ finite (pickH y).

An exact proof term for the current goal is (andEL (pickH y ⊆ Fam ∧ finite (pickH y)) (setprod y Y ⊆ ⋃ (pickH y)) HpropY).

We prove the intermediate claim HfinY: finite (pickH y).

An exact proof term for the current goal is (andER (pickH y ⊆ Fam) (finite (pickH y)) HpropYAB).

We prove the intermediate claim Heq: (⋃_{U ∈ (K0 ∪ {y})}pickH U) = (⋃_{U ∈ K0}pickH U) ∪ pickH y.

Apply set_ext to the current goal.

Let N be given.

Assume HN: N ∈ (⋃_{U ∈ (K0 ∪ {y})}pickH U).

We will prove N ∈ (⋃_{U ∈ K0}pickH U) ∪ pickH y.

Apply (famunionE_impred (K0 ∪ {y}) (λU1 : set ⇒ pickH U1) N HN) to the current goal.

Let U1 be given.

Assume HU1: U1 ∈ K0 ∪ {y}.

Assume HNin: N ∈ pickH U1.

Apply (binunionE' K0 {y} U1 (N ∈ (⋃_{U ∈ K0}pickH U) ∪ pickH y)) to the current goal.

Assume HU1K0: U1 ∈ K0.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is (famunionI K0 (λU2 : set ⇒ pickH U2) U1 N HU1K0 HNin).

Assume HU1y: U1 ∈ {y}.

We prove the intermediate claim HU1eq: U1 = y.

An exact proof term for the current goal is (SingE y U1 HU1y).

We prove the intermediate claim HNy: N ∈ pickH y.

We will prove N ∈ pickH y.

rewrite the current goal using HU1eq (from right to left) at position 1.

An exact proof term for the current goal is HNin.

An exact proof term for the current goal is (binunionI2 (⋃_{U ∈ K0}pickH U) (pickH y) N HNy).

An exact proof term for the current goal is HU1.

Let N be given.

Assume HN: N ∈ (⋃_{U ∈ K0}pickH U) ∪ pickH y.

We will prove N ∈ (⋃_{U ∈ (K0 ∪ {y})}pickH U).

Apply (binunionE' (⋃_{U ∈ K0}pickH U) (pickH y) N (N ∈ (⋃_{U ∈ (K0 ∪ {y})}pickH U))) to the current goal.

Assume HN0: N ∈ (⋃_{U ∈ K0}pickH U).

Apply (famunionE_impred K0 (λU1 : set ⇒ pickH U1) N HN0) to the current goal.

Let U1 be given.

Assume HU1K0: U1 ∈ K0.

Assume HN1: N ∈ pickH U1.

An exact proof term for the current goal is (famunionI (K0 ∪ {y}) (λU2 : set ⇒ pickH U2) U1 N (binunionI1 K0 {y} U1 HU1K0) HN1).

Assume HNy: N ∈ pickH y.

An exact proof term for the current goal is (famunionI (K0 ∪ {y}) (λU2 : set ⇒ pickH U2) y N (binunionI2 K0 {y} y (SingI y)) HNy).

An exact proof term for the current goal is HN.

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

An exact proof term for the current goal is (binunion_finite (⋃_{U ∈ K0}pickH U) Hfin0 (pickH y) HfinY).

We prove the intermediate claim Hall: K ⊆ UFam → finite (⋃_{U ∈ K}pickH U).

An exact proof term for the current goal is (finite_ind (λK0 : set ⇒ K0 ⊆ UFam → finite (⋃_{U ∈ K0}pickH U)) HpEmpty HpStep K HKfin).

An exact proof term for the current goal is (Hall HKsub).

Let p be given.

Assume Hp: p ∈ setprod X Y.

We will prove p ∈ ⋃ G.

We prove the intermediate claim Hp0X: p 0 ∈ X.

An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim Hp1Y: p 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim HpEta: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta X Y p Hp).

We prove the intermediate claim Hp0InUnion: p 0 ∈ ⋃ K.

An exact proof term for the current goal is (HXcovK (p 0) Hp0X).

Apply (UnionE_impred K (p 0) Hp0InUnion) to the current goal.

Let U0 be given.

Assume Hp0U0: p 0 ∈ U0.

Assume HU0K: U0 ∈ K.

We prove the intermediate claim HU0UFam: U0 ∈ UFam.

An exact proof term for the current goal is (HKsub U0 HU0K).

We prove the intermediate claim Hprop: pickH U0 ⊆ Fam ∧ finite (pickH U0) ∧ setprod U0 Y ⊆ ⋃ (pickH U0).

An exact proof term for the current goal is (HpickH U0 HU0UFam).

We prove the intermediate claim HcovU0: setprod U0 Y ⊆ ⋃ (pickH U0).

An exact proof term for the current goal is (andER (pickH U0 ⊆ Fam ∧ finite (pickH U0)) (setprod U0 Y ⊆ ⋃ (pickH U0)) Hprop).

We prove the intermediate claim HpInU0Y: (p 0,p 1) ∈ setprod U0 Y.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 Y (p 0) (p 1) Hp0U0 Hp1Y).

We prove the intermediate claim HpInUnionPick: (p 0,p 1) ∈ ⋃ (pickH U0).

An exact proof term for the current goal is (HcovU0 (p 0,p 1) HpInU0Y).

Apply (UnionE_impred (pickH U0) (p 0,p 1) HpInUnionPick) to the current goal.

Let N be given.

Assume HpN: (p 0,p 1) ∈ N.

Assume HNpick: N ∈ pickH U0.

We prove the intermediate claim HNinG: N ∈ G.

An exact proof term for the current goal is (famunionI K (λU1 : set ⇒ pickH U1) U0 N HU0K HNpick).

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

An exact proof term for the current goal is (UnionI G (p 0,p 1) N HpN HNinG).