Inequalities with ENNReals

Stream: mathlib4

[Connor Gordon]

I'm trying to prove some edist inequalities in a metric space, and I'm having some trouble getting ENNReals to cooperate. In particular, with this code

import Mathlib.Topology.MetricSpace.Polish
import Mathlib.MeasureTheory.Constructions.Polish
import Mathlib.Topology.MetricSpace.CantorScheme
import Mathlib.Topology.Bases
import Mathlib.Data.Nat.Pairing

variable {α : Type*} [mα : MeasurableSpace α] [tα : MetricSpace α]
  [sα : TopologicalSpace.SeparableSpace α]
variable {β : Type*} [mβ : MeasurableSpace β] [tβ : MetricSpace β]
  [sβ : TopologicalSpace.SeparableSpace β]
variable {f : α → β} (fmeas : Measurable f)

def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}

open TopologicalSpace

lemma decomp_of_sq_minus_diag {u : Set α} {ε : ENNReal} (uclosed : IsClosed u)
  (unonempty : Set.Nonempty u) (εpos : ε > 0)
  : ∃ v : ℕ → Set α, ∃ w : ℕ → Set α,
  sq_minus_diag u = ⋃ n : ℕ, v n ×ˢ w n
  ∧ (∀ n : ℕ, (v n) ⊆ u) ∧ (∀ n : ℕ, (w n) ⊆ u)
  ∧ (∀ n : ℕ, IsClosed (v n)) ∧ (∀ n : ℕ, IsClosed (w n))
  ∧ (∀ n : ℕ, EMetric.diam (v n) ≤ ε)
  ∧ (∀ n : ℕ, EMetric.diam (w n) ≤ ε)
  ∧ (∀ n : ℕ, v n ≠ w n)
  := by
    -- Prove u is separable
    have Usep : SeparableSpace u := by
      apply IsSeparable.separableSpace
      rw[IsSeparable]
      choose D Dctbl Ddense using exists_countable_dense α
      use D
      constructor
      exact Dctbl
      unfold Dense at Ddense
      intro x _
      exact Ddense x
    -- Pick a dense sequence from u
    have unonempty : Nonempty u := by
      rw[Set.nonempty_iff_ne_empty', ←Set.nonempty_iff_ne_empty]
      exact unonempty
    choose D Ddense using exists_dense_seq u
    -- Define v and w
    let v (n : ℕ × ℕ) : Set α := if edist (D n.1) (D n.2) = 0 then ∅ else
      u ∩ EMetric.closedBall (D n.1) (min (ε/2) (1/3 * edist (D n.1) (D n.2)))
    let w (n : ℕ × ℕ) : Set α := if edist (D n.1) (D n.2) = 0 then u else
      u ∩ EMetric.closedBall (D n.2) (min (ε/2) (1/3 * edist (D n.1) (D n.2)))
    -- Prove the decomposition works
    have hdecomp : ⋃ n : ℕ × ℕ, v n ×ˢ w n = sq_minus_diag u := by
      ext x; constructor
      . intro hx
        rw[Set.mem_iUnion] at hx
        cases' hx with i hi
        dsimp at hi; split at hi
        . simp only [Set.empty_prod, Set.mem_empty_iff_false] at hi
        simp only [ge_iff_le, Set.mem_prod, Set.mem_inter_iff,
          EMetric.mem_closedBall, le_min_iff] at hi
        simp only [sq_minus_diag, ne_eq, Set.mem_setOf_eq]
        constructor; exact hi.1.1; constructor; exact hi.2.1
        rw[←edist_eq_zero]
        intro hdist
        have hcont := edist_triangle4 (D i.1 : α) x.1 x.2 (D i.2)
        rw [hdist] at hcont
        have hcont2 := add_le_add hi.1.2.2 hi.2.2.2
        simp only [add_zero] at hcont hcont2
        rw[edist_comm] at hcont2
        have hcont3 := le_trans hcont hcont2
        ring_nf at hcont3
        sorry -- This one
      sorry
    sorry

I've managed to reduce my first goal (the marked sorry) to proving that it's a problem that edist x y ≤ (1/3) * edist x y * 2 when we know edist x y ≠ 0. When I initially proved this for dist, ​le_mul_iff_one_le_left was very useful, but it doesn't work for ENNReals. Any ideas what I could do?

[Damiano Testa]

In the web-browser, the dsimp on line 54 makes no progress.

[Martin Dvořák]

BTW, I spent most of today implementing ENNRat:
https://github.com/madvorak/vcsp/blob/main/VCSP/ENNRationals.lean

I wasn't planning to contribute them to Mathlib, but I wanted them for some side quests in my project.

[Connor Gordon]

Damiano Testa said:

In the web-browser, the dsimp on line 54 makes no progress.

That's really weird, it does on my end (in vscode). It's meant to unpack the definition of v and w, and unfold was getting mad at me.

[Richard Copley]

That difference is down to a relatively recent change in dsimp (and simp). You can use dsimp [v, w] or unfold_let v w.

[Connor Gordon]

I've done a lot more work, and I've reduced the problem to a bunch of sorrys that feel like they should be immediate/fast, but I don't know how to do them. I've annotated each one with what needs to be proved. If anyone has any ideas on how I could accomplish some or all of these they would be greatly appreciated. (Also needed to sorry out some things to meet the character limit; also annotated those.)

import Mathlib.Topology.MetricSpace.Polish
import Mathlib.MeasureTheory.Constructions.Polish
import Mathlib.Topology.MetricSpace.CantorScheme
import Mathlib.Topology.Bases
import Mathlib.Data.Nat.Pairing

variable {α : Type*} [mα : MeasurableSpace α] [tα : MetricSpace α]
  [sα : TopologicalSpace.SeparableSpace α]
variable {β : Type*} [mβ : MeasurableSpace β] [tβ : MetricSpace β]
  [sβ : TopologicalSpace.SeparableSpace β]
variable {f : α → β} (fmeas : Measurable f)

def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}

