awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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) ∧ ∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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)
⊢ (((∀ (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)
have left₁ : ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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) ∧ ∀ (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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), 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)
have left₁ : ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
have left : ∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : X), dist (f (inl x)) (f (inl y)) = dist x y) ∧ ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
have left₁ : ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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) ∧ ∀ (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) : ℝ)
have left : ∀ (x y : X), dist (f (inl x)) (f (inl y)) = dist x y
Tactic: repeat' constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : 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) : ℝ)
have left₁ : ∀ (x y : Y), dist (f (inr x)) (f (inr y)) = dist x y
Tactic: repeat' constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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) ∧
          ∀ (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) : ℝ)
have left₂ : ∀ (x y : X ⊕ Y), dist (f x) (f y) = dist (f y) (f x)
Tactic: repeat' constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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)
⊢ (((((∀ (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) : ℝ)
have left₃ : ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)
Tactic: repeat' constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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)
⊢ (((((∀ (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) : ℝ)
have right : ∀ (x y : X ⊕ Y), dist (f x) (f y) ≤ (↑(GromovHausdorff.maxVar✝ X Y) : ℝ)
Tactic: repeat' constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ f z ∈ range Φ ∪ range Ψ
have inl : ∀ (val : X), f (inl val) ∈ range Φ ∪ range Ψ
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 z : X ⊕ Y
inl : ∀ (val : X), f (Sum.inl val) ∈ range Φ ∪ range Ψ
⊢ f z ∈ range Φ ∪ range Ψ
have inr : ∀ (val : Y), f (inr val) ∈ range Φ ∪ range Ψ
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 Φ ∪ range Ψ
have inl : f (inl val) ∈ range Φ
Tactic: apply mem_union_left
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 Φ ∪ range Ψ
have inr : f (inr val) ∈ range Ψ
Tactic: apply mem_union_right
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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
⊢ F (x, y) ≤ diam (range Φ ∪ range Ψ)
have A : ∀ (z : X ⊕ Y), f z ∈ range Φ ∪ range Ψ
Tactic: have A : ∀ z : X ⊕ Y, f z ∈ range Φ ∪ range Ψ := by
                intro z
                cases z
                · apply mem_union_left; apply mem_range_self
                · apply mem_union_right; apply mem_range_self