awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X_1 : ℕ → Type
inst : (n : ℕ) → MetricSpace (X_1 n)
inst_1 : ∀ (n : ℕ), CompactSpace (X_1 n)
inst_2 : ∀ (n : ℕ), Nonempty (X_1 n)
d : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
this_1 : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : (n : ℕ) → Type := fun (n : ℕ) ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E :
  ∀ (n : ℕ),
    GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯ = AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1))
c : (n : ℕ) →
  (a : GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯) → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) :=
  fun (n : ℕ) ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) := fun (n : ℕ) ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (x : (Y n).Space) → InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I :=
  toInductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : (n : ℕ) → Set (UniformSpace.Completion Z0) := fun (n : ℕ) ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun (n : ℕ) ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
n : ℕ
⊢ Nonempty (↥(X3 n) ≃ᵢ (u n).Rep)
have val : ↥(X3 n) ≃ᵢ (u n).Rep
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
Goal:
X_1 : ℕ → Type
inst : (n : ℕ) → MetricSpace (X_1 n)
inst_1 : ∀ (n : ℕ), CompactSpace (X_1 n)
inst_2 : ∀ (n : ℕ), Nonempty (X_1 n)
d : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
this_1 : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : (n : ℕ) → Type := fun (n : ℕ) ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E :
  ∀ (n : ℕ),
    GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯ = AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1))
c : (n : ℕ) →
  (a : GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯) → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) :=
  fun (n : ℕ) ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) := fun (n : ℕ) ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (x : (Y n).Space) → InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I :=
  toInductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : (n : ℕ) → Set (UniformSpace.Completion Z0) := fun (n : ℕ) ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun (n : ℕ) ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
⊢ ∃ (x : GHSpace), Tendsto u atTop (𝓝 x)
have this₁ : ∀ (n : ℕ), (NonemptyCompacts.toGHSpace ∘ X3) n = u n
Tactic: have : ∀ n, (NonemptyCompacts.toGHSpace ∘ X3) n = u n := by
    intro n
    rw [Function.comp_apply, NonemptyCompacts.toGHSpace, ← (u n).toGHSpace_rep,
      toGHSpace_eq_toGHSpace_iff_isometryEquiv]
    constructor
    convert! (isom n).isometryEquivOnRange.symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X_1 : ℕ → Type
inst : (n : ℕ) → MetricSpace (X_1 n)
inst_1 : ∀ (n : ℕ), CompactSpace (X_1 n)
inst_2 : ∀ (n : ℕ), Nonempty (X_1 n)
d : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
this_1 : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : (n : ℕ) → Type := fun (n : ℕ) ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E :
  ∀ (n : ℕ),
    GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯ = AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1))
c : (n : ℕ) →
  (a : GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯) → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) :=
  fun (n : ℕ) ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) := fun (n : ℕ) ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (x : (Y n).Space) → InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I :=
  toInductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : (n : ℕ) → Set (UniformSpace.Completion Z0) := fun (n : ℕ) ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun (n : ℕ) ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this_2 : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
this : ∀ (n : ℕ), (NonemptyCompacts.toGHSpace ∘ X3) n = u n
⊢ ∃ (x : GHSpace), Tendsto u atTop (𝓝 x)
have h : Tendsto u atTop (𝓝 L.toGHSpace)
Tactic: use L.toGHSpace
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X_1 : ℕ → Type
inst : (n : ℕ) → MetricSpace (X_1 n)
inst_1 : ∀ (n : ℕ), CompactSpace (X_1 n)
inst_2 : ∀ (n : ℕ), Nonempty (X_1 n)
d : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
this_1 : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : (n : ℕ) → Type := fun (n : ℕ) ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E :
  ∀ (n : ℕ),
    GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯ = AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1))
c : (n : ℕ) →
  (a : GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯) → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) :=
  fun (n : ℕ) ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) := fun (n : ℕ) ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (x : (Y n).Space) → InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I :=
  toInductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : (n : ℕ) → Set (UniformSpace.Completion Z0) := fun (n : ℕ) ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun (n : ℕ) ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this_2 : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
