Theorem: exists_min_dist (LeanCamCombi/SylvesterChvatal.lean)

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
cases subsingleton_or_nontrivial V
State after:
case inl
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Subsingleton V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

State before:
case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
let S : Set (V × V) := (Set.diagonal V)ᶜ
State after:
case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

State before:
case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
have : S.Nonempty := have ⟨x, y, hxy⟩ := exists_pair_ne V; ⟨(x, y), by simp [S, hxy]⟩
State after:
case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

State before:
case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
obtain ⟨⟨x, y⟩, (hxy : x ≠ y), h⟩ := S.toFinite.exists_minimal_wrt (Function.uncurry dist) _ this
State after:
case inr.intro.mk.intro
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h :
  ∀ a' ∈ S,
    Function.uncurry dist a' ≤ Function.uncurry dist (x, y) → Function.uncurry dist (x, y) = Function.uncurry dist a'
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

State before:
case inr.intro.mk.intro
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h :
  ∀ a' ∈ S,
    Function.uncurry dist a' ≤ Function.uncurry dist (x, y) → Function.uncurry dist (x, y) = Function.uncurry dist a'
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
simp only [Set.mem_compl_iff, Set.mem_diagonal_iff, Function.uncurry_apply_pair, Prod.forall] at h
State after:
case inr.intro.mk.intro
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h : ∀ (a b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

State before:
case inr.intro.mk.intro
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h : ∀ (a b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
exact ⟨dist x y, by simp [hxy], fun a b hab => le_of_not_lt (fun h' => h'.ne' (h _ _ hab h'.le))⟩
State after:
no goals

State before:
case inl
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Subsingleton V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
exact ⟨1, zero_lt_one, fun x y ↦ by simp [Subsingleton.elim x y]⟩
State after:
no goals

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Subsingleton V
x y : V
⊢ x ≠ y → 1 ≤ dist x y
Tactic:
simp [Subsingleton.elim x y]
State after:
no goals

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
x y : V
hxy : x ≠ y
⊢ (x, y) ∈ S
Tactic:
simp [S, hxy]
State after:
no goals

State before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h : ∀ (a b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ 0 < dist x y
Tactic:
simp [hxy]
State after:
no goals