Theorem: exists_isLine (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 a b : V
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L
Tactic:
rcases ne_or_eq a b with h | rfl
State after:
case inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : a ≠ b
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L

case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a : V
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L

State before:
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a : V
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
Tactic:
have ⟨b, h⟩ := exists_ne a
State after:
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : b ≠ a
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L

State before:
case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : b ≠ a
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L
Tactic:
exact ⟨Line a b, Line_isLine h.symm, by simp⟩
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 a b : V
h : a ≠ b
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L
Tactic:
exact ⟨Line a b, Line_isLine h, by simp⟩
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 a b : V
h : a ≠ b
⊢ {a, b} ⊆ Line a b
Tactic:
simp
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 a b : V
h : b ≠ a
⊢ {a, a} ⊆ Line a b
Tactic:
simp
State after:
no goals