Let X, Tx, Y, Ty and f be given.
Assume Hhom: homeomorphism X Tx Y Ty f.
Assume HmetY: metrizable Y Ty.
Apply HmetY to the current goal.
Let dY be given.
Assume HdYpair: metric_on Y dY ∧ metric_topology Y dY = Ty.
We prove the intermediate claim HdY: metric_on Y dY.
An exact proof term for the current goal is (andEL (metric_on Y dY) (metric_topology Y dY = Ty) HdYpair).
We prove the intermediate claim HTyEq: metric_topology Y dY = Ty.
An exact proof term for the current goal is (andER (metric_on Y dY) (metric_topology Y dY = Ty) HdYpair).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (homeomorphism_topology_left X Tx Y Ty f Hhom).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (homeomorphism_topology_right X Tx Y Ty f Hhom).
We prove the intermediate claim Hcontf: continuous_map X Tx Y Ty f.
An exact proof term for the current goal is (homeomorphism_continuous X Tx Y Ty f Hhom).
We prove the intermediate claim Hfunf: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcontf).
We prove the intermediate claim Hinjf: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → apply_fun f x1 = apply_fun f x2 → x1 = x2.
An exact proof term for the current goal is (homeomorphism_injective X Tx Y Ty f Hhom).
We prove the intermediate claim Hexg: ∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y).
An exact proof term for the current goal is (homeomorphism_inverse_package X Tx Y Ty f Hhom).
Apply Hexg to the current goal.
Let g be given.
Assume Hgpack.
We prove the intermediate claim Hcoreg: continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x).
An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x)) (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y) Hgpack).
We prove the intermediate claim Hcontg: continuous_map Y Ty X Tx g.
An exact proof term for the current goal is (andEL (continuous_map Y Ty X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) Hcoreg).
We prove the intermediate claim Hginv: ∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x.
An exact proof term for the current goal is (andER (continuous_map Y Ty X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) Hcoreg).
Set dX to be the term graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
We prove the intermediate claim HdXmetric: metric_on X dX.
We prove the intermediate claim Hmdef: metric_on X dX = (function_on dX (setprod X X) R ∧ (∀x y : set, x ∈ X → y ∈ X → apply_fun dX (x,y) = apply_fun dX (y,x)) ∧ (∀x : set, x ∈ X → apply_fun dX (x,x) = 0) ∧ (∀x y : set, x ∈ X → y ∈ X → ¬ (Rlt (apply_fun dX (x,y)) 0) ∧ (apply_fun dX (x,y) = 0 → x = y)) ∧ (∀x y z : set, x ∈ X → y ∈ X → z ∈ X → ¬ (Rlt (add_SNo (apply_fun dX (x,y)) (apply_fun dX (y,z))) (apply_fun dX (x,z))))).
Use reflexivity.
rewrite the current goal using Hmdef (from left to right).
Apply and5I to the current goal.
We prove the intermediate claim HtotdX: total_function_on dX (setprod X X) R.
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
rewrite the current goal using HdXdef (from left to right).
Apply (total_function_on_graph (setprod X X) R (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1)))) to the current goal.
Let pq be given.
Assume Hpq: pq ∈ setprod X X.
We will prove apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1)) ∈ R.
We prove the intermediate claim HxX: (pq 0) ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ X) pq Hpq).
We prove the intermediate claim HyX: (pq 1) ∈ X.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ X) pq Hpq).
We prove the intermediate claim HfxY: apply_fun f (pq 0) ∈ Y.
An exact proof term for the current goal is (Hfunf (pq 0) HxX).
We prove the intermediate claim HfyY: apply_fun f (pq 1) ∈ Y.
An exact proof term for the current goal is (Hfunf (pq 1) HyX).
We prove the intermediate claim HpairY: (apply_fun f (pq 0),apply_fun f (pq 1)) ∈ setprod Y Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun f (pq 0)) (apply_fun f (pq 1)) HfxY HfyY).
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun f (pq 0),apply_fun f (pq 1)) HpairY).
An exact proof term for the current goal is (total_function_on_function_on dX (setprod X X) R HtotdX).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
We will prove apply_fun dX (x,y) = apply_fun dX (y,x).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim HfyY: apply_fun f y ∈ Y.
An exact proof term for the current goal is (Hfunf y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HyxIn: (y,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y x HyX HxX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HyxEq0: apply_fun dX (y,x) = apply_fun dY (apply_fun f ((y,x) 0),apply_fun f ((y,x) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (y,x) HyxIn).
rewrite the current goal using HxyEq0 (from left to right).
rewrite the current goal using HyxEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (tuple_2_0_eq y x) (from left to right).
rewrite the current goal using (tuple_2_1_eq y x) (from left to right).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f x) (apply_fun f y) HdY HfxY HfyY).
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun dX (x,x) = 0.
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim HxxIn: (x,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x x HxX HxX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
We prove the intermediate claim HxxEq0: apply_fun dX (x,x) = apply_fun dY (apply_fun f ((x,x) 0),apply_fun f ((x,x) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,x) HxxIn).
rewrite the current goal using HxxEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
An exact proof term for the current goal is (metric_on_diag_zero Y dY (apply_fun f x) HdY HfxY).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
We will prove ¬ (Rlt (apply_fun dX (x,y)) 0) ∧ (apply_fun dX (x,y) = 0 → x = y).
Apply andI to the current goal.
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim HfyY: apply_fun f y ∈ Y.
An exact proof term for the current goal is (Hfunf y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,y) HxyIn).
rewrite the current goal using HxyEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
An exact proof term for the current goal is (metric_on_nonneg Y dY (apply_fun f x) (apply_fun f y) HdY HfxY HfyY).
Assume H0: apply_fun dX (x,y) = 0.
We will prove x = y.
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim HfyY: apply_fun f y ∈ Y.
An exact proof term for the current goal is (Hfunf y HyX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HyEq0: apply_fun dY (apply_fun f x,apply_fun f y) = 0.
We prove the intermediate claim HxyEqRev: apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1)) = apply_fun dX (x,y).
Use symmetry.
An exact proof term for the current goal is HxyEq0.
We prove the intermediate claim Htmp: apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1)) = 0.
An exact proof term for the current goal is (eq_i_tra (apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1))) (apply_fun dX (x,y)) 0 HxyEqRev H0).
rewrite the current goal using (tuple_2_0_eq x y) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq x y) (from right to left) at position 2.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HfyEq: apply_fun f x = apply_fun f y.
An exact proof term for the current goal is (metric_on_zero_eq Y dY (apply_fun f x) (apply_fun f y) HdY HfxY HfyY HyEq0).
An exact proof term for the current goal is (Hinjf x y HxX HyX HfyEq).
Let x, y and z be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HzX: z ∈ X.
We will prove ¬ (Rlt (add_SNo (apply_fun dX (x,y)) (apply_fun dX (y,z))) (apply_fun dX (x,z))).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim HfyY: apply_fun f y ∈ Y.
An exact proof term for the current goal is (Hfunf y HyX).
We prove the intermediate claim HfzY: apply_fun f z ∈ Y.
An exact proof term for the current goal is (Hfunf z HzX).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y HxX HyX).
We prove the intermediate claim HyzIn: (y,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y z HyX HzX).
We prove the intermediate claim HxzIn: (x,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x z HxX HzX).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
We prove the intermediate claim HxyEq0: apply_fun dX (x,y) = apply_fun dY (apply_fun f ((x,y) 0),apply_fun f ((x,y) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,y) HxyIn).
We prove the intermediate claim HyzEq0: apply_fun dX (y,z) = apply_fun dY (apply_fun f ((y,z) 0),apply_fun f ((y,z) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (y,z) HyzIn).
We prove the intermediate claim HxzEq0: apply_fun dX (x,z) = apply_fun dY (apply_fun f ((x,z) 0),apply_fun f ((x,z) 1)).
rewrite the current goal using HdXdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,z) HxzIn).
rewrite the current goal using HxyEq0 (from left to right).
rewrite the current goal using HyzEq0 (from left to right).
rewrite the current goal using HxzEq0 (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
An exact proof term for the current goal is (metric_on_triangle Y dY (apply_fun f x) (apply_fun f y) (apply_fun f z) HdY HfxY HfyY HfzY).
We will prove ∃d : set, metric_on X d ∧ metric_topology X d = Tx.
We use dX to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HdXmetric.
We will prove metric_topology X dX = Tx.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ metric_topology X dX.
We will prove U ∈ Tx.
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hmtdef: metric_topology X dX = generated_topology X Bx.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X Bx.
rewrite the current goal using Hmtdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HBxSub: ∀b ∈ Bx, b ∈ Tx.
Let b be given.
Assume Hb: b ∈ Bx.
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}) b Hb (b ∈ Tx)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HbIn: b ∈ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X dX x0 r0) b HbIn (b ∈ Tx)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hbeq: b = open_ball X dX x0 r0.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hx0Y: apply_fun f x0 ∈ Y.
An exact proof term for the current goal is (Hfunf x0 Hx0X).
We prove the intermediate claim HballYTy: open_ball Y dY (apply_fun f x0) r0 ∈ Ty.
rewrite the current goal using HTyEq (from right to left).
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY (apply_fun f x0) r0 HdY Hx0Y Hr0pos).
We prove the intermediate claim HballPre: preimage_of X f (open_ball Y dY (apply_fun f x0) r0) = open_ball X dX x0 r0.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ preimage_of X f (open_ball Y dY (apply_fun f x0) r0).
We will prove z ∈ open_ball X dX x0 r0.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λt : set ⇒ apply_fun f t ∈ open_ball Y dY (apply_fun f x0) r0) z Hz).
We prove the intermediate claim HfzBall: apply_fun f z ∈ open_ball Y dY (apply_fun f x0) r0.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ apply_fun f t ∈ open_ball Y dY (apply_fun f x0) r0) z Hz).
We prove the intermediate claim HltY: Rlt (apply_fun dY (apply_fun f x0,apply_fun f z)) r0.
An exact proof term for the current goal is (open_ballE2 Y dY (apply_fun f x0) r0 (apply_fun f z) HfzBall).
We prove the intermediate claim HxzIn: (x0,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 z Hx0X HzX).
We prove the intermediate claim HdEq: apply_fun dX (x0,z) = apply_fun dY (apply_fun f x0,apply_fun f z).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
rewrite the current goal using HdXdef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x0,z) HxzIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x0 z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 z) (from left to right).
Use reflexivity.
We prove the intermediate claim HltX: Rlt (apply_fun dX (x0,z)) r0.
rewrite the current goal using HdEq (from left to right).
An exact proof term for the current goal is HltY.
An exact proof term for the current goal is (open_ballI X dX x0 r0 z HzX HltX).
Let z be given.
Assume Hz: z ∈ open_ball X dX x0 r0.
We will prove z ∈ preimage_of X f (open_ball Y dY (apply_fun f x0) r0).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (open_ballE1 X dX x0 r0 z Hz).
We prove the intermediate claim HltX: Rlt (apply_fun dX (x0,z)) r0.
An exact proof term for the current goal is (open_ballE2 X dX x0 r0 z Hz).
We prove the intermediate claim HxzIn: (x0,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x0 z Hx0X HzX).
We prove the intermediate claim HdEq: apply_fun dX (x0,z) = apply_fun dY (apply_fun f x0,apply_fun f z).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
rewrite the current goal using HdXdef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x0,z) HxzIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x0 z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 z) (from left to right).
Use reflexivity.
We prove the intermediate claim HzY: apply_fun f z ∈ Y.
An exact proof term for the current goal is (Hfunf z HzX).
We prove the intermediate claim HltY: Rlt (apply_fun dY (apply_fun f x0,apply_fun f z)) r0.
rewrite the current goal using HdEq (from right to left).
An exact proof term for the current goal is HltX.
We prove the intermediate claim HfzBall: apply_fun f z ∈ open_ball Y dY (apply_fun f x0) r0.
An exact proof term for the current goal is (open_ballI Y dY (apply_fun f x0) r0 (apply_fun f z) HzY HltY).
An exact proof term for the current goal is (SepI X (λt : set ⇒ apply_fun f t ∈ open_ball Y dY (apply_fun f x0) r0) z HzX HfzBall).
rewrite the current goal using HballPre (from right to left).
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcontf (open_ball Y dY (apply_fun f x0) r0) HballYTy).
We prove the intermediate claim Hfiner: finer_than Tx (generated_topology X Bx).
An exact proof term for the current goal is (generated_topology_finer_weak X Bx Tx HTx HBxSub).
An exact proof term for the current goal is (Hfiner U HUgen).
Let U be given.
Assume HU: U ∈ Tx.
We will prove U ∈ metric_topology X dX.
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X dX x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hmtdef: metric_topology X dX = generated_topology X Bx.
Use reflexivity.
rewrite the current goal using Hmtdef (from left to right).
We prove the intermediate claim HBasis: basis_on X Bx.
An exact proof term for the current goal is (open_balls_form_basis X dX HdXmetric).
rewrite the current goal using (lemma_generated_topology_characterization X Bx HBasis) (from left to right).
We will prove U ∈ {U0 ∈ 𝒫 X|∀x ∈ U0, ∃b ∈ Bx, x ∈ b ∧ b ⊆ U0}.
Apply (SepI (𝒫 X) (λU0 : set ⇒ ∀x : set, x ∈ U0 → ∃b ∈ Bx, x ∈ b ∧ b ⊆ U0) U) to the current goal.
An exact proof term for the current goal is (PowerI X U (topology_elem_subset X Tx U HTx HU)).
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is ((topology_elem_subset X Tx U HTx HU) x HxU).
Set V to be the term preimage_of Y g U.
We prove the intermediate claim HVTy: V ∈ Ty.
An exact proof term for the current goal is (continuous_map_preimage Y Ty X Tx g Hcontg U HU).
We prove the intermediate claim HVmt: V ∈ metric_topology Y dY.
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is HVTy.
We prove the intermediate claim Hy0Y: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfunf x HxX).
We prove the intermediate claim HgfxEq: apply_fun g (apply_fun f x) = x.
An exact proof term for the current goal is (Hginv x HxX).
We prove the intermediate claim HgfxU: apply_fun g (apply_fun f x) ∈ U.
rewrite the current goal using HgfxEq (from left to right).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hy0V: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepI Y (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun f x) Hy0Y HgfxU).
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball Y dY (apply_fun f x) r ⊆ V).
An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball Y dY (apply_fun f x) V HdY Hy0Y HVmt Hy0V).
Apply Hexr to the current goal.
Let r be given.
Assume Hrpack: r ∈ R ∧ (Rlt 0 r ∧ open_ball Y dY (apply_fun f x) r ⊆ V).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball Y dY (apply_fun f x) r ⊆ V) Hrpack).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball Y dY (apply_fun f x) r ⊆ V) (andER (r ∈ R) (Rlt 0 r ∧ open_ball Y dY (apply_fun f x) r ⊆ V) Hrpack)).
Set bx to be the term open_ball X dX x r.
We prove the intermediate claim HbxInBx: bx ∈ Bx.
We prove the intermediate claim HbxIn: bx ∈ {open_ball X dX x rr|rr ∈ R, Rlt 0 rr}.
An exact proof term for the current goal is (ReplSepI R (λrr : set ⇒ Rlt 0 rr) (λrr : set ⇒ open_ball X dX x rr) r HrR Hrpos).
An exact proof term for the current goal is (famunionI X (λx0 : set ⇒ {open_ball X dX x0 rr|rr ∈ R, Rlt 0 rr}) x bx HxX HbxIn).
We prove the intermediate claim HxInbx: x ∈ bx.
An exact proof term for the current goal is (center_in_open_ball X dX x r HdXmetric HxX Hrpos).
We use bx to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbxInBx.
Apply andI to the current goal.
An exact proof term for the current goal is HxInbx.
We will prove bx ⊆ U.
Let z be given.
Assume Hz: z ∈ bx.
We will prove z ∈ U.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (open_ballE1 X dX x r z Hz).
We prove the intermediate claim HltX: Rlt (apply_fun dX (x,z)) r.
An exact proof term for the current goal is (open_ballE2 X dX x r z Hz).
We prove the intermediate claim HxzIn: (x,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x z HxX HzX).
We prove the intermediate claim HdEq: apply_fun dX (x,z) = apply_fun dY (apply_fun f x,apply_fun f z).
We prove the intermediate claim HdXdef: dX = graph (setprod X X) (λpq : set ⇒ apply_fun dY (apply_fun f (pq 0),apply_fun f (pq 1))).
Use reflexivity.
rewrite the current goal using HdXdef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) (λpq0 : set ⇒ apply_fun dY (apply_fun f (pq0 0),apply_fun f (pq0 1))) (x,z) HxzIn) (from left to right).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
Use reflexivity.
We prove the intermediate claim HzY: apply_fun f z ∈ Y.
An exact proof term for the current goal is (Hfunf z HzX).
We prove the intermediate claim HltY: Rlt (apply_fun dY (apply_fun f x,apply_fun f z)) r.
rewrite the current goal using HdEq (from right to left).
An exact proof term for the current goal is HltX.
We prove the intermediate claim HfzBall: apply_fun f z ∈ open_ball Y dY (apply_fun f x) r.
An exact proof term for the current goal is (open_ballI Y dY (apply_fun f x) r (apply_fun f z) HzY HltY).
We prove the intermediate claim HballSub: open_ball Y dY (apply_fun f x) r ⊆ V.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball Y dY (apply_fun f x) r ⊆ V) (andER (r ∈ R) (Rlt 0 r ∧ open_ball Y dY (apply_fun f x) r ⊆ V) Hrpack)).
We prove the intermediate claim HfzV: apply_fun f z ∈ V.
An exact proof term for the current goal is (HballSub (apply_fun f z) HfzBall).
We prove the intermediate claim HgFzU: apply_fun g (apply_fun f z) ∈ U.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun f z) HfzV).
rewrite the current goal using (Hginv z HzX) (from right to left).
An exact proof term for the current goal is HgFzU.
∎