awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
left :
  ((∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y) ∧
    ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)
left₁ : ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)
⊢ (((∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y) ∧
      ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)) ∧
    ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
left : (∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
left₁ : ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)
⊢ ((∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y) ∧
    ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
left : ∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y
left₁ : ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
⊢ (∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ True

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
left : ∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y
left₁ : ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
left₂ : ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)
left₃ : ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)
right : ∀ (x y : X ⊕ Y), dist (f x) (f y) ≤ (↑(GromovHausdorff.maxVar✝ X Y) : ℝ)
⊢ (((((∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y) ∧
          ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)) ∧
        ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)) ∧
      True) ∧
    ∀ (x y : X ⊕ Y), dist (f x) (f y) ≤ (↑(GromovHausdorff.maxVar✝ X Y) : ℝ)

Tactic:
repeat' constructor
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y

Tactic:
fun x y =>
          calc
            F (inl x, inl y) = dist (Φ x) (Φ y) := rfl
            _ = dist x y := Φisom.dist_eq x y

Premises used: ENNReal.ofNNReal, Trans.trans, WithTop.some, Isometry.dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y

Tactic:
exact fun x y =>
          calc
            F (inl x, inl y) = dist (Φ x) (Φ y) := rfl
            _ = dist x y := Φisom.dist_eq x y

Premises used: Trans.trans, Isometry.dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y

Tactic:
fun x y =>
          calc
            F (inr x, inr y) = dist (Ψ x) (Ψ y) := rfl
            _ = dist x y := Ψisom.dist_eq x y

Premises used: ENNReal.ofNNReal, Trans.trans, WithTop.some, Isometry.dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y

Tactic:
exact fun x y =>
          calc
            F (inr x, inr y) = dist (Ψ x) (Ψ y) := rfl
            _ = dist x y := Ψisom.dist_eq x y

Premises used: Trans.trans, Isometry.dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)

Tactic:
fun x y => dist_comm _ _

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)

Tactic:
exact fun x y => dist_comm _ _

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)

Tactic:
fun x y z => dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
⊢ ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)

Tactic:
exact fun x y z => dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | Sum.inl y => Φ y
    | Sum.inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
x y z : X ⊕ Y
inl : ∀ (val : X), f (Sum.inl val) ∈ range Φ ∪ range Ψ
inr : ∀ (val : Y), f (Sum.inr val) ∈ range Φ ∪ range Ψ
⊢ f z ∈ range Φ ∪ range Ψ

Tactic:
cases z
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | Sum.inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val : X
inl : f (Sum.inl val) ∈ range Φ
⊢ f (Sum.inl val) ∈ range Φ ∪ range Ψ

Tactic:
apply mem_union_left

Premises used: Set.mem_union_left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val : X
⊢ f (inl val) ∈ range Φ

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | Sum.inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val : Y
inr : f (Sum.inr val) ∈ range Ψ
⊢ f (Sum.inr val) ∈ range Φ ∪ range Ψ

Tactic:
apply mem_union_right

Premises used: Set.mem_union_right
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
f : X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) :=
  fun (x : X ⊕ Y) ↦
    match (motive := X ⊕ Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val : Y
⊢ f (inr val) ∈ range Ψ

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self