open TopologicalSpace

lemma denseRange_aux {γ : Type*} [MetricSpace γ] {f : ℕ → γ} :
  DenseRange f → ∀ x, ∀ r : ENNReal,
  r > 0 → ∃ y, edist x (f y) < r := by
    sorry -- Done; removed for length

lemma decomp_of_sq_minus_diag {u : Set α} {ε : ENNReal} (uclosed : IsClosed u)
  (unonempty : Set.Nonempty u) (εpos : ε > 0)
  : ∃ v : ℕ → Set α, ∃ w : ℕ → Set α,
  sq_minus_diag u = ⋃ n : ℕ, v n ×ˢ w n
  ∧ (∀ n : ℕ, (v n) ⊆ u) ∧ (∀ n : ℕ, (w n) ⊆ u)
  ∧ (∀ n : ℕ, IsClosed (v n)) ∧ (∀ n : ℕ, IsClosed (w n))
  ∧ (∀ n : ℕ, EMetric.diam (v n) ≤ ε)
  ∧ (∀ n : ℕ, EMetric.diam (w n) ≤ ε)
  ∧ (∀ n : ℕ, v n ≠ w n)
  := by
    -- Pick a point in u (to be used later)
    have unonempty' := unonempty
    choose x0 hx0 using unonempty'
    -- Prove u is separable
    have Usep : SeparableSpace u := by
      apply IsSeparable.separableSpace
      rw[IsSeparable]
      choose D Dctbl Ddense using exists_countable_dense α
      use D
      constructor
      exact Dctbl
      unfold Dense at Ddense
      intro x _
      exact Ddense x
    -- Pick a dense sequence from u
    have unonempty : Nonempty u := by
      rw[Set.nonempty_iff_ne_empty', ←Set.nonempty_iff_ne_empty]
      exact unonempty
    choose D Ddense using exists_dense_seq u
    -- Define v and w
    let v (n : ℕ × ℕ) : Set α := if edist (D n.1) (D n.2) = 0 then ∅ else
      u ∩ EMetric.closedBall (D n.1) (min (ε/2) (1/3 * edist (D n.1) (D n.2)))
    let w (n : ℕ × ℕ) : Set α := if edist (D n.1) (D n.2) = 0 then {x0} else
      u ∩ EMetric.closedBall (D n.2) (min (ε/2) (1/3 * edist (D n.1) (D n.2)))
    -- Prove the decomposition works
    have hdecomp : ⋃ n : ℕ × ℕ, v n ×ˢ w n = sq_minus_diag u := by
      ext x; constructor
      . intro hx
        rw[Set.mem_iUnion] at hx
        cases' hx with i hi
        simp only at hi; split at hi
        . simp only [Set.empty_prod, Set.mem_empty_iff_false] at hi
        simp only [ge_iff_le, Set.mem_prod, Set.mem_inter_iff,
          EMetric.mem_closedBall, le_min_iff] at hi
        simp only [sq_minus_diag, ne_eq, Set.mem_setOf_eq]
        constructor; exact hi.1.1; constructor; exact hi.2.1
        rw[←edist_eq_zero]
        intro hdist
        have hcont := edist_triangle4 (D i.1 : α) x.1 x.2 (D i.2)
        rw [hdist] at hcont
        have hcont2 := add_le_add hi.1.2.2 hi.2.2.2
        simp only [add_zero] at hcont hcont2
        rw[edist_comm] at hcont2
        have hcont3 := le_trans hcont hcont2
        ring_nf at hcont3
        rw[mul_comm, ←mul_assoc] at hcont3
        sorry -- need x ≤ 2/3 * x is a contradiction for nonzero, non-infinity x
      intro hx
      simp only [sq_minus_diag, ne_eq, Set.mem_setOf_eq] at hx
      rcases hx with ⟨hx1, hx2, hne⟩
      set r := edist x.1 x.2
      have : min (ε/2) (r/6) > 0 := by
        apply lt_min
        simp only [ENNReal.div_pos_iff, and_true]
        exact ne_of_gt εpos
        simp only [ENNReal.div_pos_iff, ne_eq, edist_eq_zero, and_true]
        exact hne
      choose a ha using denseRange_aux Ddense ⟨x.1, hx1⟩ (min (ε/2) (r/6)) this
      choose b hb using denseRange_aux Ddense ⟨x.2, hx2⟩ (min (ε/2) (r/6)) this
      rw[Set.mem_iUnion]
      use (a,b)
      have hab : D a ≠ D b := by
        intro heq
        rw[←zero_eq_edist] at heq
        have hcont := edist_triangle4 x.1 (D a : α) (D b) x.2
        have : edist x.1 x.2 ≤ 2/6 * edist x.1 x.2 := by
          apply le_trans hcont _
          have aux1 : edist x.1 (D a : α) ≤ r/6 := by
            exact le_trans (le_of_lt ha) (min_le_right _ _)
          have aux2 : edist (D a : α) (D b) ≤ 0 := le_of_eq heq.symm
          have aux3 : edist (D b : α) x.2 ≤ r/6 := by
            rw[edist_comm]
            exact le_trans (le_of_lt hb) (min_le_right _ _)
          have ineq2 := add_le_add (add_le_add aux1 aux2) aux3
          apply le_trans ineq2 _
          apply le_of_eq
          ring_nf
          sorry -- need x/6 * 2 = (2/6) * x
        sorry -- need x ≤ 2/6 * x is a contradiction for nonzero, non-infinity x
      simp only [edist_eq_zero, ge_iff_le, Set.mem_prod,
        Set.mem_ite_empty_left, Set.mem_inter_iff,
        EMetric.mem_closedBall, le_min_iff]
      constructor
      . constructor; exact hab
        constructor; exact hx1
        constructor; exact le_trans (le_of_lt ha) (min_le_left _ _)
        apply le_of_not_gt
        intro hdist; rw[gt_iff_lt] at hdist
        have hdist : edist (D a : α) (D b) ≤ 3 * edist x.1 (D a : α) := by
          sorry -- need to multiply both sides of the old hdist by 3
        have hcont := edist_triangle4 x.1 (D a : α) (D b) x.2
        have : edist x.1 x.2 ≤ 5/6 * edist x.1 x.2 := by
          apply le_trans hcont
          have aux1 : edist x.1 (D a : α) ≤ r/6 := by
            exact le_trans (le_of_lt ha) (min_le_right _ _)
          have aux2 : edist (D a : α) (D b) ≤ 3 * r/6 := by
            apply le_trans hdist
            sorry -- need to multiply both sides of aux1 by 3
          have aux3 : edist (D b : α) x.2 ≤ r/6 := by
            rw[edist_comm]; exact le_trans (le_of_lt hb) (min_le_right _ _)
          have ineq2 := add_le_add (add_le_add aux1 aux2) aux3
          apply le_trans ineq2 _
          ring_nf
          apply le_of_eq
          sorry -- need x/6 * 2 + x*3/6 = 5/6 * x
        sorry -- need x ≤ 5/6 * x is a contradiction for nonzero, non-infinity x
      rw[ne_eq, ←edist_eq_zero] at hab
      rw[if_neg hab]
      apply Set.mem_inter
      exact hx2
      rw[EMetric.mem_closedBall]
      apply le_trans (le_of_lt hb) _
      apply min_le_min
      exact Eq.ge rfl
      apply le_of_not_gt
      intro hdist; rw[gt_iff_lt] at hdist
      have hdist : edist (D a : α) (D b) ≤ 3 * edist x.1 (D a : α) := by
        sorry -- need to multiply both sides of the old hdist by 3
      have hcont := edist_triangle4 x.1 (D a : α) (D b) x.2
      have : edist x.1 x.2 ≤ 5/6 * edist x.1 x.2 := by
        apply le_trans hcont
        have aux1 : edist x.1 (D a : α) ≤ r/6 := by
          exact le_trans (le_of_lt ha) (min_le_right _ _)
        have aux2 : edist (D a : α) (D b) ≤ 3 * r/6 := by
          apply le_trans hdist
          sorry -- need to multiply both sides of aux1 by 3
        have aux3 : edist (D b : α) x.2 ≤ r/6 := by
          rw[edist_comm]; exact le_trans (le_of_lt hb) (min_le_right _ _)
        have ineq2 := add_le_add (add_le_add aux1 aux2) aux3
        apply le_trans ineq2 _
        ring_nf
        apply le_of_eq
        sorry -- need x/6 * 2 + x*3/6 = 5/6 * x
      sorry -- need x ≤ 5/6 * x is a contradiction for nonzero, non-infinity x
    let v' (n : ℕ) : Set α := v (Nat.unpair n)
    let w' (n : ℕ) : Set α := w (Nat.unpair n)
    use v'
    use w'
    constructor
    -- Prove the decomposition works
    . rw[←hdecomp]
      ext x; constructor
      . intro hx
        rw[Set.mem_iUnion] at hx ⊢
        cases' hx with n hn
        use Nat.pair n.1 n.2
        simp only [Nat.unpair_pair] at hn ⊢
        exact hn
      intro hx
      rw[Set.mem_iUnion] at hx ⊢
      cases' hx with n hn
      use Nat.unpair n
    constructor
    -- Prove v n is a subset of u
    . intro n; simp only; split
      exact Set.empty_subset u
      exact Set.inter_subset_left _ _
    constructor
    -- Prove w n in a subset of u
    . intro n; simp only; split
      intro x hx; rw[Set.mem_singleton_iff] at hx; rw [hx]; exact hx0
      exact Set.inter_subset_left _ _
    constructor
    -- Prove v n is closed
    . intro n; simp only; split
      exact isClosed_empty
      apply IsClosed.inter
      exact uclosed
      exact EMetric.isClosed_ball
    constructor
    -- Prove w n is closed
    . intro n; simp only; split
      exact T1Space.t1 x0
      apply IsClosed.inter
      exact uclosed
      exact EMetric.isClosed_ball
    constructor
    -- Prove v n has small diameter
    . sorry -- Done; removed for length
    constructor
    -- Prove w n has small diameter
    . sorry -- Done; removed for length
    -- Prove v n ≠ w n
    intro n; simp only; split
    . have := Set.singleton_nonempty x0
      exact (Set.Nonempty.ne_empty this).symm
    have : (D (Nat.unpair n).fst : α) ∉ u ∩ EMetric.closedBall
      (D (Nat.unpair n).snd : α) (min (ε / 2) (1 / 3 *
      edist (D (Nat.unpair n).fst) (D (Nat.unpair n).snd))) := by
      intro hcont
      rw[Set.mem_inter_iff, EMetric.mem_closedBall] at hcont
      rcases hcont with ⟨_, hcont⟩
      have hcont := le_trans hcont (min_le_right _ _)
      sorry -- need x ≤ 1/3 * x is a contradiction for nonzero, non-infinity x
    rw[ne_eq, subset_antisymm_iff, not_and_or]
    apply Or.inl
    rw[Set.not_subset]
    use (D (Nat.unpair n).1 : α)
    constructor
    . apply Set.mem_inter
      exact Subtype.mem (D (Nat.unpair n).fst)
      exact EMetric.mem_closedBall_self
    exact this

[Rida Hamadani]

When I open this in Lean 4 Playground, I get a bunch of errors, such as tactic 'split' failed at line 62.

[Connor Gordon]

That's rather unfortunate, it seems that I may have an outdated version of lean/mathlib even though I thought I updated it, because it's all fine on my end. I'll see what I can do and try to fix it

[Rida Hamadani]

I suggest trying to see if your code runs successfully here first, that way you verify that it will work on our side too.

[Connor Gordon]

Ah, thank you for the link; I'd never heard of that before. Will test there going forward. In any case, here's a correct version that works on the website; seems like the simp issue persisted, although it should be good now.

import Mathlib.Topology.MetricSpace.Polish
import Mathlib.MeasureTheory.Constructions.Polish
import Mathlib.Topology.MetricSpace.CantorScheme
import Mathlib.Topology.Bases
import Mathlib.Data.Nat.Pairing

variable {α : Type*} [mα : MeasurableSpace α] [tα : MetricSpace α]
  [sα : TopologicalSpace.SeparableSpace α]
variable {β : Type*} [mβ : MeasurableSpace β] [tβ : MetricSpace β]
  [sβ : TopologicalSpace.SeparableSpace β]
variable {f : α → β} (fmeas : Measurable f)

def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}

open TopologicalSpace

lemma denseRange_aux {γ : Type*} [MetricSpace γ] {f : ℕ → γ} :
  DenseRange f → ∀ x, ∀ r : ENNReal,
  r > 0 → ∃ y, edist x (f y) < r := by
    sorry -- Done

lemma decomp_of_sq_minus_diag {u : Set α} {ε : ENNReal} (uclosed : IsClosed u)
  (unonempty : Set.Nonempty u) (εpos : ε > 0)
  : ∃ v : ℕ → Set α, ∃ w : ℕ → Set α,
  sq_minus_diag u = ⋃ n : ℕ, v n ×ˢ w n
  ∧ (∀ n : ℕ, (v n) ⊆ u) ∧ (∀ n : ℕ, (w n) ⊆ u)
  ∧ (∀ n : ℕ, IsClosed (v n)) ∧ (∀ n : ℕ, IsClosed (w n))
  ∧ (∀ n : ℕ, EMetric.diam (v n) ≤ ε)
  ∧ (∀ n : ℕ, EMetric.diam (w n) ≤ ε)
  ∧ (∀ n : ℕ, v n ≠ w n)
  := by
    -- Pick a point in u (to be used later)
    have unonempty' := unonempty
    choose x0 hx0 using unonempty'
    -- Prove u is separable
    have Usep : SeparableSpace u := by
      apply IsSeparable.separableSpace
      rw[IsSeparable]
      choose D Dctbl Ddense using exists_countable_dense α
      use D
      constructor
      exact Dctbl
      unfold Dense at Ddense
      intro x _
      exact Ddense x
    -- Pick a dense sequence from u
    have unonempty : Nonempty u := by
      rw[Set.nonempty_iff_ne_empty', ←Set.nonempty_iff_ne_empty]
      exact unonempty
    choose D Ddense using exists_dense_seq u
    -- Define v and w
    let v (n : ℕ × ℕ) : Set α := if edist (D n.1) (D n.2) = 0 then ∅ else
      u ∩ EMetric.closedBall (D n.1) (min (ε/2) (1/3 * edist (D n.1) (D n.2)))
    let w (n : ℕ × ℕ) : Set α := if edist (D n.1) (D n.2) = 0 then {x0} else
      u ∩ EMetric.closedBall (D n.2) (min (ε/2) (1/3 * edist (D n.1) (D n.2)))
    -- Prove the decomposition works
    have hdecomp : ⋃ n : ℕ × ℕ, v n ×ˢ w n = sq_minus_diag u := by
      ext x; constructor
      . intro hx
        rw[Set.mem_iUnion] at hx
        cases' hx with i hi
        dsimp [v,w] at hi; split at hi
        . simp only [Set.empty_prod, Set.mem_empty_iff_false] at hi
        simp only [ge_iff_le, Set.mem_prod, Set.mem_inter_iff,
          EMetric.mem_closedBall, le_min_iff] at hi
        simp only [sq_minus_diag, ne_eq, Set.mem_setOf_eq]
        constructor; exact hi.1.1; constructor; exact hi.2.1
        rw[←edist_eq_zero]
        intro hdist
        have hcont := edist_triangle4 (D i.1 : α) x.1 x.2 (D i.2)
        rw [hdist] at hcont
        have hcont2 := add_le_add hi.1.2.2 hi.2.2.2
        simp only [add_zero] at hcont hcont2
        rw[edist_comm] at hcont2
        have hcont3 := le_trans hcont hcont2
        ring_nf at hcont3
        rw[mul_comm, ←mul_assoc] at hcont3
        sorry -- need x ≤ 2/3 * x is a contradiction for nonzero, non-infinity x
      intro hx
      simp only [sq_minus_diag, ne_eq, Set.mem_setOf_eq] at hx
      rcases hx with ⟨hx1, hx2, hne⟩
      set r := edist x.1 x.2
      have : min (ε/2) (r/6) > 0 := by
        apply lt_min
        simp only [ENNReal.div_pos_iff, ne_eq, ENNReal.two_ne_top, not_false_eq_true, and_true]
        exact ne_of_gt εpos
        simp only [ENNReal.div_pos_iff, ne_eq]
        constructor
        rw[edist_eq_zero]; exact hne
        exact ne_of_beq_false rfl
      choose a ha using denseRange_aux Ddense ⟨x.1, hx1⟩ (min (ε/2) (r/6)) this
      choose b hb using denseRange_aux Ddense ⟨x.2, hx2⟩ (min (ε/2) (r/6)) this
      rw[Set.mem_iUnion]
      use (a,b)
      have hab : D a ≠ D b := by
        intro heq
        rw[←zero_eq_edist] at heq
        have hcont := edist_triangle4 x.1 (D a : α) (D b) x.2
        have : edist x.1 x.2 ≤ 2/6 * edist x.1 x.2 := by
          apply le_trans hcont _
          have aux1 : edist x.1 (D a : α) ≤ r/6 := by
            exact le_trans (le_of_lt ha) (min_le_right _ _)
          have aux2 : edist (D a : α) (D b) ≤ 0 := le_of_eq heq.symm
          have aux3 : edist (D b : α) x.2 ≤ r/6 := by
            rw[edist_comm]
            exact le_trans (le_of_lt hb) (min_le_right _ _)
          have ineq2 := add_le_add (add_le_add aux1 aux2) aux3
          apply le_trans ineq2 _
          apply le_of_eq
          ring_nf
          sorry -- need x/6 * 2 = (2/6) * x
        sorry -- need x ≤ 2/6 * x is a contradiction for nonzero, non-infinity x
      simp only [edist_eq_zero, one_div, Set.mem_prod, Set.mem_ite_empty_left, Set.mem_inter_iff,
        EMetric.mem_closedBall, le_min_iff, v, w]
      constructor
      . constructor; exact hab
        constructor; exact hx1
        constructor; exact le_trans (le_of_lt ha) (min_le_left _ _)
        apply le_of_not_gt
        intro hdist; rw[gt_iff_lt] at hdist
        have hdist : edist (D a : α) (D b) ≤ 3 * edist x.1 (D a : α) := by
          sorry -- need to multiply both sides of the old hdist by 3
        have hcont := edist_triangle4 x.1 (D a : α) (D b) x.2
        have : edist x.1 x.2 ≤ 5/6 * edist x.1 x.2 := by
          apply le_trans hcont
          have aux1 : edist x.1 (D a : α) ≤ r/6 := by
            exact le_trans (le_of_lt ha) (min_le_right _ _)
          have aux2 : edist (D a : α) (D b) ≤ 3 * r/6 := by
            apply le_trans hdist
            sorry -- need to multiply both sides of aux1 by 3
          have aux3 : edist (D b : α) x.2 ≤ r/6 := by
            rw[edist_comm]; exact le_trans (le_of_lt hb) (min_le_right _ _)
          have ineq2 := add_le_add (add_le_add aux1 aux2) aux3
          apply le_trans ineq2 _
          ring_nf
          apply le_of_eq
          sorry -- need x/6 * 2 + x*3/6 = 5/6 * x
        sorry -- need x ≤ 5/6 * x is a contradiction for nonzero, non-infinity x
      rw[ne_eq, ←edist_eq_zero] at hab
      rw[if_neg hab]
      apply Set.mem_inter
      exact hx2
      rw[EMetric.mem_closedBall]
      apply le_trans (le_of_lt hb) _
      apply min_le_min
      exact Eq.ge rfl
      apply le_of_not_gt
      intro hdist; rw[gt_iff_lt] at hdist
      have hdist : edist (D a : α) (D b) ≤ 3 * edist x.1 (D a : α) := by
        sorry -- need to multiply both sides of the old hdist by 3
      have hcont := edist_triangle4 x.1 (D a : α) (D b) x.2
      have : edist x.1 x.2 ≤ 5/6 * edist x.1 x.2 := by
        apply le_trans hcont
        have aux1 : edist x.1 (D a : α) ≤ r/6 := by
          exact le_trans (le_of_lt ha) (min_le_right _ _)
        have aux2 : edist (D a : α) (D b) ≤ 3 * r/6 := by
          apply le_trans hdist
          sorry -- need to multiply both sides of aux1 by 3
        have aux3 : edist (D b : α) x.2 ≤ r/6 := by
          rw[edist_comm]; exact le_trans (le_of_lt hb) (min_le_right _ _)
        have ineq2 := add_le_add (add_le_add aux1 aux2) aux3
        apply le_trans ineq2 _
        ring_nf
        apply le_of_eq
        sorry -- need x/6 * 2 + x*3/6 = 5/6 * x
      sorry -- need x ≤ 5/6 * x is a contradiction for nonzero, non-infinity x
    let v' (n : ℕ) : Set α := v (Nat.unpair n)
    let w' (n : ℕ) : Set α := w (Nat.unpair n)
    use v'
    use w'
    constructor
    -- Prove the decomposition works
    . sorry -- Done
    constructor
    -- Prove v n is a subset of u
    . intro n; simp only [v', v]; split
      exact Set.empty_subset u
      exact Set.inter_subset_left _ _
    constructor
    -- Prove w n in a subset of u
    . intro n; simp only [w', w]; split
      intro x hx; rw[Set.mem_singleton_iff] at hx; rw [hx]; exact hx0
      exact Set.inter_subset_left _ _
    constructor
    -- Prove v n is closed
    . intro n; simp only [v', v]; split
      exact isClosed_empty
      apply IsClosed.inter
      exact uclosed
      exact EMetric.isClosed_ball
    constructor
    -- Prove w n is closed
    . intro n; simp only [w', w]; split
      exact T1Space.t1 x0
      apply IsClosed.inter
      exact uclosed
      exact EMetric.isClosed_ball
    constructor
    -- Prove v n has small diameter
    . sorry -- Done
    constructor
    -- Prove w n has small diameter
    . sorry -- Done
    -- Prove v n ≠ w n
    intro n; simp only [v', w', v, w]; split
    . have := Set.singleton_nonempty x0
      exact (Set.Nonempty.ne_empty this).symm
    have : (D (Nat.unpair n).fst : α) ∉ u ∩ EMetric.closedBall
      (D (Nat.unpair n).snd : α) (min (ε / 2) (1 / 3 *
      edist (D (Nat.unpair n).fst) (D (Nat.unpair n).snd))) := by
      intro hcont
      rw[Set.mem_inter_iff, EMetric.mem_closedBall] at hcont
      rcases hcont with ⟨_, hcont⟩
      have hcont := le_trans hcont (min_le_right _ _)
      sorry -- need x ≤ 1/3 * x is a contradiction for nonzero, non-infinity x
    rw[ne_eq, subset_antisymm_iff, not_and_or]
    apply Or.inl
    rw[Set.not_subset]
    use (D (Nat.unpair n).1 : α)
    constructor
    . apply Set.mem_inter
      exact Subtype.mem (D (Nat.unpair n).fst)
      exact EMetric.mem_closedBall_self
    exact this

[Patrick Massot]

This proof is way too complicated. You should try to reorganize it instead of trying to fill in the sorries.

[Patrick Massot]

The first thing to do is to get rid of U and first prove an absolute version, and then deduce the relative one.

[Patrick Massot]

The next step is probably to abstract this is term of filter bases and first countable topologies. We don’t care that the result will become more general, the point is to focus on the relevant things by getting rid of extra structures.