awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

Tactic:
simp only [le_refl, true_or, or_true]

Premises used: le_refl, true_or, or_true
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

Tactic:
try simp only [le_refl, true_or, or_true]

Premises used: le_refl, true_or, or_true
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
simp only [le_refl, true_or, or_true]

Premises used: le_refl, true_or, or_true
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
try simp only [le_refl, true_or, or_true]

Premises used: le_refl, true_or, or_true
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

Tactic:
contradiction
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b

Tactic:
contradiction
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {x, y} ≤ edist x y

Tactic:
einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hxy

Premises used: Set.mem_singleton, Set.einfsep_le_edist_of_mem, Set.mem_insert_of_mem, Set.mem_insert
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
rw : einfsep (α := α) {y, x} ≤ edist y x
⊢ einfsep (α := α) {x, y} ≤ edist y x

Tactic:
rw [pair_comm]

Premises used: Set.pair_comm
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {y, x} ≤ edist y x

Tactic:
einfsep_pair_le_left hxy.symm

Premises used: Set.einfsep_pair_le_left, Ne.symm
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {y, x} ≤ edist y x

Tactic:
exact einfsep_pair_le_left hxy.symm

Premises used: Set.einfsep_pair_le_left, Ne.symm
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {x, y} = min (edist x y) (edist y x)

Tactic:
le_antisymm (le_inf (einfsep_pair_le_left hxy) (einfsep_pair_le_right hxy)) le_einfsep_pair

Premises used: Set.einfsep_pair_le_left, le_inf, le_antisymm, Set.einfsep_pair_le_right, Set.le_einfsep_pair
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
⊢ s.einfsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑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 : EDist α
s : Set α
refine : ∀ (x : ℝ≥0∞), x ≤ s.einfsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)
⊢ s.einfsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑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 : EDist α
s : Set α
x : ℝ≥0∞
simp_rw :
  (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ edist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)
simp_rw₁ :
  (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ edist x_1 y) ↔ ∀ (i : (↑s.offDiag : Type u_1)), x ≤ uncurry edist (↑i : α × α)
simp_rw₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (i : (↑s.offDiag : Type u_1)), x ≤ uncurry edist (↑i : α × α)
simp_rw₃ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (x_1 : α × α) (h : x_1 ∈ s.offDiag), x ≤ uncurry edist x_1
simp_rw₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (x_1 : α × α) (h : x_1.1 ∈ s ∧ x_1.2 ∈ s ∧ x_1.1 ≠ x_1.2), x ≤ uncurry edist x_1
simp_rw₅ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (a b : α) (h : a ∈ s ∧ b ∈ s ∧ a ≠ b), x ≤ uncurry edist (a, b)
simp_rw₆ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (a b : α) (h : a ∈ s ∧ b ∈ s ∧ a ≠ b), x ≤ edist a b
⊢ x ≤ s.einfsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry edist (↑d : α × α)

Tactic:
simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

Premises used: and_imp, Set.mem_offDiag, le_iInf_iff, Set.le_einfsep_iff, imp_forall_iff, Prod.forall, SetCoe.forall, Function.uncurry_apply_pair
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
⊢ s.einfsep = s.offDiag.toFinset.inf (uncurry edist)

Tactic:
eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
refine : ∀ (x : ℝ≥0∞), x ≤ s.einfsep ↔ x ≤ s.offDiag.toFinset.inf (uncurry edist)
⊢ s.einfsep = s.offDiag.toFinset.inf (uncurry edist)

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 : EDist α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
x : ℝ≥0∞
simp_rw : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ edist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf (uncurry edist)
simp_rw₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf (uncurry edist)
simp_rw₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔ ∀ b ∈ s.offDiag.toFinset, x ≤ uncurry edist b
simp_rw₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry edist b
simp_rw₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x ≤ uncurry edist b
simp_rw₅ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry edist (a, b)
simp_rw₆ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ edist a b
⊢ x ≤ s.einfsep ↔ x ≤ s.offDiag.toFinset.inf (uncurry edist)

Tactic:
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, mem_toFinset, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

Premises used: and_imp, Set.mem_offDiag, Set.le_einfsep_iff, Finset.le_inf_iff, imp_forall_iff, Prod.forall, Set.mem_toFinset, Function.uncurry_apply_pair
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Finite
⊢ s.einfsep = ⋯.toFinset (s := s.offDiag).inf (uncurry edist)

Tactic:
eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hs : s.Finite
refine : ∀ (x : ℝ≥0∞), x ≤ s.einfsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf (uncurry edist)
⊢ s.einfsep = ⋯.toFinset (s := s.offDiag).inf (uncurry edist)

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 : EDist α
s : Set α
hs : s.Finite
x : ℝ≥0∞
simp_rw : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ edist x_1 y) ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf (uncurry edist)
simp_rw₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    x ≤ ⋯.toFinset (s := s.offDiag).inf (uncurry edist)
simp_rw₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ b ∈ ⋯.toFinset (s := s.offDiag), x ≤ uncurry edist b
simp_rw₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry edist b
simp_rw₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x ≤ uncurry edist b
simp_rw₅ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry edist (a, b)
simp_rw₆ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ edist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ edist a b
⊢ x ≤ s.einfsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf (uncurry edist)

Tactic:
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, Finite.mem_toFinset, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

