\import Algebra.Meta
\import Algebra.Monoid
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Function()
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Product
\import Topology.MetricSpace
\import Topology.NormedAbGroup.Real
\import Topology.NormedAbGroup.Real.Functions
\import Topology.TopAbGroup.Product
\import Topology.TopSpace
\import Topology.TopSpace.Product
\import Topology.UniformSpace
\import Topology.UniformSpace.Complete

\func dense-metric-lift {X Y : MetricSpace} {Z : CompleteMetricSpace} (f : IsometricMap X Y) (fd : f.IsDense) (g : MetricMap X Z) : MetricMap Y Z \cowith
  | UniformMap => dense-uniform-lift f (f.dense->uniformEmbedding fd) g
  | func-dist {y} {y'} =>
    \have | g~ : UniformMap Y Z => dense-uniform-lift f (f.dense->uniformEmbedding fd) g
          | g-char {x} : g~ (f x) = g x => dense-lift-char (fd, f.embedding->coverEmbedding (f.dense->uniformEmbedding fd).) x
    \in Function.id {dist (g~ y) (g~ y') <= dist y y'} $ RealAbGroup.meet_<=' $ dense-lift-unique (prod f f) (prod.isDense fd fd) (real-meet-uniform ∘ tuple (dist-uniform-map ∘ prod g~ g~) dist-uniform-map) (dist-uniform-map ∘ prod g~ g~)
          (\lam (x,x') => Function.id {dist (g~ (f x)) (g~ (f x')) ∧ dist (f x) (f x') = dist (g~ (f x)) (g~ (f x'))} $ rewrite (g-char,g-char) $ RealAbGroup.meet_<= $ later $ rewrite f.func-isometry g.func-dist) (y,y')
  \where {
    \open ProductTopSpace
    \open ContMap
  }

\instance MetricCompletion (X : PseudoMetricSpace) : CompleteMetricSpace
  | CompleteUniformSpace => UniformCompletion X
  | dist x y => dist-cover (x,y)
  | dist-refl => dist-refl-lem
  | dist-symm {y} {y'} => dense-lift-unique (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding). dist-cover (dist-cover ∘ tuple proj2 proj1) (\lam x => dist-char *> dist-symm *> inv dist-char) (y,y')
  | dist-triang => filter-dist-triang _ _ _
  | dist-uniform => dist-uniform-lem
  | dist-ext {F} {G} FG=0 => isSeparatedCoverSpace $ UniformSpace.uniform-separated. $ later \case dist-uniform-lem. __ \with {
    | inP (eps,eps>0,h) => later \case h F \with {
      | inP (U,CU,g) => inP (U, CU, (g $ rewrite dist-refl-lem eps>0, g $ rewrite FG=0 eps>0))
    }
  }
  \where {
    \open ProductCoverSpace
    \open CoverMap

    \sfunc dist-cover : CoverMap (Completion X ⨯ Completion X) RealNormed
      => dense-lift (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) dist-uniform-map

    \lemma dist-char {x y : X} : dist-cover (pointCF x, pointCF y) = dist x y
      => rewrite (\peval dist-cover) $ dense-lift-char (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) (x,y)

    \private \lemma dist-refl-lem {F : RegularCauchyFilter X} : dist-cover (F, F) = ( : Real)
      => dense-lift-unique completion completion.isDenseEmbedding. (dist-cover ∘ tuple id id) (const ) (\lam x => dist-char *> dist-refl) F

    \private \lemma dist-uniform-lem {C : Set (Set (Completion X))} : isUniform C <-> ∃ (eps : Real) ( < eps) ∀ x ∃ (U : C) ∀ {y} (dist-cover (x,y) < eps -> U y)
      => (later \lam (inP (D,Du,g)) => \case dist-uniform. Du \with {
        | inP (eps,eps>0,h) => inP (halfs  eps, halfs>0  eps>0, \lam F => \case isCauchyFilter (X.makeCauchy $ X.makeUniform (halfs>0  eps>0)) \with {
          | inP (_, inP (x,idp), Fx) => \case h x \with {
            | inP (V,DV,Vd) => \case g DV \with {
              | inP (U,CU,VU) => inP (U, CU, \lam {G} d => \case isCauchyFilter (X.makeCauchy $ X.makeUniform (halfs>0  eps>0)) \with {
                | inP (_, inP (y,idp), Gy) => VU $ filter-mono (later \lam {z} d' => Vd
                    \have | t => dist-neighborhood (pointCF x) F (halfs>0  eps>0) (OBall-center_<=< $ halfs>0  eps>0) Fx
                          | s => dist-neighborhood G (pointCF y) (halfs>0  eps>0) Gy (OBall-center_<=< $ halfs>0  eps>0)
                    \in rewriteI dist-char $ rewriteI dist-char at d' $ linarith (filter-dist-triang (pointCF x) F (pointCF z), filter-dist-triang F G (pointCF z), filter-dist-triang G (pointCF y) (pointCF z))) Gy
              })
            }
          }
        })
      }, \lam (inP (eps,eps>0,h)) => inP (_, X.makeUniform {half (half eps)} $ half>0 $ half>0 eps>0, \lam {_} (inP (x,idp)) => \case h (pointCF x) \with {
        | inP (U,CU,g) => inP (U, CU, \lam {F} Fx => g $ dist-neighborhood _ _ eps>0 {x} (OBall-center_<=< $ half>0 $ half>0 eps>0) Fx)
      }))

    \lemma filter-dist-triang (x y z : RegularCauchyFilter X) : dist-cover (x,z) <= dist-cover (x,y) + dist-cover (y,z)
      => RealAbGroup.meet_<=' $ dense-lift-unique (prod (prod completion completion) completion) (prod.isDenseEmbedding (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) completion.isDenseEmbedding).
          (real-meet-uniform ∘ tuple (dist-cover ∘ prod proj1 id) (+-uniform ∘ tuple (dist-cover ∘ proj1) (dist-cover ∘ prod proj2 id)))
          (dist-cover ∘ prod proj1 id)
          (\lam ((x,y),z) => Function.id {dist-cover (pointCF x, pointCF z) ∧ (dist-cover (pointCF x, pointCF y) + dist-cover (pointCF y, pointCF z)) = dist-cover (pointCF x, pointCF z)} $
            rewrite (dist-char,dist-char,dist-char) $ RealAbGroup.meet_<= dist-triang)
          ((x,y),z)

    \lemma dist-neighborhood (F G : RegularCauchyFilter X) {eps : Real} (eps>0 :  < eps) {x : X} (Fx : F (OBall (half (half eps)) x)) (Gx : G (OBall (half (half eps)) x)) : dist-cover (F,G) < eps
      => rewrite (\peval dist-cover) $ simplify in RealAbGroup.abs>=_- <∘r <=<_<= ((completion-lift-neighborhood2 (dist-uniform-map {X}) F G (OBall eps )). $ inP
          (OBall (half eps) , <=*_<=< $ OBall_<=* (half<id eps>0), _, Fx, _, Gx, \lam {z1} d1 {z2} d2 => RealAbGroup.abs_-_< (linarith (dist>=0 {X} {z1}, half>0 eps>0)) $ simplify $ halving d1 d2)) idp
  }