awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
intro : ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
intro₁ : ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
have intro₂ : ∀ (val : Fintype (↑s : Type u_1)) (w : α × α) (hxy : w ∈ s.offDiag.toFinset)
  (hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w),
  ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y
Tactic: classical
    cases nonempty_fintype s
    simp_rw [einfsep_of_fintype]
    rcases Finset.exists_mem_eq_inf s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩
    simp_rw [mem_toFinset] at hxy
    exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
intro : ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
intro₁ : ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y
intro₂ :
  ∀ (val : Fintype (↑s : Type u_1)) (w : α × α) (hxy : w ∈ s.offDiag.toFinset)
    (hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w),
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
have intro₃ : ∀ (val : Fintype (↑s : Type u_1)) (w : α × α) (hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w)
  (hxy : w ∈ s.offDiag), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y
Tactic: classical
    cases nonempty_fintype s
    simp_rw [einfsep_of_fintype]
    rcases Finset.exists_mem_eq_inf s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩
    simp_rw [mem_toFinset] at hxy
    exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {x, y} = edist x y
have nth_rw : einfsep (α := α) {x, y} = min (edist x y) (edist x y)
Tactic: nth_rw 1 [← min_self (edist x y)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {x, y} = min (edist x y) (edist x y)
have h : edist x y = edist y x
Tactic: convert! einfsep_pair_eq_inf hxy using 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ edist x y = edist y x
have h : edist y x = edist y x
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep
have refine : min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep
Tactic: refine le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep
have simp_rw : ∀ (x_1 : α),
  x_1 = x ∨ x_1 ∈ s →
    ∀ (y : α), y = x ∨ y ∈ s → x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y
Tactic: simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z
have inr : ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw : min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
    (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
      (einfsep (α := α) {z})) =
  min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
simp_rw :
  min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw₁ : min
    (min (⨅ (_ : x ≠ y), edist x y)
      (⨅ (x_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} x_1), ⨅ (_ : x ≠ x_1), edist x x_1))
    (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
      (einfsep (α := α) {z})) =
  min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
simp_rw :
  min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₁ :
  min
      (min (⨅ (_ : x ≠ y), edist x y)
        (⨅ (x_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} x_1), ⨅ (_ : x ≠ x_1), edist x x_1))
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw₂ : min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z))
    (min (⨅ (_ : y ≠ z), edist y z) (einfsep (α := α) {z})) =
  min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
simp_rw :
  min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₁ :
  min
      (min (⨅ (_ : x ≠ y), edist x y)
        (⨅ (x_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} x_1), ⨅ (_ : x ≠ x_1), edist x x_1))
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₂ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z))
      (min (⨅ (_ : y ≠ z), edist y z) (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw₃ : min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) ∞) =
  min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
simp_rw :
  min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₁ :
  min
      (min (⨅ (_ : x ≠ y), edist x y)
        (⨅ (x_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} x_1), ⨅ (_ : x ≠ x_1), edist x x_1))
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₂ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z))
      (min (⨅ (_ : y ≠ z), edist y z) (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₃ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) ∞) =
    min (min (edist x y) (edist x z)) (edist y z)
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw₄ : min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (⨅ (_ : y ≠ z), edist y z) =
  min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
simp_rw :
  min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₁ :
  min
      (min (⨅ (_ : x ≠ y), edist x y)
        (⨅ (x_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} x_1), ⨅ (_ : x ≠ x_1), edist x x_1))
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₂ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z))
      (min (⨅ (_ : y ≠ z), edist y z) (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₃ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) ∞) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₄ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (⨅ (_ : y ≠ z), edist y z) =
    min (min (edist x y) (edist x z)) (edist y z)
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw₅ : min (min (edist x y) (⨅ (_ : x ≠ z), edist x z)) (⨅ (_ : y ≠ z), edist y z) =
  min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
