case inl
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d

case inr
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : ¬Set.Nontrivial s
⊢ infsep s = 0
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
⊢ infsep s = if Set.Nontrivial s then ⨅ (d : ↑(offDiag s)), uncurry dist ↑d else 0
split_ifs with hs
case inl
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
hb : BddBelow (uncurry dist '' offDiag s)
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
case inl
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
have hb : BddBelow (uncurry dist '' s.offDiag) := by
  refine' ⟨0, fun d h => _⟩
  simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
  rcases h with ⟨_, _, _, rfl⟩
  exact dist_nonneg
case inl
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
hb : BddBelow (uncurry dist '' offDiag s)
x✝ : ℝ
⊢ x✝ ≤ infsep s ↔ x✝ ≤ ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
case inl
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
hb : BddBelow (uncurry dist '' offDiag s)
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
refine' eq_of_forall_le_iff fun _ => _
no goals
case inl
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
hb : BddBelow (uncurry dist '' offDiag s)
x✝ : ℝ
⊢ x✝ ≤ infsep s ↔ x✝ ≤ ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
  mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
d : ℝ
h : d ∈ uncurry dist '' offDiag s
⊢ 0 ≤ d
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
⊢ BddBelow (uncurry dist '' offDiag s)
refine' ⟨0, fun d h => _⟩
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
d : ℝ
h : ∃ a b, (a, b) ∈ offDiag s ∧ dist a b = d
⊢ 0 ≤ d
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
d : ℝ
h : d ∈ uncurry dist '' offDiag s
⊢ 0 ≤ d
simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
case intro.intro.intro
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
w✝¹ w✝ : α
left✝ : (w✝¹, w✝) ∈ offDiag s
⊢ 0 ≤ dist w✝¹ w✝
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
d : ℝ
h : ∃ a b, (a, b) ∈ offDiag s ∧ dist a b = d
⊢ 0 ≤ d
rcases h with ⟨_, _, _, rfl⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
w✝¹ w✝ : α
left✝ : (w✝¹, w✝) ∈ offDiag s
⊢ 0 ≤ dist w✝¹ w✝
exact dist_nonneg
no goals
case inr
α : Type u_1
β : Type ?u.62378
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : ¬Set.Nontrivial s
⊢ infsep s = 0
exact (not_nontrivial_iff.mp hs).infsep_zero