-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_eq_iInf [Decidable s.Nontrivial] :
    s.infsep = if s.Nontrivial then ⨅ d : s.offDiag, (uncurry dist) (d : α × α) else 0

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ BddBelow (uncurry dist '' s.offDiag)

Tactic:
refine ⟨0, fun d h => ?_⟩

Result:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : d ∈ uncurry dist '' s.offDiag
⊢ 0 ≤ d

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Result:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⨅ d, uncurry dist ↑d

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⨅ d, uncurry dist ↑d

Tactic:
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]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Tactic:
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

Result:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
⊢ s.infsep = if s.Nontrivial then ⨅ d, uncurry dist ↑d else 0

Tactic:
split_ifs with hs

Result:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : d ∈ uncurry dist '' s.offDiag
⊢ 0 ≤ d

Tactic:
simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h

Result:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : ∃ a b, (a, b) ∈ s.offDiag ∧ dist a b = d
⊢ 0 ≤ d

Proof state:
case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
exact (not_nontrivial_iff.mp hs).infsep_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : ∃ a b, (a, b) ∈ s.offDiag ∧ dist a b = d
⊢ 0 ≤ d

Tactic:
rcases h with ⟨_, _, _, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
w✝¹ w✝ : α
left✝ : (w✝¹, w✝) ∈ s.offDiag
⊢ 0 ≤ dist w✝¹ w✝

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
w✝¹ w✝ : α
left✝ : (w✝¹, w✝) ∈ s.offDiag
⊢ 0 ≤ dist w✝¹ w✝

Tactic:
exact dist_nonneg

Result:
no goals