awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
⊢ s.Subsingleton

Tactic:
fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)

Premises used: edist_ne_top, Set.Subsingleton, of_not_not
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
⊢ s.Subsingleton

Tactic:
exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)

Premises used: edist_ne_top, of_not_not
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
⊢ s.einfsep = ∞ ↔ s.Subsingleton

Tactic:
⟨subsingleton_of_einfsep_eq_top, Subsingleton.einfsep⟩

Premises used: Set.subsingleton_of_einfsep_eq_top, Iff.intro, Set.Subsingleton.einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
contrapose! : ∀ (hs : s.einfsep = ∞), s.Subsingleton
⊢ s.einfsep ≠ ∞

Tactic:
contrapose! hs
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ∞
⊢ s.Subsingleton

Tactic:
subsingleton_of_einfsep_eq_top hs

Premises used: Set.subsingleton_of_einfsep_eq_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ∞
⊢ s.Subsingleton

Tactic:
exact subsingleton_of_einfsep_eq_top hs

Premises used: Set.subsingleton_of_einfsep_eq_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
rw : s.einfsep ≠ ∞
⊢ s.einfsep < ∞

Tactic:
rw [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ∞

Tactic:
hs.einfsep_ne_top

Premises used: Set.Nontrivial.einfsep_ne_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ∞

Tactic:
exact hs.einfsep_ne_top

Premises used: Set.Nontrivial.einfsep_ne_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
⊢ s.einfsep < ∞ ↔ s.Nontrivial

Tactic:
⟨nontrivial_of_einfsep_lt_top, Nontrivial.einfsep_lt_top⟩

Premises used: Set.nontrivial_of_einfsep_lt_top, Iff.intro, Set.Nontrivial.einfsep_lt_top
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
⊢ s.einfsep ≠ ∞ ↔ s.Nontrivial

Tactic:
⟨nontrivial_of_einfsep_ne_top, Nontrivial.einfsep_ne_top⟩

Premises used: Set.Nontrivial.einfsep_ne_top, Set.nontrivial_of_einfsep_ne_top, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
⊢ ENNReal.ofReal d ≤ s.einfsep

Tactic:
le_einfsep fun x hx y hy hxy => (edist_dist x y).symm ▸ ENNReal.ofReal_le_ofReal (h x hx y hy hxy)

Premises used: ENNReal.ofReal_le_ofReal, Eq.rec, Set.le_einfsep, edist_dist, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
intro : ∀ (val : Fintype (↑s : Type u_1)), 0 < s.einfsep
⊢ 0 < s.einfsep

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
neg : ∀ (hs : ¬s.Nontrivial), 0 < s.einfsep
⊢ 0 < s.einfsep

Tactic:
by_cases hs : s.Nontrivial

Premises used: Set.Nontrivial
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
pos : ∀ (x : α) (_hx : x ∈ s) (y : α) (_hy : y ∈ s) (hxy : x ≠ y) (hxy' : s.einfsep = edist x y), 0 < s.einfsep
⊢ 0 < s.einfsep

Tactic:
rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩

Premises used: Set.Nontrivial.einfsep_exists_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : s.einfsep = edist x y
⊢ 0 < s.einfsep

Tactic:
hxy'.symm ▸ edist_pos.2 hxy

Premises used: Iff.mpr, Eq.rec, Eq.symm, edist_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : s.einfsep = edist x y
⊢ 0 < s.einfsep

Tactic:
exact hxy'.symm ▸ edist_pos.2 hxy
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
⊢ s.Subsingleton

Tactic:
rw [not_nontrivial_iff] at hs

Premises used: Set.not_nontrivial_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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.Subsingleton
⊢ 0 < s.einfsep

Tactic:
hs.einfsep.symm ▸ WithTop.top_pos

Premises used: Eq.rec, WithTop.top_pos, Eq.symm, Set.Subsingleton.einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
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.Subsingleton
⊢ 0 < s.einfsep

Tactic:
exact hs.einfsep.symm ▸ WithTop.top_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
rw : 0 < s.einfsep
⊢ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
rw [← einfsep_pos]

Premises used: Set.einfsep_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ 0 < s.einfsep

Tactic:
einfsep_pos_of_finite

Premises used: Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ 0 < s.einfsep

Tactic:
exact einfsep_pos_of_finite

Premises used: Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
hs : s.Finite
⊢ 0 < s.einfsep

Tactic:
letI := hs.fintype
  einfsep_pos_of_finite

Premises used: Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EMetricSpace α
s : Set α
hs : s.Finite
⊢ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
letI := hs.fintype
  relatively_discrete_of_finite

Premises used: Set.relatively_discrete_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
rw : s.einfsep.toReal = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞
rw₁ rw₂ : s.einfsep = 0 ∨ s.einfsep = ∞ ↔ s.einfsep = 0 ∨ s.einfsep = ∞
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Tactic:
rw [infsep, ENNReal.toReal_eq_zero_iff]

Premises used: Set.infsep, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ 0 ≤ s.infsep

Tactic:
ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, Set.infsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
Set.infsep_zero.mpr <| Or.inr hs.einfsep

Premises used: Iff.mpr, Set.infsep_zero, Set.Subsingleton.einfsep, Or.inr
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : 0 < s.infsep
contrapose : ∀ (hs : ¬s.Nontrivial), ¬0 < s.infsep
⊢ s.Nontrivial

Tactic:
contrapose hs
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : ¬s.Nontrivial
⊢ s.Subsingleton

Tactic:
rw [not_nontrivial_iff] at hs

Premises used: Set.not_nontrivial_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
⊢ ¬0 < s.infsep

Tactic:
hs.infsep_zero ▸ lt_irrefl _

Premises used: lt_irrefl, Eq.rec, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Subsingleton
⊢ ¬0 < s.infsep

Tactic:
exact hs.infsep_zero ▸ lt_irrefl _
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
⊢ infsep.{u_1} (α := α) ∅ = 0

Tactic:
subsingleton_empty.infsep_zero

Premises used: Set.subsingleton_empty, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x : α
⊢ infsep (α := α) {x} = 0

Tactic:
subsingleton_singleton.infsep_zero

Premises used: Set.subsingleton_singleton, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
simp_rw : (min (edist x y) (edist y x)).toReal ≤ (min (edist x y) (edist y x)).toReal
⊢ infsep (α := α) {x, y} ≤ (min (edist x y) (edist y x)).toReal

Tactic:
simp_rw [infsep, einfsep_pair_eq_inf hxy]

Premises used: Set.einfsep_pair_eq_inf, Set.infsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ (min (edist x y) (edist y x)).toReal ≤ (min (edist x y) (edist y x)).toReal

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
pos : ∀ (hxy : x = y), infsep (α := α) {x, y} = (edist x y).toReal
neg : ∀ (hxy : ¬x = y), infsep (α := α) {x, y} = (edist x y).toReal
⊢ infsep (α := α) {x, y} = (edist x y).toReal

Tactic:
by_cases hxy : x = y
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x = y
pos : infsep (α := α) {y, y} = (edist y y).toReal
⊢ infsep (α := α) {x, y} = (edist x y).toReal

Tactic:
rw [hxy]
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ infsep (α := α) {y, y} = (edist y y).toReal

Tactic:
simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.toReal_zero]

Premises used: PseudoEMetricSpace.edist_self, Set.infsep_singleton, ENNReal.toReal_zero, Set.pair_eq_singleton
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
neg : (einfsep (α := α) {x, y}).toReal = (edist x y).toReal
neg₁ neg₂ : (edist x y).toReal = (edist x y).toReal
⊢ infsep (α := α) {x, y} = (edist x y).toReal

Tactic:
rw [infsep, einfsep_pair hxy]

Premises used: Set.einfsep_pair, Set.infsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
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
⊢ d ≤ s.infsep ↔ ∀ 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]