simp_rw :
  min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {y, z} y_1), ⨅ (_ : x ≠ y_1), edist x y_1)
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₁ :
  min
      (min (⨅ (_ : x ≠ y), edist x y)
        (⨅ (x_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} x_1), ⨅ (_ : x ≠ x_1), edist x x_1))
      (min (⨅ (y_1 : α), ⨅ (_ : Membership.mem (γ := Set α) {z} y_1), ⨅ (_ : y ≠ y_1), edist y y_1)
        (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₂ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z))
      (min (⨅ (_ : y ≠ z), edist y z) (einfsep (α := α) {z})) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₃ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) ∞) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₄ :
  min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (⨅ (_ : y ≠ z), edist y z) =
    min (min (edist x y) (edist x z)) (edist y z)
simp_rw₅ :
  min (min (edist x y) (⨅ (_ : x ≠ z), edist x z)) (⨅ (_ : y ≠ z), edist y z) =
    min (min (edist x y) (edist x z)) (edist y z)
⊢ einfsep (α := α) {x, y, z} = min (min (edist x y) (edist x z)) (edist y z)
have simp_rw₆ : min (min (edist x y) (⨅ (_ : x ≠ z), edist x z)) (edist y z) = min (min (edist x y) (edist x z)) (edist y z)
Tactic: simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
⊢ c ≤ (pi (α := X) univ s).einfsep
have refine : ∀ (x : (i : β) → X i) (hx : x ∈ pi (α := X) univ s) (y : (i : β) → X i) (hy : y ∈ pi (α := X) univ s) (hxy : x ≠ y),
  c ≤ edist x y
