α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = if hs : Finset.Nonempty (Finset.offDiag s) then Finset.inf' (Finset.offDiag s) hs (uncurry dist) else 0
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
⊢ infsep ↑s = if hs : Finset.Nonempty (Finset.offDiag s) then Finset.inf' (Finset.offDiag s) hs (uncurry dist) else 0
have H : (s : Set α).Nontrivial ↔ s.offDiag.Nonempty := by
  rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]
case inl
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
hs : Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = Finset.inf' (Finset.offDiag s) hs (uncurry dist)

case inr
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
hs : ¬Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = 0
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = if hs : Finset.Nonempty (Finset.offDiag s) then Finset.inf' (Finset.offDiag s) hs (uncurry dist) else 0
split_ifs with hs
no goals
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]
no goals
case inl
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
hs : Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = Finset.inf' (Finset.offDiag s) hs (uncurry dist)
simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]
no goals
case inr
α : Type u_1
β : Type ?u.73231
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
hs : ¬Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = 0
exact (not_nontrivial_iff.mp (H.mp.mt hs)).infsep_zero