Premises used: ENNReal.ofReal_le_ofReal_iff, Set.Nontrivial.einfsep_ne_top, dist_nonneg, ENNReal.ofReal_le_iff_le_toReal, Set.le_einfsep_iff, edist_dist, Set.infsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
contrapose! : d ≤ s.infsep ↔ ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), d ≤ dist x y
⊢ s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Tactic:
contrapose!
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), d ≤ dist x y

Tactic:
hs.le_infsep_iff

Premises used: Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), d ≤ dist x y

Tactic:
exact hs.le_infsep_iff

Premises used: Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
⊢ d ≤ s.infsep

Tactic:
hs.le_infsep_iff.2 h

Premises used: Iff.mpr, Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
neg : ∀ (hs : ¬s.Nontrivial), d ≤ dist x y
⊢ d ≤ dist x y

Tactic:
by_cases hs : s.Nontrivial

Premises used: Set.Nontrivial
-- Module: Mathlib.Topology.MetricSpace.Infsep
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

Tactic:
hs.le_infsep_iff.1 hd x hx y hy hxy

Premises used: Iff.mp, Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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

Tactic:
exact hs.le_infsep_iff.1 hd x hx y hy hxy

Premises used: Iff.mp, Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
⊢ s.Subsingleton

Tactic:
rw [not_nontrivial_iff] at hs

Premises used: Set.not_nontrivial_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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 ≤ 0

Tactic:
rw [hs.infsep_zero] at hd

Premises used: Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
hd₁ : d ≤ 0
⊢ s.Subsingleton

Tactic:
rw [hs.infsep_zero] at hd

Premises used: Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ 0
hs : s.Subsingleton
⊢ d ≤ dist x y

Tactic:
le_trans hd dist_nonneg

Premises used: dist_nonneg, le_trans
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ 0
hs : s.Subsingleton
⊢ d ≤ dist x y

Tactic:
exact le_trans hd dist_nonneg

Premises used: dist_nonneg, le_trans
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
s : Set α
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ s.infsep ≤ dist x y

Tactic:
le_edist_of_le_infsep hx hy hxy le_rfl

Premises used: le_rfl, Set.le_edist_of_le_infsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hxy' : dist x y ≤ d
⊢ s.infsep ≤ d

