-- Mathlib/Topology/MetricSpace/GromovHausdorff.lean
theorem hausdorffDist_optimal {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X]
    {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] :
    hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Proof state:
case neg
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
h : ¬hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
calc
  hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
      HD (candidatesBDist X Y) :=
    hausdorffDist_optimal_le_HD _ _ candidatesBDist_mem_candidatesB
  _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := HD_candidatesBDist_le
  _ ≤ hausdorffDist (p : Set ℓ_infty_ℝ) q := not_lt.1 h

Result:
no goals

Proof state:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n => ℝ) ⊤)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam univ + dist (Φ xX) (Ψ z) + diam univ ≤ diam univ + (diam univ + 1 + diam univ) + diam univ

Tactic:
gcongr

Result:
no goals

Proof state:
case intro
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
have : ∃ y ∈ range Ψ, dist (Φ xX) y < diam (univ : Set X) + 1 + diam (univ : Set Y) := by
  rw [Ψrange]
  have : Φ xX ∈ (p : Set _) := Φrange ▸ (mem_range_self _)
  exact
    exists_dist_lt_of_hausdorffDist_lt this bound
      (hausdorffEdist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty
        p.isCompact.isBounded q.isCompact.isBounded)

Result:
case intro
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
this : ∃ y ∈ range Ψ, dist (Φ xX) y < diam univ + 1 + diam univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ

Proof state:
case intro.intro
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n => ℝ) ⊤) :=
  fun x =>
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p => dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
x : X
this✝ : f (inl x) ∈ ↑p
z : ↥(lp (fun n => ℝ) ⊤)
zq : z ∈ ↑q
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
⊢ ⨅ y, Fb (inl x, inr y) ≤ r

Tactic:
rcases mem_range.1 this with ⟨y, hy⟩

Result:
case intro.intro.intro
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n => ℝ) ⊤) :=
  fun x =>
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p => dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
x : X
this✝ : f (inl x) ∈ ↑p
z : ↥(lp (fun n => ℝ) ⊤)
zq : z ∈ ↑q
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
y : Y
hy : Ψ y = z
⊢ ⨅ y, Fb (inl x, inr y) ≤ r

Proof state:
case intro.intro.intro.intro
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n => ℝ) ⊤)
hy : y ∈ range Ψ
dy : dist (Φ xX) y < diam univ + 1 + diam univ
z : Y
hzy : Ψ z = y
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
rw [← hzy] at dy

Result:
case intro.intro.intro.intro
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n => ℝ) ⊤)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n => ℝ) ⊤)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n => ℝ) ⊤)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