awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q
have hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
Tactic: have hb : Isometry ((↑) : q → X) := isometry_subtype_coe
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q
have A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
Tactic: have A : dist p q = hausdorffDist (p : Set X) q := rfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q
have I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
Tactic: have I : ↑p = range ((↑) : p → X) := Subtype.range_coe_subtype.symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q
have J : (↑q : Set X) = range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
Tactic: have J : ↑q = range ((↑) : q → X) := Subtype.range_coe_subtype.symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
J : (↑q : Set X) = range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q
have rw : dist p.toGHSpace q.toGHSpace ≤
  hausdorffDist.{u} (α := X) (range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p)))
    (range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q)))
Tactic: rw [A, I, J]
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃
have refine : ∀ (δ : ℝ) (δ0 : 0 < δ), ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
Tactic: refine le_of_forall_pos_le_add fun δ δ0 => ?_
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have rcases : ∀ (xX : X), Membership.mem (γ := Set X) univ xX → ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
Tactic: rcases exists_mem_of_nonempty X with ⟨xX, _⟩
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have rcases : ∀ (xs : X) (hxs : xs ∈ s) (Dxs : dist xX xs ≤ ε₁), ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
Tactic: rcases hs xX with ⟨xs, hxs, Dxs⟩
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have sne : s.Nonempty
Tactic: have sne : s.Nonempty := ⟨xs, hxs⟩
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this : 0 ≤ ε₂
Tactic: have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩)
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this : 0 ≤ ε₂
p q : (↑s : Type u)
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)
have linarith : 2 * (ε₂ / 2 + δ) < ε₂ → 2 / 2 = 1
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this : 0 ≤ ε₂
p q : (↑s : Type u)
linarith : 2 * (ε₂ / 2 + δ) < ε₂ → 2 / 2 = 1
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)
have linarith₁ : 2 * (ε₂ / 2 + δ) < ε₂ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this : 0 ≤ ε₂
p q : (↑s : Type u)
linarith : 2 * (ε₂ / 2 + δ) < ε₂ → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (ε₂ / 2 + δ) < ε₂ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)
have linarith₃ : 2 * (ε₂ / 2 + δ) < ε₂ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this : 0 ≤ ε₂
p q : (↑s : Type u)
linarith : 2 * (ε₂ / 2 + δ) < ε₂ → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (ε₂ / 2 + δ) < ε₂ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 2 * (ε₂ / 2 + δ) < ε₂ → GT.gt (α := ℝ) 2 0
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)
have linarith₄ : 2 * (ε₂ / 2 + δ) < ε₂ → 4 * (0 - δ) + (HMul.hMul (α := ℝ) 1 2 * (1 * ε₂ + 2 * δ) - 2 * ε₂) = 0
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this : 0 ≤ ε₂
p q : (↑s : Type u)
linarith : 2 * (ε₂ / 2 + δ) < ε₂ → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (ε₂ / 2 + δ) < ε₂ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 2 * (ε₂ / 2 + δ) < ε₂ → GT.gt (α := ℝ) 2 0
linarith₄ : 2 * (ε₂ / 2 + δ) < ε₂ → 4 * (0 - δ) + (HMul.hMul (α := ℝ) 1 2 * (1 * ε₂ + 2 * δ) - 2 * ε₂) = 0
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)
have linarith₅ : 2 * (ε₂ / 2 + δ) < ε₂ → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this : 0 ≤ ε₂
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this₁ : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
Tactic: have : ∀ p q : s, |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ) := fun p q =>
    calc
      |dist p q - dist (Φ p) (Φ q)| ≤ ε₂ := H p q
      _ ≤ 2 * (ε₂ / 2 + δ) := by linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
⊢ 0 < ε₂ / 2 + δ
have linarith : ε₂ / 2 + δ ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
linarith : ε₂ / 2 + δ ≤ 0 → 2 / 2 = 1
⊢ 0 < ε₂ / 2 + δ
have linarith₁ : ε₂ / 2 + δ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
linarith : ε₂ / 2 + δ ≤ 0 → 2 / 2 = 1
linarith₁ : ε₂ / 2 + δ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < ε₂ / 2 + δ
have linarith₂ : ε₂ / 2 + δ ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
linarith : ε₂ / 2 + δ ≤ 0 → 2 / 2 = 1
linarith₁ : ε₂ / 2 + δ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε₂ / 2 + δ ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < ε₂ / 2 + δ
have linarith₃ : ε₂ / 2 + δ ≤ 0 → 2 * (0 - δ) + (0 - ε₂) + (1 * ε₂ + 2 * δ - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have Il : Isometry Fl
Tactic: have Il : Isometry Fl := Isometry.of_dist_eq fun x y => rfl
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have Ir : Isometry Fr
Tactic: have Ir : Isometry Fr := Isometry.of_dist_eq fun x y => rfl
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this₁ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
Tactic: have : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr) := ghDist_le_hausdorffDist Il Ir
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this₁ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
Tactic: have :
    hausdorffDist (range Fl) (range Fr) ≤
      hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr) :=
    have B : IsBounded (range Fl) := (isCompact_range Il.continuous).isBounded
    hausdorffDist_triangle
      (hausdorffEDist_ne_top_of_nonempty_of_bounded (range_nonempty _) (sne.image _) B
        (B.subset (image_subset_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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this₁ : hausdorffDist (Fl '' s) (range Fr) ≤ hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
Tactic: have :
    hausdorffDist (Fl '' s) (range Fr) ≤
      hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr) :=
    have B : IsBounded (range Fr) := (isCompact_range Ir.continuous).isBounded
    hausdorffDist_triangle'
      (hausdorffEDist_ne_top_of_nonempty_of_bounded ((range_nonempty _).image _) (range_nonempty _)
        (B.subset (image_subset_range _ _)) B)
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
have rw : hausdorffDist univ s ≤ ε₁
Tactic: rw [← image_univ, hausdorffDist_image Il]
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ hausdorffDist univ s ≤ ε₁
have this₁ : 0 ≤ ε₁
Tactic: have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs