Let X, Tx, Y, dY, F, g and a be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Assume HFsubC: F ⊆ continuous_function_space X Tx Y (metric_topology Y dY).
Assume Hgcl: g ∈ Ascoli_g_pointwise_closure X Tx Y dY F.
Assume HaX: a ∈ X.
Set Ty to be the term metric_topology Y dY.
Set Dom to be the term function_space X Y.
Set Tpt to be the term pointwise_convergence_topology X Tx Y Ty.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
We prove the intermediate claim HTpt: topology_on Dom Tpt.
An exact proof term for the current goal is (pointwise_convergence_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HFsubDom: F ⊆ Dom.
Let f be given.
Assume HfF: f ∈ F.
We prove the intermediate claim HfC: f ∈ continuous_function_space X Tx Y Ty.
An exact proof term for the current goal is (HFsubC f HfF).
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f HfC).
Set evala to be the term graph Dom (λf : set ⇒ apply_fun f a).
We prove the intermediate claim Hevala_cont: continuous_map Dom Tpt Y Ty evala.
An exact proof term for the current goal is (pointwise_eval_continuous X Tx Y Ty a HTx HTy HaX).
We prove the intermediate claim Himg: apply_fun evala g ∈ closure_of Y Ty (Repl F (λf : set ⇒ apply_fun evala f)).
An exact proof term for the current goal is (continuous_map_image_of_closure_subset_closure_of_image Dom Tpt Y Ty evala F g HTpt HTy Hevala_cont HFsubDom Hgcl).
We prove the intermediate claim Hevala_g: apply_fun evala g = apply_fun g a.
We prove the intermediate claim HgDom: g ∈ Dom.
An exact proof term for the current goal is (Ascoli_g_pointwise_closure_sub X Tx Y dY F HTpt g Hgcl).
rewrite the current goal using (apply_fun_graph Dom (λf : set ⇒ apply_fun f a) g HgDom) (from left to right).
Use reflexivity.
rewrite the current goal using Hevala_g (from right to left).
rewrite the current goal using (Ascoli_F_at_def X Y a F) (from left to right).
We prove the intermediate claim HReplEq: Repl F (λf : set ⇒ apply_fun evala f) = Repl F (λf : set ⇒ apply_fun f a).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ Repl F (λf : set ⇒ apply_fun evala f).
Apply (ReplE_impred F (λf : set ⇒ apply_fun evala f) y Hy) to the current goal.
Let f be given.
Assume HfF: f ∈ F.
Assume Hyeq: y = apply_fun evala f.
We will prove y ∈ Repl F (λf : set ⇒ apply_fun f a).
We prove the intermediate claim HfDom: f ∈ Dom.
An exact proof term for the current goal is (HFsubDom f HfF).
We prove the intermediate claim Hevalaf: apply_fun evala f = apply_fun f a.
rewrite the current goal using (apply_fun_graph Dom (λf0 : set ⇒ apply_fun f0 a) f HfDom) (from left to right).
Use reflexivity.
rewrite the current goal using Hyeq (from left to right).
rewrite the current goal using Hevalaf (from left to right).
An exact proof term for the current goal is (ReplI F (λf0 : set ⇒ apply_fun f0 a) f HfF).
Let y be given.
Assume Hy: y ∈ Repl F (λf : set ⇒ apply_fun f a).
Apply (ReplE_impred F (λf : set ⇒ apply_fun f a) y Hy) to the current goal.
Let f be given.
Assume HfF: f ∈ F.
Assume Hyeq: y = apply_fun f a.
We will prove y ∈ Repl F (λf : set ⇒ apply_fun evala f).
We prove the intermediate claim HfDom: f ∈ Dom.
An exact proof term for the current goal is (HFsubDom f HfF).
We prove the intermediate claim Hevalaf: apply_fun evala f = apply_fun f a.
rewrite the current goal using (apply_fun_graph Dom (λf0 : set ⇒ apply_fun f0 a) f HfDom) (from left to right).
Use reflexivity.
rewrite the current goal using Hyeq (from left to right).
rewrite the current goal using Hevalaf (from right to left).
An exact proof term for the current goal is (ReplI F (λf0 : set ⇒ apply_fun evala f0) f HfF).
rewrite the current goal using HReplEq (from right to left).
An exact proof term for the current goal is Himg.
∎