-- Mathlib/Topology/MetricSpace/GromovHausdorff.lean
theorem ghDist_le_nonemptyCompacts_dist (p q : NonemptyCompacts X) :
    dist p.toGHSpace q.toGHSpace ≤ dist p q

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
rw [A, I, J]

Result:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ hausdorffDist (range Subtype.val) (range Subtype.val)

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
have hb : Isometry ((↑) : q → X) := isometry_subtype_coe

Result:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
have I : ↑p = range ((↑) : p → X) := Subtype.range_coe_subtype.symm

Result:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ hausdorffDist (range Subtype.val) (range Subtype.val)

Tactic:
exact ghDist_le_hausdorffDist ha hb

Result:
no goals

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
have J : ↑q = range ((↑) : q → X) := Subtype.range_coe_subtype.symm

Result:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
I : ↑p = range Subtype.val
J : ↑q = range Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
have A : dist p q = hausdorffDist (p : Set X) q := rfl

Result:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
A : dist p q = hausdorffDist ↑p ↑q
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Proof state:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
have ha : Isometry ((↑) : p → X) := isometry_subtype_coe

Result:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q