α : Type u_1
β : Type ?u.33000
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Finite s
x✝ : ℝ≥0∞
⊢ x✝ ≤ Set.einfsep s ↔ x✝ ≤ Finset.inf (Finite.toFinset (_ : Set.Finite (offDiag s))) (uncurry edist)
α : Type u_1
β : Type ?u.33000
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Finite s
⊢ Set.einfsep s = Finset.inf (Finite.toFinset (_ : Set.Finite (offDiag s))) (uncurry edist)
refine' eq_of_forall_le_iff fun _ => _
no goals
α : Type u_1
β : Type ?u.33000
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Finite s
x✝ : ℝ≥0∞
⊢ x✝ ≤ Set.einfsep s ↔ x✝ ≤ Finset.inf (Finite.toFinset (_ : Set.Finite (offDiag s))) (uncurry edist)
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, Finite.mem_toFinset, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]