Theorem: abd_special (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 c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
⊢ List.Special a b d [a, b, d]
Tactic:
simp only [List.Special, ne_eq, List.getLast_cons, List.getLast_singleton', and_true, hbd,
  or_true, true_and, List.nodup_cons, List.nodup_nil, List.not_mem_nil, List.mem_cons,
  List.mem_singleton, or_false, hbd', hacd.ne13, notCollinear_iff, habc.1.ne, Set.subset_def,
  Set.mem_singleton_iff, Set.mem_insert_iff, forall_eq_or_imp, forall_eq, le_refl,
  List.chain'_cons, List.chain'_singleton, not_false_eq_true]
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
⊢ ∀ (l : Set V), l.IsLine → ¬(a ∈ l ∧ b ∈ l ∧ d ∈ l)

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
⊢ ∀ (l : Set V), l.IsLine → ¬(a ∈ l ∧ b ∈ l ∧ d ∈ l)
Tactic:
intro l hl hl'
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
hl' : a ∈ l ∧ b ∈ l ∧ d ∈ l
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
hl' : a ∈ l ∧ b ∈ l ∧ d ∈ l
⊢ False
Tactic:
exact habc.2.2.2.2.2.2 l hl $ by simp [*, hl.close_middle hl'.1 hl'.2.2 hacd]
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 c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
hl' : a ∈ l ∧ b ∈ l ∧ d ∈ l
⊢ {a, b, c} ⊆ l
Tactic:
simp [*, hl.close_middle hl'.1 hl'.2.2 hacd]
State after:
no goals