awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have this : ∃ y ∈ range Ψ, dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) 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)
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
this : ∃ y ∈ range Ψ, dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have rcases : ∀ (y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (hy : y ∈ range Ψ)
  (dy : dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ),
  diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
Tactic: rcases this with ⟨y, hy, dy⟩
Cleared hypotheses: this
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
dy : dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have rcases : ∀ (z : Y) (hzy : Ψ z = y), diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
Tactic: rcases mem_range.1 hy with ⟨z, hzy⟩
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
dy : dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
z : Y
hzy : Ψ z = y
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have dy₁ : dist (Φ xX) (Ψ z) < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Tactic: rw [← hzy] at dy
Cleared hypotheses: dy, hzy
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
hzy : Ψ z = y
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have DΦ : diam (range Φ) = diam.{u} (α := X) univ
Tactic: have DΦ : diam (range Φ) = diam (univ : Set X) := Φisom.diam_range
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam.{u} (α := X) univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have DΨ : diam (range Ψ) = diam.{v} (α := Y) univ
Tactic: have DΨ : diam (range Ψ) = diam (univ : Set Y) := Ψisom.diam_range
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam.{u} (α := X) univ
DΨ : diam (range Ψ) = diam.{v} (α := Y) univ
⊢ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) ≤
    diam.{u} (α := X) univ + (diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ) + diam.{v} (α := Y) univ
have rw : diam.{u} (α := X) univ + dist (Φ xX) (Ψ z) + diam.{v} (α := Y) univ ≤
  diam.{u} (α := X) univ + (diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ) + diam.{v} (α := Y) univ
Tactic: rw [DΦ, DΨ]
-- 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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam.{u} (α := X) univ
DΨ : diam (range Ψ) = diam.{v} (α := Y) univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have diam : diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) ≤
  diam.{u} (α := X) univ + (diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ) + diam.{v} (α := Y) univ
Tactic: calc
        diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) :=
          diam_union (mem_range_self _) (mem_range_self _)
        _ ≤
            diam (univ : Set X) + (diam (univ : Set X) + 1 + diam (univ : Set Y)) +
              diam (univ : Set Y) := by
          rw [DΦ, DΨ]
          gcongr
        _ = 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by ring
-- 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 : ℕ) ↦ ℝ) ∞)) <
    Metric.diam.{u} (α := X) univ + 1 + Metric.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 : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
y : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < Metric.diam.{u} (α := X) univ + 1 + Metric.diam.{v} (α := Y) univ
hzy : Ψ z = y
DΦ : Metric.diam (range Φ) = Metric.diam.{u} (α := X) univ
DΨ : Metric.diam (range Ψ) = Metric.diam.{v} (α := Y) univ
diam :
  Metric.diam (range Φ) + dist (Φ xX) (Ψ z) + Metric.diam (range Ψ) ≤
    Metric.diam.{u} (α := X) univ + (Metric.diam.{u} (α := X) univ + 1 + Metric.diam.{v} (α := Y) univ) +
      Metric.diam.{v} (α := Y) univ
⊢ Metric.diam (range Φ ∪ range Ψ) ≤ 2 * Metric.diam.{u} (α := X) univ + 1 + 2 * Metric.diam.{v} (α := Y) univ
have diam₁ : Metric.diam.{u} (α := X) univ + (Metric.diam.{u} (α := X) univ + 1 + Metric.diam.{v} (α := Y) univ) +
    Metric.diam.{v} (α := Y) univ =
  2 * Metric.diam.{u} (α := X) univ + 1 + 2 * Metric.diam.{v} (α := Y) univ
Tactic: calc
        diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) :=
          diam_union (mem_range_self _) (mem_range_self _)
        _ ≤
            diam (univ : Set X) + (diam (univ : Set X) + 1 + diam (univ : Set Y)) +
              diam (univ : Set Y) := by
          rw [DΦ, DΨ]
          gcongr
        _ = 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by ring
-- 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 : ℕ) ↦ ℝ) ∞))
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have I : diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
Tactic: have I : diam (range Φ ∪ range Ψ) ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by
      rcases exists_mem_of_nonempty X with ⟨xX, _⟩
      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)
      rcases this with ⟨y, hy, dy⟩
      rcases mem_range.1 hy with ⟨z, hzy⟩
      rw [← hzy] at dy
      have DΦ : diam (range Φ) = diam (univ : Set X) := Φisom.diam_range
      have DΨ : diam (range Ψ) = diam (univ : Set Y) := Ψisom.diam_range
      calc
        diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) :=
          diam_union (mem_range_self _) (mem_range_self _)
        _ ≤
            diam (univ : Set X) + (diam (univ : Set X) + 1 + diam (univ : Set Y)) +
              diam (univ : Set Y) := by
          rw [DΦ, DΨ]
          gcongr
        _ = 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by ring
-- 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)
⊢ F ∈ candidates X Y
have simp : (((((∀ (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: simp only [F, candidates, forall_const,
        dist_eq_zero, Set.mem_setOf_eq]
-- 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) ∧ ∀ (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
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 z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)) ∧
    True
⊢ (((((∀ (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: 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
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)) ∧
  ∀ (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)
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 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
have left₁ : True
Tactic: constructor