internlm/Lean-Github huggingface dataset:
Theorem: NotCollinear.mk
Proof 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
Proof state after:
no goals
Theorem: NotCollinear.rotate
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 : NotCollinear u v w
l : Set V
h₁ : l.IsLine
h₂ : {v, w, u} ⊆ l
⊢ {u, v, w} ≤ {v, w, u}
Tactic:
simp
Proof state after:
no goals
Theorem: NotCollinear.swap
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 : NotCollinear u v w
l : Set V
h₁ : l.IsLine
h₂ : {w, v, u} ⊆ l
⊢ {u, v, w} ≤ {w, v, u}
Tactic:
simp
Proof state after:
no goals
Theorem: thm_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 : V), ¬NotCollinear x y z
⊢ Set.univ.IsLine
Tactic:
let S : Set (Set V) := setOf Set.IsLine
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
⊢ Set.univ.IsLine
Theorem: thm_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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
⊢ Set.univ.IsLine
Tactic:
have : S.Nonempty := let ⟨x, y, hxy⟩ := exists_pair_ne V; ⟨_, Line_isLine hxy⟩
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
⊢ Set.univ.IsLine
Theorem: thm_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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
⊢ Set.univ.IsLine
Tactic:
obtain ⟨L, hL, hL'⟩ := S.toFinite.exists_maximal_wrt id S this
Proof state after:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, id L ≤ id a' → id L = id a'
⊢ Set.univ.IsLine
Theorem: thm_two
Proof state before:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, id L ≤ id a' → id L = id a'
⊢ Set.univ.IsLine
Tactic:
dsimp at hL'
Proof state after:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ Set.univ.IsLine
Theorem: thm_two
Proof state before:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ Set.univ.IsLine
Tactic:
suffices L = Set.univ by rwa [← this]
Proof state after:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ L = Set.univ
Theorem: thm_two
Proof state before:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ L = Set.univ
Tactic:
rw [Set.eq_univ_iff_forall]
Proof state after:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ ∀ (x : V), x ∈ L
Theorem: thm_two
Proof state before:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ ∀ (x : V), x ∈ L
Tactic:
by_contra!
Proof state after:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
this : ∃ x, x ∉ L
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
this : ∃ x, x ∉ L
⊢ False
Tactic:
obtain ⟨a, b, hab, rfl⟩ := hL
Proof state after:
case intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
this : ∃ x, x ∉ Line a b
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
this : ∃ x, x ∉ Line a b
⊢ False
Tactic:
obtain ⟨c, hc'⟩ := this
Proof state after:
case intro.intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
⊢ False
Tactic:
have hac : a ≠ c := fun h => hc' (subset_generateLine _ (by simp [h]))
Proof state after:
case intro.intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
⊢ False
Tactic:
have hbc : b ≠ c := fun h => hc' (subset_generateLine _ (by simp [h]))
Proof state after:
case intro.intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro
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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Tactic:
simp only [NotCollinear, not_and, not_forall, not_not] at h
Proof state after:
case intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
⊢ False
Tactic:
obtain ⟨M, hM, habc⟩ := h a b c hab hac hbc
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
⊢ False
Tactic:
have := hL' M hM (Set.IsLine.generateLine_subset (habc.trans' (by simp)) hM)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False
Tactic:
rw [this] at hc'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hc' : c ∉ M
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False
Theorem: thm_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hc' : c ∉ M
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ False
Tactic:
exact hc' (habc (by simp))
Proof state after:
no goals
Theorem: thm_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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
this : L = Set.univ
⊢ Set.univ.IsLine
Tactic:
rwa [← this]
Proof state after:
no goals
Theorem: thm_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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
h : a = c
⊢ c ∈ {a, b}
Tactic:
simp [h]
Proof state after:
no goals
Theorem: thm_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 : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
h : b = c
⊢ c ∈ {a, b}
Tactic:
simp [h]
Proof state after:
no goals
Theorem: thm_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
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hc' : c ∉ Line a b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hM : M.IsLine
habc : {a, b, c} ⊆ M
⊢ {a, b} ≤ {a, b, c}
Tactic:
simp
Proof state after:
no goals
Theorem: thm_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
S : Set (Set V) := setOf Set.IsLine
this✝ : S.Nonempty
a b : V
hab : a ≠ b
hL' : ∀ a' ∈ S, (∀ x ∈ Line a b, x ∈ a') → Line a b = a'
c : V
hac : a ≠ c
hbc : b ≠ c
h : ∀ (x y z : V), x ≠ y → x ≠ z → y ≠ z → ∃ x_1, ∃ (_ : x_1.IsLine), {x, y, z} ⊆ x_1
M : Set V
hc' : c ∉ M
hM : M.IsLine
habc : {a, b, c} ⊆ M
this : Line a b = M
⊢ c ∈ {a, b, c}
Tactic:
simp
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
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
let S : Set (V × V × V) := setOf (fun ⟨a, b, c⟩ => NotCollinear a b c)
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}
⊢ ∃ x y z, SimpleTriangle x y z
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}
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
have : S.Nonempty := let ⟨x, y, z, hxyz⟩ := h; ⟨(x, y, z), hxyz⟩
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
⊢ ∃ x y z, SimpleTriangle x y z
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
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
let f : V × V × V → ℝ := fun ⟨a, b, c⟩ => dist a b + dist b c + dist c a
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
⊢ ∃ x y z, SimpleTriangle x y z
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
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
obtain ⟨⟨a, b, c⟩, (h₁ : NotCollinear _ _ _), h₂⟩ := S.toFinite.exists_minimal_wrt f S this
Proof state after:
case intro.mk.mk.intro
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' ∈ S, f a' ≤ f (a, b, c) → f (a, b, c) = f a'
⊢ ∃ x y z, SimpleTriangle x y z
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro
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' ∈ S, f a' ≤ f (a, b, c) → f (a, b, c) = f a'
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
simp only [Prod.forall, Set.mem_setOf_eq] at h₂
Proof state after:
case intro.mk.mk.intro
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
⊢ ∃ x y z, SimpleTriangle x y z
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro
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_1 a_2 b_1 : V), (a_1, a_2, b_1) ∈ S → f (a_1, a_2, b_1) ≤ f (a, b, c) → f (a, b, c) = f (a_1, a_2, b_1)
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
replace 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' := by
  intro a' b' c' hL
  by_contra! h
  exact h.ne' (h₂ a' b' c' hL h.le)
Proof state after:
case intro.mk.mk.intro
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'
⊢ ∃ x y z, SimpleTriangle x y z
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro
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'
⊢ ∃ x y z, SimpleTriangle x y z
Tactic:
simp only [SimpleTriangle]
Proof state after:
case intro.mk.mk.intro
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'
⊢ ∃ x y z, SimpleEdges.Adj x y ∧ SimpleEdges.Adj y z ∧ SimpleEdges.Adj z x ∧ NotCollinear x y z
Theorem: one_implies_two
Proof state before:
case intro.mk.mk.intro
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'
⊢ ∃ x y z, SimpleEdges.Adj x y ∧ SimpleEdges.Adj y z ∧ SimpleEdges.Adj z x ∧ NotCollinear x y z
Tactic:
by_contra! cont
Proof state after:
case intro.mk.mk.intro
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
⊢ False