Tactic: refine le_einfsep fun x hx y hy hxy => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : x ∈ pi (α := X) univ s
y : (i : β) → X i
hy : y ∈ pi (α := X) univ s
hxy : x ≠ y
⊢ c ≤ edist x y
have rw : ∀ (hx : ∀ (i : β), x i ∈ s i) (y : (i : β) → X i) (hy : ∀ (i : β), y i ∈ s i) (hxy : x ≠ y), c ≤ edist x y
Tactic: rw [mem_univ_pi] at hx hy
Cleared hypotheses: hx, y, hy, hxy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → X i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y
have rcases : ∀ (i : β) (hi : x i ≠ y i), c ≤ edist x y
Tactic: rcases Function.ne_iff.mp hxy with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ∞
⊢ s.Subsingleton
have hs₁ : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
Tactic: rw [einfsep_top] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ∞
have contrapose! : ∀ (hs : s.einfsep = ∞), s.Subsingleton
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep < ∞
have rw : s.einfsep ≠ ∞
Tactic: rw [lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ 0 < s.einfsep
have intro : ∀ (val : Fintype (↑s : Type u_1)), 0 < s.einfsep
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
val : Fintype (↑s : Type u_1)
⊢ 0 < s.einfsep
have pos : ∀ (hs : s.Nontrivial), 0 < s.einfsep
Tactic: by_cases hs : s.Nontrivial
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
val : Fintype (↑s : Type u_1)
pos : ∀ (hs : s.Nontrivial), 0 < s.einfsep
⊢ 0 < s.einfsep
have neg : ∀ (hs : ¬s.Nontrivial), 0 < s.einfsep
Tactic: by_cases hs : s.Nontrivial
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
val : Fintype (↑s : Type u_1)
hs : s.Nontrivial
⊢ 0 < s.einfsep
have pos : ∀ (x : α) (_hx : x ∈ s) (y : α) (_hy : y ∈ s) (hxy : x ≠ y) (hxy' : s.einfsep = edist x y), 0 < s.einfsep
Tactic: rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
val : Fintype (↑s : Type u_1)
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep
have hs₁ : s.Subsingleton
Tactic: rw [not_nontrivial_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
have rw : 0 < s.einfsep
Tactic: rw [← einfsep_pos]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞
have rw : s.einfsep.toReal = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞
Tactic: rw [infsep, ENNReal.toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
rw : s.einfsep.toReal = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞
have rw₁ : s.einfsep = 0 ∨ s.einfsep = ∞ ↔ s.einfsep = 0 ∨ s.einfsep = ∞
Tactic: rw [infsep, ENNReal.toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : 0 < s.infsep
⊢ s.Nontrivial
have contrapose : ∀ (hs : ¬s.Nontrivial), ¬0 < s.infsep
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : ¬s.Nontrivial
⊢ ¬0 < s.infsep
have hs₁ : s.Subsingleton
Tactic: rw [not_nontrivial_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ infsep (α := α) {x, y} ≤ (min (edist x y) (edist y x)).toReal
have simp_rw : (min (edist x y) (edist y x)).toReal ≤ (min (edist x y) (edist y x)).toReal
Tactic: simp_rw [infsep, einfsep_pair_eq_inf hxy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
⊢ infsep (α := α) {x, y} = (edist x y).toReal
have pos : ∀ (hxy : x = y), infsep (α := α) {x, y} = (edist x y).toReal
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
pos : ∀ (hxy : x = y), infsep (α := α) {x, y} = (edist x y).toReal
⊢ infsep (α := α) {x, y} = (edist x y).toReal
have neg : ∀ (hxy : ¬x = y), infsep (α := α) {x, y} = (edist x y).toReal
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ infsep (α := α) {x, y} = (edist x y).toReal
have pos : infsep (α := α) {y, y} = (edist y y).toReal
Tactic: rw [hxy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
⊢ infsep (α := α) {x, y} = (edist x y).toReal
have neg : (einfsep (α := α) {x, y}).toReal = (edist x y).toReal
Tactic: rw [infsep, einfsep_pair hxy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
neg : (einfsep (α := α) {x, y}).toReal = (edist x y).toReal
⊢ infsep (α := α) {x, y} = (edist x y).toReal
have neg₁ : (edist x y).toReal = (edist x y).toReal
Tactic: rw [infsep, einfsep_pair hxy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
have simp_rw : d ≤ s.einfsep.toReal ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
Tactic: simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
    ENNReal.ofReal_le_ofReal_iff dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
simp_rw : d ≤ s.einfsep.toReal ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
have simp_rw₁ : ENNReal.ofReal d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
Tactic: simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
    ENNReal.ofReal_le_ofReal_iff dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
simp_rw : d ≤ s.einfsep.toReal ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
simp_rw₁ : ENNReal.ofReal d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
have simp_rw₂ : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → ENNReal.ofReal d ≤ edist x y) ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
Tactic: simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
    ENNReal.ofReal_le_ofReal_iff dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
simp_rw : d ≤ s.einfsep.toReal ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
simp_rw₁ : ENNReal.ofReal d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
simp_rw₂ : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → ENNReal.ofReal d ≤ edist x y) ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
have simp_rw₃ : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → ENNReal.ofReal d ≤ ENNReal.ofReal (dist x y)) ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
Tactic: simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
    ENNReal.ofReal_le_ofReal_iff dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d
have contrapose! : d ≤ s.infsep ↔ ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), d ≤ dist x y
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
⊢ d ≤ dist x y
have pos : ∀ (hs : s.Nontrivial), d ≤ dist x y
Tactic: by_cases hs : s.Nontrivial
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
pos : ∀ (hs : s.Nontrivial), d ≤ dist x y
⊢ d ≤ dist x y
have neg : ∀ (hs : ¬s.Nontrivial), d ≤ dist x y
Tactic: by_cases hs : s.Nontrivial
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : ¬s.Nontrivial
⊢ d ≤ dist x y
have hs₁ : s.Subsingleton
Tactic: rw [not_nontrivial_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : s.Subsingleton
⊢ d ≤ dist x y
have hd₁ : d ≤ 0
Tactic: rw [hs.infsep_zero] at hd
Cleared hypotheses: hd, hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
⊢ infsep (α := α) {x, y} = dist x y
have rw : (ENNReal.ofReal (dist x y)).toReal = dist x y
Tactic: rw [infsep_pair_eq_toReal, edist_dist]