this : ∀ (n : ℕ), (NonemptyCompacts.toGHSpace ∘ X3) n = u n
⊢ Tendsto u atTop (𝓝 L.toGHSpace)
have h : Tendsto (NonemptyCompacts.toGHSpace ∘ X3) atTop (𝓝 L.toGHSpace)
Tactic: apply Filter.Tendsto.congr this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X_1 : ℕ → Type
inst : (n : ℕ) → MetricSpace (X_1 n)
inst_1 : ∀ (n : ℕ), CompactSpace (X_1 n)
inst_2 : ∀ (n : ℕ), Nonempty (X_1 n)
d : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
this_1 : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : (n : ℕ) → Type := fun (n : ℕ) ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E :
  ∀ (n : ℕ),
    GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯ = AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1))
c : (n : ℕ) →
  (a : GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯) → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) :=
  fun (n : ℕ) ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → AuxGluingStruct.Space (A := X (n + 1)) (Y (n + 1)) := fun (n : ℕ) ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (x : (Y n).Space) → InductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I :=
  toInductiveLimit (X := fun (n : ℕ) ↦ (Y n).Space) I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : (n : ℕ) → Set (UniformSpace.Completion Z0) := fun (n : ℕ) ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun (n : ℕ) ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this_2 : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
this : ∀ (n : ℕ), (NonemptyCompacts.toGHSpace ∘ X3) n = u n
⊢ Tendsto (NonemptyCompacts.toGHSpace ∘ X3) atTop (𝓝 L.toGHSpace)
have h : Tendsto NonemptyCompacts.toGHSpace (𝓝 L) (𝓝 L.toGHSpace)
Tactic: refine Tendsto.comp ?_ hL
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ HMul.hMul (α := ℝ) 2 0 + 1 + HMul.hMul (α := ℝ) 2 0 ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have h₁ : 0 ≤ diam.{u} (α := X) univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
h₁ : 0 ≤ diam.{u} (α := X) univ
⊢ HMul.hMul (α := ℝ) 2 0 + 1 + HMul.hMul (α := ℝ) 2 0 ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have h₂ : 0 ≤ diam.{v} (α := Y) univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ diam (α := X ⊕ Y) univ = diam (α := X ⊕ Y) (range inl ∪ range inr)
have rw : diam (α := X ⊕ Y) univ = diam (α := X ⊕ Y) univ
Tactic: rw [range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ diam (α := X ⊕ Y) (range inl) + dist (α := X ⊕ Y) (inl default) (inr default) + diam (α := X ⊕ Y) (range inr) =
    diam.{u} (α := X) univ + (dist.{u} (α := X) default default + 1 + dist.{v} (α := Y) default default) +
      diam.{v} (α := Y) univ
have rw : diam.{u} (α := X) univ + dist (α := X ⊕ Y) (inl default) (inr default) + diam.{v} (α := Y) univ =
  diam.{u} (α := X) univ + (dist.{u} (α := X) default default + 1 + dist.{v} (α := Y) default default) +
    diam.{v} (α := Y) univ
Tactic: rw [isometry_inl.diam_range, isometry_inr.diam_range]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ 1 * diam.{u} (α := X) univ + 1 + 1 * diam.{v} (α := Y) univ ≤
    2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have h₁ : LE.le (α := ℝ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ 1 * dist (α := X ⊕ Y) (inl x) (inl y) ≤ (↑(maxVar X Y) : ℝ) * dist (α := X ⊕ Y) (inl x) (inl y)
have hbc : 1 ≤ (↑(maxVar X Y) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ (↑(maxVar X Y) : ℝ) * 1 ≤ (↑(maxVar X Y) : ℝ) * dist (inl x) (inr y)
have hbc : 1 ≤ dist (inl x) (inr y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ (↑(maxVar X Y) : ℝ) * 1 ≤ (↑(maxVar X Y) : ℝ) * dist (inl x) (inr y)
have hbc : 1 ≤ dist (inl x) (inr y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 * dist (α := X ⊕ Y) (inr x) (inr y) ≤ (↑(maxVar X Y) : ℝ) * dist (α := X ⊕ Y) (inr x) (inr y)
have hbc : 1 ≤ (↑(maxVar X Y) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) + f (t, y) ≤ (↑(maxVar X Y) : ℝ) * dist x z + (↑(maxVar X Y) : ℝ) * dist t y
have h₁ : f (x, z) ≤ (↑(maxVar X Y) : ℝ) * dist x z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
h₁ : f (x, z) ≤ (↑(maxVar X Y) : ℝ) * dist x z
⊢ f (x, z) + f (t, y) ≤ (↑(maxVar X Y) : ℝ) * dist x z + (↑(maxVar X Y) : ℝ) * dist t y
have h₂ : f (t, y) ≤ (↑(maxVar X Y) : ℝ) * dist t y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ (↑(maxVar X Y) : ℝ) * dist x z + (↑(maxVar X Y) : ℝ) * dist t y ≤
    (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y)
have h₁ : dist x z ≤ max (dist x z) (dist t y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
h₁ : dist x z ≤ max (dist x z) (dist t y)
⊢ (↑(maxVar X Y) : ℝ) * dist x z + (↑(maxVar X Y) : ℝ) * dist t y ≤
    (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y)
have h₂ : dist t y ≤ max (dist x z) (dist t y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) =
    2 * (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t)
have rw : (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t) =
  2 * (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t)
Tactic: rw [dist_comm t y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ LipschitzWith (2 * maxVar X Y) f
have a : ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist x y
Tactic: apply LipschitzWith.of_dist_le_mul
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ dist (f (x, y)) (f (z, t)) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
have a : f (x, y) - f (z, t) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t) ∧
  f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
Tactic: rw [Real.dist_eq, abs_sub_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (x, y) - f (z, t) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t) ∧
    f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
have right : f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
Tactic: use candidates_lipschitz_aux fA
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
have right : f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (z, t) (x, y)
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ IsClosed (X := Cb X Y) (candidatesB X Y)
have I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
Tactic: have I1 : ∀ x y, IsClosed { f : Cb X Y | f (inl x, inl y) = dist x y } := fun x y =>
    isClosed_eq (continuous_eval_const _) continuous_const
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
⊢ IsClosed (X := Cb X Y) (candidatesB X Y)
have I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
Tactic: have I2 : ∀ x y, IsClosed { f : Cb X Y | f (inr x, inr y) = dist x y } := fun x y =>
    isClosed_eq (continuous_eval_const _) continuous_const
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
⊢ IsClosed (X := Cb X Y) (candidatesB X Y)
have I3 : ∀ (x y : X ⊕ Y),
  IsClosed (X := Cb X Y)
    {f : Cb X Y |
      Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
Tactic: have I3 : ∀ x y, IsClosed { f : Cb X Y | f (x, y) = f (y, x) } := fun x y =>
    isClosed_eq (continuous_eval_const _) (continuous_eval_const _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
⊢ IsClosed (X := Cb X Y) (candidatesB X Y)
have I4 : ∀ (x y z : X ⊕ Y),
  IsClosed (X := Cb X Y)
    {f : Cb X Y |
      (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
        HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
          ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
Tactic: have I4 : ∀ x y z, IsClosed { f : Cb X Y | f (x, z) ≤ f (x, y) + f (y, z) } := fun x y z =>
    isClosed_le (continuous_eval_const _) ((continuous_eval_const _).add (continuous_eval_const _))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
I4 :
  ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
⊢ IsClosed (X := Cb X Y) (candidatesB X Y)
have I5 : ∀ (x : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}
Tactic: have I5 : ∀ x, IsClosed { f : Cb X Y | f (x, x) = 0 } := fun x =>
    isClosed_eq (continuous_eval_const _) continuous_const
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
I4 :
  ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
I5 :
  ∀ (x : X ⊕ Y),
    IsClosed (X := Cb X Y) {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}
⊢ IsClosed (X := Cb X Y) (candidatesB X Y)
have I6 : ∀ (x y : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)}
Tactic: have I6 : ∀ x y, IsClosed { f : Cb X Y | f (x, y) ≤ maxVar X Y } := fun x y =>
    isClosed_le (continuous_eval_const _) continuous_const