Premises used: and_imp, Set.Finite.mem_toFinset, Set.mem_offDiag, Set.le_einfsep_iff, Finset.le_inf_iff, imp_forall_iff, Prod.forall, Function.uncurry_apply_pair
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Finset α
simp_rw : (↑s : Set α).offDiag.toFinset.inf (uncurry edist) = s.offDiag.inf (uncurry edist)
simp_rw₁ : (↑s.offDiag : Set (α × α)).toFinset.inf (uncurry edist) = s.offDiag.inf (uncurry edist)
⊢ (↑s : Set α).einfsep = s.offDiag.inf (uncurry edist)

Tactic:
simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Premises used: Set.einfsep_of_fintype, Finset.toFinset_coe, Finset.coe_offDiag
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Finset α
classical : (↑s : Set α).offDiag.toFinset.inf (uncurry edist) = s.offDiag.inf (uncurry edist)
classical₁ : (↑s.offDiag : Set (α × α)).toFinset.inf (uncurry edist) = s.offDiag.inf (uncurry edist)
⊢ (↑s : Set α).einfsep = s.offDiag.inf (uncurry edist)

Tactic:
classical simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Premises used: Set.einfsep_of_fintype, Finset.toFinset_coe, Finset.coe_offDiag
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
intro : ∃ 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

Tactic:
simp_rw [einfsep_of_fintype]

Premises used: Set.einfsep_of_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
intro :
  ∀ (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.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
rcases Finset.exists_mem_eq_inf s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩

Premises used: Finset.exists_mem_eq_inf, Set.offDiag, Set.toFinset, EDist.edist, Function.uncurry
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
⊢ w ∈ s.offDiag

Tactic:
simp_rw [mem_toFinset] at hxy

Premises used: Set.mem_toFinset
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
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:
⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

Premises used: Prod.fst, And.right, And.left, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
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:
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
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
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = 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⟩

Premises used: Set.einfsep_of_fintype, Set.Elem, nonempty_fintype, Set.mem_toFinset
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : EDist α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
letI := hsf.fintype
  hs.einfsep_exists_of_finite

Premises used: Set.Nontrivial.einfsep_exists_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
nth_rw : einfsep (α := α) {x, y} = min (edist x y) (edist x y)
⊢ einfsep (α := α) {x, y} = edist x y

Tactic:
nth_rw 1 [← min_self (edist x y)]

Premises used: min_self, EDist.edist
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ einfsep (α := α) {x, y} = min (edist x y) (edist y x)

Tactic:
einfsep_pair_eq_inf hxy

Premises used: Set.einfsep_pair_eq_inf
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
h : edist x y = edist y x
⊢ einfsep (α := α) {x, y} = min (edist x y) (edist x y)

Tactic:
convert! einfsep_pair_eq_inf hxy using 2

Premises used: Set.einfsep_pair_eq_inf
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
h h₁ : edist y x = edist y x
⊢ edist x y = edist y x

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep

Tactic:
le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_

Premises used: Set.einfsep_anti, Set.einfsep_insert_le, le_min, le_antisymm, Set.subset_insert
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
refine : min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep
⊢ (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep

Tactic:
refine le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_

Premises used: Set.einfsep_anti, Set.einfsep_insert_le, le_min, le_antisymm, Set.subset_insert
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
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
⊢ min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep

Tactic:
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]

Premises used: inf_le_iff, Set.le_einfsep_iff, Set.mem_insert_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
z : α
hyz : z ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z z ∨ s.einfsep ≤ edist z z

Tactic:
False.elim (hyz rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
z : α
hyz : z ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z z ∨ s.einfsep ≤ edist z z

Tactic:
exact False.elim (hyz rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
y z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y_1 ∈ s, ⨅ (_ : y ≠ y_1), edist y y_1 ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))

Premises used: iInf₂_le, Or.inl, iInf_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
y z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y_1 ∈ s, ⨅ (_ : y ≠ y_1), edist y y_1 ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))

Premises used: iInf₂_le, Or.inl, iInf_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
inr : ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y

Tactic:
Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))

Premises used: iInf₂_le, Or.inl, iInf_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y

Tactic:
exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))

Premises used: iInf₂_le, Or.inl, iInf_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
Or.inr (einfsep_le_edist_of_mem hy hz hyz)

Premises used: Set.einfsep_le_edist_of_mem, Or.inr
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)

Premises used: Set.einfsep_le_edist_of_mem, Or.inr
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)
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)
⊢ einfsep (α := α) {x, 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]

Premises used: inf_top_eq, Set.einfsep_insert, Set.einfsep_singleton, iInf_singleton, iInf_insert, ciInf_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
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

Tactic:
le_einfsep fun x hx y hy hxy => ?_

Premises used: Set.le_einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
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
⊢ c ≤ (pi (α := X) univ s).einfsep

Tactic:
refine le_einfsep fun x hx y hy hxy => ?_

Premises used: Set.le_einfsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
rw : ∀ (hx : ∀ (i : β), x i ∈ s i) (y : (i : β) → X i) (hy : ∀ (i : β), y i ∈ s i) (hxy : x ≠ y), c ≤ edist x y
⊢ c ≤ edist x y

Tactic:
rw [mem_univ_pi] at hx hy

Premises used: Set.mem_univ_pi
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
rcases : ∀ (i : β) (hi : x i ≠ y i), c ≤ edist x y
⊢ c ≤ edist x y

Tactic:
rcases Function.ne_iff.mp hxy with ⟨i, hi⟩

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y

Tactic:
le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

Premises used: edist_le_pi_edist, Set.le_einfsep_iff, Iff.mp, le_trans
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y

Tactic:
exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

Premises used: edist_le_pi_edist, Set.le_einfsep_iff, Iff.mp, le_trans
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ∞
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
rw [einfsep_top] at hs

Premises used: Set.einfsep_top