-- Mathlib/Topology/MetricSpace/GromovHausdorff.lean
theorem ghDist_eq_hausdorffDist (X : Type u) [MetricSpace X] [CompactSpace X] [Nonempty X]
    (Y : Type v) [MetricSpace Y] [CompactSpace Y] [Nonempty Y] :
    ∃ Φ : X → ℓ_infty_ℝ,
      ∃ Ψ : Y → ℓ_infty_ℝ,
        Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

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
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
let Φ := F ∘ optimalGHInjl X Y

Result:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

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
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
let F := kuratowskiEmbedding (OptimalGHCoupling X Y)

Result:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Proof state:
case refine_1
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ Isometry Φ

Tactic:
exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjl X Y)

Result:
no goals

Proof state:
case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
    hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))

Tactic:
exact (hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm

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
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
refine ⟨Φ, Ψ, ?_, ?_, ?_⟩

Result:
case refine_1
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ Isometry Φ

case refine_2
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ Isometry Ψ

case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

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
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
let Ψ := F ∘ optimalGHInjr X Y

Result:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Proof state:
case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y),
  image_univ, ← hausdorffDist_optimal]

Result:
case refine_3
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
    hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))

Proof state:
case refine_2
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun i => ℝ) ⊤) := F ∘ optimalGHInjr X Y
⊢ Isometry Ψ

Tactic:
exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjr X Y)

Result:
no goals