α : Type u_1
β : Type ?u.28409
inst✝ : EDist α
x y : α
s t : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ einfsep s ↔ x✝ ≤ ⨅ (d : ↑(offDiag s)), uncurry edist ↑d
α : Type u_1
β : Type ?u.28409
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s = ⨅ (d : ↑(offDiag s)), uncurry edist ↑d
refine' eq_of_forall_le_iff fun _ => _
no goals
α : Type u_1
β : Type ?u.28409
inst✝ : EDist α
x y : α
s t : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ einfsep s ↔ x✝ ≤ ⨅ (d : ↑(offDiag s)), uncurry edist ↑d
simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]