no goals
α : Type ?u.65546
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ Finset.Nonempty (toFinset (offDiag s))
simpa
case inl
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ infsep s = Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)

case inr
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : ¬Set.Nontrivial s
⊢ infsep s = 0
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ infsep s =
    if hs : Set.Nontrivial s then
      Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
    else 0
split_ifs with hs
case inl
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
x✝ : ℝ
⊢ x✝ ≤ infsep s ↔ x✝ ≤ Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
case inl
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ infsep s = Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
refine' eq_of_forall_le_iff fun _ => _
no goals
case inl
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
x✝ : ℝ
⊢ x✝ ≤ infsep s ↔ x✝ ≤ Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]
case inr
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Subsingleton s
⊢ infsep s = 0
case inr
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : ¬Set.Nontrivial s
⊢ infsep s = 0
rw [not_nontrivial_iff] at hs
no goals
case inr
α : Type u_1
β : Type ?u.65549
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Subsingleton s
⊢ infsep s = 0
exact hs.infsep_zero