internlm/Lean-Github huggingface dataset:
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V) (h₁ : NotCollinear a b c)
    (h₂ :
      ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'),
    ¬SimpleEdges.Adj a b → False
hab : ¬¬SimpleEdges.Adj a b
⊢ False
Tactic:
rw [not_not] at hab
Proof state after:
case intro.mk.mk.intro.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V) (h₁ : NotCollinear a b c)
    (h₂ :
      ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'),
    ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
⊢ False

V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
⊢ (a b c : V) →
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        MetricSpace V
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro.inr.refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V),
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
⊢ SimpleEdges.Adj b c
Tactic:
exact not_not.1 <| this b c a h₁.rotate <|
  fun _ _ _ h => (h₂ _ _ _ h).trans_eq' <| by ring
Proof state after:
no goals
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V),
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
x✝² x✝¹ x✝ : V
h : NotCollinear x✝² x✝¹ x✝
⊢ dist b c + dist c a + dist a b = dist a b + dist b c + dist c a
Tactic:
ring
Proof state after:
no goals
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro.inr.refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V),
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
⊢ SimpleEdges.Adj c a
Tactic:
exact not_not.1 <| this c a b h₁.rotate.rotate <|
  fun _ _ _ h => (h₂ _ _ _ h).trans_eq' <| by ring
Proof state after:
no goals
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
this :
  ∀ (a b c : V),
    NotCollinear a b c →
      (∀ (a' b' c' : V),
          NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a') →
        ¬SimpleEdges.Adj a b → False
hab : SimpleEdges.Adj a b
x✝² x✝¹ x✝ : V
h : NotCollinear x✝² x✝¹ x✝
⊢ dist c a + dist a b + dist b c = dist a b + dist b c + dist c a
Tactic:
ring
Proof state after:
no goals
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
hc : c ∈ Line a b
⊢ {a, b, c} ⊆ Line a b
Tactic:
simp [left_mem_Line, right_mem_Line, hc]
Proof state after:
no goals
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
⊢ dist d c < dist d b + dist b c
Tactic:
by_contra!
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ False
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ False
Tactic:
refine habc (generateLine_close_right hdab right_mem_Line ?_)
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ sbtw d b c
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d b + dist b c ≤ dist d c
⊢ sbtw d b c
Tactic:
exact ⟨adb.ne23, hcd.symm, h₁.2.2.1, this.antisymm (dist_triangle _ _ _)⟩
Proof state after:
no goals
Theorem: one_implies_two
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this✝ : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
cont : ∀ (x y z : V), SimpleEdges.Adj x y → SimpleEdges.Adj y z → SimpleEdges.Adj z x → ¬NotCollinear x y z
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ (a' b' c' : V), NotCollinear a' b' c' → dist a b + dist b c + dist c a ≤ dist a' b' + dist b' c' + dist c' a'
d : V
adb : sbtw a d b
habc : c ∉ Line a b
hdab : d ∈ Line a b
hcd : c ≠ d
this : dist d c < dist d b + dist b c
⊢ dist a d + dist d c + dist c a < dist a b + dist b c + dist c a
Tactic:
linarith only [this, adb.2.2.2]
Proof state after:
no goals
Theorem: Delta_comm
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
⊢ Delta u v w = Delta w v u
Tactic:
simp only [Delta, add_comm, dist_comm]
Proof state after:
no goals
Theorem: Delta_pos_of
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
⊢ 0 < Delta u v w
Tactic:
rw [Delta]
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
⊢ 0 < dist u v + dist v w - dist u w
Theorem: Delta_pos_of
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
⊢ 0 < dist u v + dist v w - dist u w
Tactic:
by_contra!
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this : dist u v + dist v w - dist u w ≤ 0
⊢ False
Theorem: Delta_pos_of
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this : dist u v + dist v w - dist u w ≤ 0
⊢ False
Tactic:
have : sbtw u v w := sbtw_mk h.1 h.2.2.1 (by linarith only [this])
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ False
Theorem: Delta_pos_of
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ False
Tactic:
exact h.2.2.2 (Line u v) (Line_isLine this.ne12) (by simp [right_extend_mem_Line this])
Proof state after:
no goals
Theorem: Delta_pos_of
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this : dist u v + dist v w - dist u w ≤ 0
⊢ dist u v + dist v w ≤ dist u w
Tactic:
linarith only [this]
Proof state after:
no goals
Theorem: Delta_pos_of
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ {u, v, w} ⊆ Line u v
Tactic:
simp [right_extend_mem_Line this]
Proof state after:
no goals
Theorem: exists_third
Proof 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
hab : a ≠ b
h : Line a b ≠ {a, b}
⊢ ∃ c ∈ Line a b, sbtw c a b ∨ sbtw a c b ∨ sbtw a b c
Tactic:
by_contra! h'
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ False
Theorem: exists_third
Proof 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
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
this : Line a b = {a, b}
⊢ False
Tactic:
exact h this
Proof state after:
no goals
Theorem: exists_third
Proof 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
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ Line a b = {a, b}
Tactic:
refine (subset_generateLine _).antisymm' ?_
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ GenerateLine {a, b} ⊆ {a, b}
Theorem: exists_third
Proof 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
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ GenerateLine {a, b} ⊆ {a, b}
Tactic:
change Line a b ⊆ {a, b}
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ Line a b ⊆ {a, b}
Theorem: exists_third
Proof 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
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ Line a b ⊆ {a, b}
Tactic:
refine generateLine_minimal le_rfl ?_ ?_
Proof 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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x y z → z ∈ {a, b}

case refine_2
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x z y → z ∈ {a, b}
Theorem: exists_third
Proof 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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x y z → z ∈ {a, b}
Tactic:
rintro x y z (rfl | rfl) (rfl | rfl) h
Proof state after:
case refine_1.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y y z
⊢ z ∈ {y, b}

case refine_1.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x y z
⊢ z ∈ {x, y}

case refine_1.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x y z
⊢ z ∈ {y, x}

case refine_1.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y y z
⊢ z ∈ {a, y}
Theorem: exists_third
Proof state before:
case refine_1.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y y z
⊢ z ∈ {y, b}
Tactic:
exact (h.ne12 rfl).elim
Proof state after:
no goals
Theorem: exists_third
Proof state before:
case refine_1.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x y z
⊢ z ∈ {x, y}
Tactic:
exact ((h' z (right_extend_mem_Line h)).2.2 h).elim
Proof state after:
no goals
Theorem: exists_third
Proof state before:
case refine_1.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x y z
⊢ z ∈ {y, x}
Tactic:
exact ((h' z (left_extend_mem_Line h.symm)).1 h.symm).elim
Proof state after:
no goals
Theorem: exists_third
Proof state before:
case refine_1.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y y z
⊢ z ∈ {a, y}
Tactic:
exact (h.ne12 rfl).elim
Proof state after:
no goals
Theorem: exists_third
Proof 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 a b : V
hab : a ≠ b
h : Line a b ≠ {a, b}
h' : ∀ c ∈ Line a b, ¬sbtw c a b ∧ ¬sbtw a c b ∧ ¬sbtw a b c
⊢ ∀ {x y z : V}, x ∈ {a, b} → y ∈ {a, b} → sbtw x z y → z ∈ {a, b}
Tactic:
rintro x y z (rfl | rfl) (rfl | rfl) h
Proof state after:
case refine_2.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y z y
⊢ z ∈ {y, b}

case refine_2.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x z y
⊢ z ∈ {x, y}

case refine_2.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x z y
⊢ z ∈ {y, x}

case refine_2.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y z y
⊢ z ∈ {a, y}
Theorem: exists_third
Proof state before:
case refine_2.inl.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ b y z : V
hab : y ≠ b
h✝ : Line y b ≠ {y, b}
h' : ∀ c ∈ Line y b, ¬sbtw c y b ∧ ¬sbtw y c b ∧ ¬sbtw y b c
h : sbtw y z y
⊢ z ∈ {y, b}
Tactic:
exact (h.ne13 rfl).elim
Proof state after:
no goals
Theorem: exists_third
Proof state before:
case refine_2.inl.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : x ≠ y
h✝ : Line x y ≠ {x, y}
h' : ∀ c ∈ Line x y, ¬sbtw c x y ∧ ¬sbtw x c y ∧ ¬sbtw x y c
h : sbtw x z y
⊢ z ∈ {x, y}
Tactic:
exact ((h' z (middle_extend_mem_Line h)).2.1 h).elim
Proof state after:
no goals
Theorem: exists_third
Proof state before:
case refine_2.inr.inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z✝ x y z : V
hab : y ≠ x
h✝ : Line y x ≠ {y, x}
h' : ∀ c ∈ Line y x, ¬sbtw c y x ∧ ¬sbtw y c x ∧ ¬sbtw y x c
h : sbtw x z y
⊢ z ∈ {y, x}
Tactic:
exact ((h' z (middle_extend_mem_Line h.symm)).2.1 h.symm).elim
Proof state after:
no goals
Theorem: exists_third
Proof state before:
case refine_2.inr.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y✝ z✝ a y z : V
hab : a ≠ y
h✝ : Line a y ≠ {a, y}
h' : ∀ c ∈ Line a y, ¬sbtw c a y ∧ ¬sbtw a c y ∧ ¬sbtw a y c
h : sbtw y z y
⊢ z ∈ {a, y}
Tactic:
exact (h.ne13 rfl).elim
Proof state after:
no goals
Theorem: eqn_7
Proof 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
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
⊢ ¬SimpleEdges.Adj b d
Tactic:
intro h
Proof 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
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
⊢ False
Theorem: eqn_7
Proof 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
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
⊢ False
Tactic:
have hbcd : NotCollinear b c d := by
  refine ⟨habc.2.1.ne, h.ne, hcd.ne, fun l hl h ↦ ?_⟩
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
    forall_eq] at h
  refine habc.2.2.2.2.2.2 l hl (by simp [*, hl.close_left h.2.1 h.2.2 hacd])
Proof 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
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : NotCollinear b c d
⊢ False