Theorem: NotCollinear.mk (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
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ NotCollinear x y z
Tactic:
refine ⟨?_, ?_, ?_, hl⟩
State after:
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ y

case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ z

case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ y ≠ z

State before:
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ y
Tactic:
rintro rfl
State after:
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
⊢ False

State before:
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := exists_isLine x z
State after:
case refine_1.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, z} ⊆ L
⊢ False

State before:
case refine_1.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, z} ⊆ L
⊢ False
Tactic:
aesop
State after:
no goals

State before:
case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ z
Tactic:
rintro rfl
State after:
case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
⊢ False

State before:
case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := exists_isLine x y
State after:
case refine_2.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False

State before:
case refine_2.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, x} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False
Tactic:
aesop
State after:
no goals

State before:
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ y ≠ z
Tactic:
rintro rfl
State after:
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
⊢ False

State before:
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
⊢ False
Tactic:
obtain ⟨L, hL, hL'⟩ := exists_isLine x y
State after:
case refine_3.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False

State before:
case refine_3.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
L : Set V
hL : L.IsLine
hL' : {x, y} ⊆ L
⊢ False
Tactic:
aesop
State after:
no goals