no goals
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
classical
  cases nonempty_fintype s
  simp_rw [hs.infsep_of_fintype]
  rcases@Finset.exists_mem_eq_inf' _ _ _ s.offDiag.toFinset (by simpa) (uncurry dist) with
    ⟨w, hxy, hed⟩
  simp_rw [mem_toFinset] at hxy
  exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
case intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
cases nonempty_fintype s
case intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
case intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
simp_rw [hs.infsep_of_fintype]
case intro.intro.intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ toFinset (offDiag s)
hed : Finset.inf' (toFinset (offDiag s)) ?m.80020 (uncurry dist) = uncurry dist w
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
case intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
rcases@Finset.exists_mem_eq_inf' _ _ _ s.offDiag.toFinset (by simpa) (uncurry dist) with
  ⟨w, hxy, hed⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hed : Finset.inf' (toFinset (offDiag s)) ?m.80020 (uncurry dist) = uncurry dist w
hxy : w ∈ offDiag s
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
case intro.intro.intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ toFinset (offDiag s)
hed : Finset.inf' (toFinset (offDiag s)) ?m.80020 (uncurry dist) = uncurry dist w
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
simp_rw [mem_toFinset] at hxy
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hed : Finset.inf' (toFinset (offDiag s)) ?m.80020 (uncurry dist) = uncurry dist w
hxy : w ∈ offDiag s
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
no goals
α : Type u_1
β : Type ?u.77742
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ Finset.Nonempty (toFinset (offDiag s))
simpa