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 ⊕ Y
A : ∀ (z : X ⊕ Y), f z ∈ range Φ ∪ range Ψ
⊢ F (x, y) ≤ diam (range Φ ∪ range Ψ)
have refine : Bornology.IsBounded (range Φ ∪ range Ψ)
Tactic: refine dist_le_diam_of_mem ?_ (A _) (A _)
-- 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
A : ∀ (z : X ⊕ Y), f z ∈ range Φ ∪ range Ψ
⊢ Bornology.IsBounded (range Φ ∪ range Ψ)
have rw : Bornology.IsBounded ((↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ∪ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
Tactic: rw [Φrange, Ψ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 : ℕ) ↦ ℝ) ∞))
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)
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have Fgood : F ∈ candidates X Y
Tactic: have Fgood : F ∈ candidates X Y := by
      simp only [F, candidates, forall_const,
        dist_eq_zero, Set.mem_setOf_eq]
      repeat' constructor
      · exact fun x y =>
          calc
            F (inl x, inl y) = dist (Φ x) (Φ y) := rfl
            _ = dist x y := Φisom.dist_eq x y
      · exact fun x y =>
          calc
            F (inr x, inr y) = dist (Ψ x) (Ψ y) := rfl
            _ = dist x y := Ψisom.dist_eq x y
      · exact fun x y => dist_comm _ _
      · exact fun x y z => dist_triangle _ _ _
      · exact fun x y =>
          calc
            F (x, y) ≤ diam (range Φ ∪ range Ψ) := by
              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
              refine dist_le_diam_of_mem ?_ (A _) (A _)
              rw [Φrange, Ψrange]
              exact (p ⊔ q).isCompact.isBounded
            _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := I
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have this : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
Tactic: have : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb :=
      hausdorffDist_optimal_le_HD _ _ (candidatesBOfCandidates_mem F Fgood)
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have refine : ∀ (r : ℝ) (hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r), HD Fb ≤ r
Tactic: refine le_trans this (le_of_forall_gt_imp_ge_of_dense fun r hr => ?_)
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
⊢ ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
have this₁ : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: have : f (inl x) ∈ (p : Set _) := Φrange ▸ (mem_range_self _)
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this_1 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
this : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
have rcases : ∀ (z : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (zq : z ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (hz : dist (f (inl x)) z < r),
  ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
Tactic: rcases exists_dist_lt_of_hausdorffDist_lt this hr
          (hausdorffEDist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.isCompact.isBounded
            q.isCompact.isBounded) with
        ⟨z, zq, hz⟩
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this_1 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
this : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
z : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
zq : z ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
hz : dist (f (inl x)) z < r
⊢ z ∈ range Ψ
have rwa : ∀ (zq : z ∈ range Ψ) (hz : dist (f (inl x)) z < r), z ∈ range Ψ
Tactic: rwa [← Ψrange] at zq
Cleared hypotheses: zq, hz
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this_1 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
this : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
z : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
zq : z ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
hz : dist (f (inl x)) z < r
⊢ ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
have this₁ : z ∈ range Ψ
Tactic: have : z ∈ range Ψ := by rwa [← Ψrange] at zq
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this_1 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
this_2 : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
z : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
zq : z ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
⊢ ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
have rcases : ∀ (y : Y) (hy : Ψ y = z), ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
Tactic: rcases mem_range.1 this with ⟨y, hy⟩
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this_1 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
this_2 : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
z : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
zq : z ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
y : Y
hy : Ψ y = z
⊢ dist (Φ x) (Ψ y) = dist (f (inl x)) z
have rw : dist (Φ x) z = dist (f (inl x)) z
Tactic: rw [hy]
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this_1 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
x : X
this_2 : f (inl x) ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
z : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
zq : z ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
y : Y
hy : Ψ y = z
⊢ ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
have Fb₁ : dist (Φ x) (Ψ y) = dist (f (inl x)) z
Tactic: calc
        (⨅ y, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :=
          ciInf_le (by simpa only [add_zero] using HD_below_aux1 0) y
        _ = dist (Φ x) (Ψ y) := rfl
        _ = dist (f (inl x)) z := by rw [hy]
        _ ≤ r := le_of_lt hz
-- 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)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) < r
⊢ HD Fb ≤ r
have I1 : ∀ (x : X), ⨅ (y : Y), (Fb : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ r
Tactic: have I1 : ∀ x : X, (⨅ y, Fb (inl x, inr y)) ≤ r := by
      intro x
      have : f (inl x) ∈ (p : Set _) := Φrange ▸ (mem_range_self _)
      rcases exists_dist_lt_of_hausdorffDist_lt this hr
          (hausdorffEDist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.isCompact.isBounded
            q.isCompact.isBounded) with
        ⟨z, zq, hz⟩
      have : z ∈ range Ψ := by rwa [← Ψrange] at zq
      rcases mem_range.1 this with ⟨y, hy⟩
      calc
        (⨅ y, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :=
          ciInf_le (by simpa only [add_zero] using HD_below_aux1 0) y
        _ = dist (Φ x) (Ψ y) := rfl
        _ = dist (f (inl x)) z := by rw [hy]
        _ ≤ r := le_of_lt hz