Tactic:
le_trans (infsep_le_dist_of_mem hx hy hxy) hxy'

Premises used: Set.infsep_le_dist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
rw : (ENNReal.ofReal (dist x y)).toReal = dist x y
⊢ infsep (α := α) {x, y} = dist x y

Tactic:
rw [infsep_pair_eq_toReal, edist_dist]

Premises used: edist_dist, Set.infsep_pair_eq_toReal
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
⊢ (ENNReal.ofReal (dist x y)).toReal = dist x y

Tactic:
ENNReal.toReal_ofReal dist_nonneg

Premises used: dist_nonneg, ENNReal.toReal_ofReal
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
⊢ (ENNReal.ofReal (dist x y)).toReal = dist x y

Tactic:
exact ENNReal.toReal_ofReal dist_nonneg

Premises used: dist_nonneg, ENNReal.toReal_ofReal
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ infsep (α := α) {x, y, z} = min (min (dist x y) (dist x z)) (dist y z)

Tactic:
simp only [infsep, einfsep_triple hxy hyz hxz, ENNReal.toReal_inf, edist_ne_top x y,
    edist_ne_top x z, edist_ne_top y z, dist_edist, Ne, inf_eq_top_iff, and_self_iff,
    not_false_iff]

Premises used: Ne, edist_ne_top, inf_eq_top_iff, Set.einfsep_triple, ENNReal.toReal_inf, and_self_iff, dist_edist, Set.infsep, not_false_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s t : Set α
hs : s.Nontrivial
hst : s ⊆ t
⊢ t.infsep ≤ s.infsep

Tactic:
ENNReal.toReal_mono hs.einfsep_ne_top (einfsep_anti hst)

Premises used: Set.Nontrivial.einfsep_ne_top, Set.einfsep_anti, Set.infsep, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
pos : ∀ (hs : s.Nontrivial), s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
neg : ∀ (hs : ¬s.Nontrivial), s.infsep = 0
⊢ s.infsep = if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0

Tactic:
split_ifs with hs
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ BddBelow (uncurry dist '' s.offDiag)

Tactic:
⟨0, fun d h => ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
refine : ∀ (d : ℝ) (h : d ∈ uncurry dist '' s.offDiag), 0 ≤ d
⊢ BddBelow (uncurry dist '' s.offDiag)

Tactic:
refine ⟨0, fun d h => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : d ∈ uncurry dist '' s.offDiag
⊢ ∃ (a : α) (b : α), (a, b) ∈ s.offDiag ∧ dist a b = d

Tactic:
simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h

Premises used: Set.mem_image, Prod.exists, Function.uncurry_apply_pair
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : ∃ (a : α) (b : α), (a, b) ∈ s.offDiag ∧ dist a b = d
rcases : ∀ (w w_1 : α), (w, w_1) ∈ s.offDiag → 0 ≤ dist w w_1
⊢ 0 ≤ d

Tactic:
rcases h with ⟨_, _, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
w w_1 : α
left : (w, w_1) ∈ s.offDiag
⊢ 0 ≤ dist w w_1

Tactic:
dist_nonneg

Premises used: dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
w w_1 : α
left : (w, w_1) ∈ s.offDiag
⊢ 0 ≤ dist w w_1

Tactic:
exact dist_nonneg

Premises used: dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ BddBelow (uncurry dist '' s.offDiag)

Tactic:
have hb : BddBelow (uncurry dist '' s.offDiag) := by
      refine ⟨0, fun d h => ?_⟩
      simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
      rcases h with ⟨_, _, _, rfl⟩
      exact dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)

Tactic:
eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
pos : ∀ (x : ℝ), x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
pos₁ : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₃ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (i : α × α), i.1 ∈ s ∧ i.2 ∈ s ∧ i.1 ≠ i.2 → x ≤ uncurry dist i
pos₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry dist (a, b)
pos₅ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ dist a b
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)

Tactic:
simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]

Premises used: Iff.mpr, Set.offDiag_nonempty, and_imp, Set.mem_offDiag, imp_forall_iff, Prod.forall, le_ciInf_set_iff, Function.uncurry_apply_pair, Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
(not_nontrivial_iff.mp hs).infsep_zero

Premises used: Set.not_nontrivial_iff, Iff.mp, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
exact (not_nontrivial_iff.mp hs).infsep_zero

Premises used: Set.not_nontrivial_iff, Iff.mp, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
rw :
  Eq (α := ℝ) (if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0)
    (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
rw₁ rw₂ :
  Eq (α := ℝ) (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
    (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)

Tactic:
rw [Set.infsep_eq_iInf, if_pos hs]

Premises used: Set.infsep_eq_iInf, if_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
classical :
  Eq (α := ℝ) (if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0)
    (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
classical₁ classical₂ :
  Eq (α := ℝ) (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
    (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)

Tactic:
classical rw [Set.infsep_eq_iInf, if_pos hs]

Premises used: Set.infsep_eq_iInf, if_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
x y z : α
s t : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa