Mathlib.Topology.Metric.Basic

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning

def MetricBall.{u,v} :
  forall (X : Sort u), forall (R : Sort v), forall (dist : forall (a : X), forall (b : X), R), forall (lt : forall (a : R), forall (b : R), Prop), forall (center : X), forall (radius : R), forall (x : X), Prop :=
  fun X => fun R => fun dist => fun lt => fun center => fun radius => fun x => lt (dist center x) radius

def Neighborhood.{u} :
  forall (X : Sort u), forall (center : X), forall (domain : forall (x : X), Prop), Prop :=
  fun X => fun center => fun domain => domain center

def LocalMem.{u} :
  forall (X : Sort u), forall (domain : forall (x : X), Prop), forall (x : X), Prop :=
  fun X => fun domain => fun x => domain x

def LocalPred.{u} :
  forall (X : Sort u), forall (domain : forall (x : X), Prop), forall (P : forall (x : X), Prop), Prop :=
  fun X => fun domain => fun P => forall (x : X), forall (hx : domain x), P x

def LocalEq.{u,v} :
  forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (f : forall (x : X), Y), forall (g : forall (x : X), Y), Prop :=
  fun X => fun Y => fun domain => fun f => fun g => forall (x : X), forall (hx : domain x), @Eq.{v} Y (f x) (g x)

def LocalUnique.{u,v} :
  forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (predicate : forall (x : X), forall (y : Y), Prop), forall (candidate : forall (x : X), Y), Prop :=
  fun X => fun Y => fun domain => fun predicate => fun candidate => forall (other : forall (x : X), Y), forall (other_sol : forall (x : X), forall (hx : domain x), predicate x (other x)), forall (candidate_sol : forall (x : X), forall (hx : domain x), predicate x (candidate x)), @LocalEq.{u,v} X Y domain other candidate

theorem metric_ball_intro.{u,v} :
  forall (X : Sort u), forall (R : Sort v), forall (dist : forall (a : X), forall (b : X), R), forall (lt : forall (a : R), forall (b : R), Prop), forall (center : X), forall (radius : R), forall (x : X), forall (h : lt (dist center x) radius), @MetricBall.{u,v} X R dist lt center radius x :=
  fun X => fun R => fun dist => fun lt => fun center => fun radius => fun x => fun h => h

theorem metric_ball_elim.{u,v} :
  forall (X : Sort u), forall (R : Sort v), forall (dist : forall (a : X), forall (b : X), R), forall (lt : forall (a : R), forall (b : R), Prop), forall (center : X), forall (radius : R), forall (x : X), forall (h : @MetricBall.{u,v} X R dist lt center radius x), lt (dist center x) radius :=
  fun X => fun R => fun dist => fun lt => fun center => fun radius => fun x => fun h => h

theorem neighborhood_intro.{u} :
  forall (X : Sort u), forall (center : X), forall (domain : forall (x : X), Prop), forall (h : domain center), @Neighborhood.{u} X center domain :=
  fun X => fun center => fun domain => fun h => h

theorem neighborhood_center.{u} :
  forall (X : Sort u), forall (center : X), forall (domain : forall (x : X), Prop), forall (h : @Neighborhood.{u} X center domain), domain center :=
  fun X => fun center => fun domain => fun h => h

theorem neighborhood_shrink.{u} :
  forall (X : Sort u), forall (center : X), forall (larger : forall (x : X), Prop), forall (smaller : forall (x : X), Prop), forall (sub : forall (x : X), forall (hx : smaller x), larger x), forall (h : @Neighborhood.{u} X center smaller), @Neighborhood.{u} X center larger :=
  fun X => fun center => fun larger => fun smaller => fun sub => fun h => sub center h

theorem local_mem_intro.{u} :
  forall (X : Sort u), forall (domain : forall (x : X), Prop), forall (x : X), forall (h : domain x), @LocalMem.{u} X domain x :=
  fun X => fun domain => fun x => fun h => h

theorem local_mem_elim.{u} :
  forall (X : Sort u), forall (domain : forall (x : X), Prop), forall (x : X), forall (h : @LocalMem.{u} X domain x), domain x :=
  fun X => fun domain => fun x => fun h => h

theorem local_pred_intro.{u} :
  forall (X : Sort u), forall (domain : forall (x : X), Prop), forall (P : forall (x : X), Prop), forall (h : forall (x : X), forall (hx : domain x), P x), @LocalPred.{u} X domain P :=
  fun X => fun domain => fun P => fun h => h

theorem local_pred_apply.{u} :
  forall (X : Sort u), forall (domain : forall (x : X), Prop), forall (P : forall (x : X), Prop), forall (local : @LocalPred.{u} X domain P), forall (x : X), forall (hx : domain x), P x :=
  fun X => fun domain => fun P => fun local => fun x => fun hx => local x hx

theorem local_pred_shrink.{u} :
  forall (X : Sort u), forall (larger : forall (x : X), Prop), forall (smaller : forall (x : X), Prop), forall (P : forall (x : X), Prop), forall (sub : forall (x : X), forall (hx : smaller x), larger x), forall (local : @LocalPred.{u} X larger P), @LocalPred.{u} X smaller P :=
  fun X => fun larger => fun smaller => fun P => fun sub => fun local => fun (x : X) => fun (hx : smaller x) => local x (sub x hx)

theorem metric_ball_mono.{u,v} :
  forall (X : Sort u), forall (R : Sort v), forall (dist : forall (a : X), forall (b : X), R), forall (lt : forall (a : R), forall (b : R), Prop), forall (center : X), forall (r1 : R), forall (r2 : R), forall (h_le : forall (x : X), forall (hx : @MetricBall.{u,v} X R dist lt center r1 x), @MetricBall.{u,v} X R dist lt center r2 x), @LocalPred.{u} X (@MetricBall.{u,v} X R dist lt center r1) (@MetricBall.{u,v} X R dist lt center r2) :=
  fun X => fun R => fun dist => fun lt => fun center => fun r1 => fun r2 => fun h_le => fun (x : X) => fun (hx : @MetricBall.{u,v} X R dist lt center r1 x) => h_le x hx

theorem local_eq_refl.{u,v} :
  forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (f : forall (x : X), Y), @LocalEq.{u,v} X Y domain f f :=
  fun X => fun Y => fun domain => fun f => fun (x : X) => fun (hx : domain x) => @Eq.refl.{v} Y (f x)

theorem local_eq_symm.{u,v} :
  forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (f : forall (x : X), Y), forall (g : forall (x : X), Y), forall (h : @LocalEq.{u,v} X Y domain f g), @LocalEq.{u,v} X Y domain g f :=
  fun X => fun Y => fun domain => fun f => fun g => fun h => fun (x : X) => fun (hx : domain x) => @eq_symm.{v} Y (f x) (g x) (h x hx)

theorem local_eq_trans.{u,v} :
  forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (f : forall (x : X), Y), forall (g : forall (x : X), Y), forall (k : forall (x : X), Y), forall (hfg : @LocalEq.{u,v} X Y domain f g), forall (hgk : @LocalEq.{u,v} X Y domain g k), @LocalEq.{u,v} X Y domain f k :=
  fun X => fun Y => fun domain => fun f => fun g => fun k => fun hfg => fun hgk => fun (x : X) => fun (hx : domain x) => @eq_trans.{v} Y (f x) (g x) (k x) (hfg x hx) (hgk x hx)

theorem local_unique_apply.{u,v} :
  forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (predicate : forall (x : X), forall (y : Y), Prop), forall (candidate : forall (x : X), Y), forall (uniq : @LocalUnique.{u,v} X Y domain predicate candidate), forall (other : forall (x : X), Y), forall (other_sol : forall (x : X), forall (hx : domain x), predicate x (other x)), forall (candidate_sol : forall (x : X), forall (hx : domain x), predicate x (candidate x)), @LocalEq.{u,v} X Y domain other candidate :=
  fun X => fun Y => fun domain => fun predicate => fun candidate => fun uniq => fun other => fun other_sol => fun candidate_sol => uniq other other_sol candidate_sol