internlm/Lean-Github huggingface dataset:
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
Proof state before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊
Tactic:
have := length_mul_le_pathLength_add hr.le hr' hl
Proof state after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ l.length ≤ ⌊R / r + 1⌋₊
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
Proof state before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ l.length ≤ ⌊R / r + 1⌋₊
Tactic:
rw [Nat.le_floor_iff, div_add_one hr.ne', le_div_iff hr]
Proof state after:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ ↑l.length * r ≤ R + r

V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ 0 ≤ R / r + 1
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
Proof state before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ ↑l.length * r ≤ R + r
Tactic:
linarith
Proof state after:
no goals
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
Proof state before:
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
this : ↑l.length * r ≤ l.pathLength + r
⊢ 0 ≤ R / r + 1
Tactic:
positivity
Proof state after:
no goals
Theorem: abd_special
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
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]
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
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
⊢ ∀ (l : Set V), l.IsLine → ¬(a ∈ l ∧ b ∈ l ∧ d ∈ l)
Theorem: abd_special
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
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'
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
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
Theorem: abd_special
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
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]
Proof state after:
no goals
Theorem: abd_special
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
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]
Proof state after:
no goals
Theorem: eqn_9
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
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ P.pathLength < dist a d + Delta a b c
Tactic:
refine (hP' [a, b, d] (abd_special habc hacd hbd' hbd)).trans_lt ?_
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
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ [a, b, d].pathLength < dist a d + Delta a b c
Theorem: eqn_9
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
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ [a, b, d].pathLength < dist a d + Delta a b c
Tactic:
rw [List.pathLength, List.pathLength, List.pathLength, add_zero]
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
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ dist a b + dist b d < dist a d + Delta a b c
Theorem: eqn_9
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
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ dist a b + dist b d < dist a d + Delta a b c
Tactic:
exact eqn_8 habc hacd
Proof state after:
no goals
Theorem: exists_simple_split_right
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
hab' : ¬SimpleEdges.Adj a b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
simp only [SimpleEdges_adj, hab, not_false_eq_true, true_and, ne_eq, not_forall, not_not] at hab'
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
hab' : ∃ x, sbtw a x b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Theorem: exists_simple_split_right
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
hab' : ∃ x, sbtw a x b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
obtain ⟨c', hc'⟩ := hab'
Proof state after:
case intro
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
c' : V
hc' : sbtw a c' b
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Theorem: exists_simple_split_right
Proof state before:
case intro
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
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
obtain ⟨c, hc : sbtw _ c _, hcmin⟩ := S.toFinite.exists_minimal_wrt (dist b) _ ⟨c', hc'⟩
Proof state after:
case intro.intro.intro
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
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Theorem: exists_simple_split_right
Proof state before:
case intro.intro.intro
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
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
Tactic:
refine ⟨c, hc, hc.ne23, fun c' hc' => ?_⟩
Proof state after:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
⊢ False
Theorem: exists_simple_split_right
Proof state before:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
⊢ False
Tactic:
have : dist b c ≤ dist b c' :=
  le_of_not_lt fun h => h.ne' <| hcmin _ (hc.trans_right' hc') h.le
Proof state after:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist b c ≤ dist b c'
⊢ False
Theorem: exists_simple_split_right
Proof state before:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist b c ≤ dist b c'
⊢ False
Tactic:
rw [dist_comm b, dist_comm b] at this
Proof state after:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist c b ≤ dist c' b
⊢ False
Theorem: exists_simple_split_right
Proof state before:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist c b ≤ dist c' b
⊢ False
Tactic:
have : dist c c' ≤ 0 := by linarith [hc'.dist]
Proof state after:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : dist c c' ≤ 0
⊢ False
Theorem: exists_simple_split_right
Proof state before:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : dist c c' ≤ 0
⊢ False
Tactic:
simp only [dist_le_zero] at this
Proof state after:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : c = c'
⊢ False
Theorem: exists_simple_split_right
Proof state before:
case intro.intro.intro
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this✝ : dist c b ≤ dist c' b
this : c = c'
⊢ False
Tactic:
exact hc'.ne12 this
Proof state after:
no goals
Theorem: exists_simple_split_right
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
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist c b ≤ dist c' b
⊢ dist c c' ≤ 0
Tactic:
linarith [hc'.dist]
Proof state after:
no goals
Theorem: case1
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
⊢ a₁ :: a₂ :: a₃ :: l ≠ []
Tactic:
simp
Proof state after:
no goals
Theorem: case1
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
have ⟨b₁₂, hb₁₂, hba⟩ := exists_simple_split_right hα.1 c₁1
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
⊢ False
Theorem: case1
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
⊢ False
Tactic:
have ⟨b₂₃, hb₂₃, hab⟩ := exists_simple_split_left hα.2.2.1 c₁2
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
⊢ False
Theorem: case1
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
⊢ False
Tactic:
have hb : NotCollinear b₁₂ a₂ b₂₃ := by
  refine NotCollinear.mk fun l hl hl' ↦ ?_
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
    forall_eq] at hl'
  have : a₁ ∈ l := hl.close_left hl'.1 hl'.2.1 hb₁₂
  have : a₃ ∈ l := hl.close_right hl'.2.1 hl'.2.2 hb₂₃
  exact hα.2.2.2 l hl (by simp [*, -ha₁])
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear b₁₂ a₂ b₂₃
⊢ False
Theorem: case1
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 a₁ a₂ a₃ : V
l : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
⊢ NotCollinear b₁₂ a₂ b₂₃
Tactic:
refine NotCollinear.mk fun l hl hl' ↦ ?_
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 a₁ a₂ a₃ : V
l✝ : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l✝).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l✝).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l✝)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : {b₁₂, a₂, b₂₃} ⊆ l
⊢ False
Theorem: case1
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 a₁ a₂ a₃ : V
l✝ : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l✝).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l✝).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l✝)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : {b₁₂, a₂, b₂₃} ⊆ l
⊢ False
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
  forall_eq] at hl'
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 a₁ a₂ a₃ : V
l✝ : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l✝).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l✝).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l✝)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : b₁₂ ∈ l ∧ a₂ ∈ l ∧ b₂₃ ∈ l
⊢ False
Theorem: case1
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 a₁ a₂ a₃ : V
l✝ : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l✝).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l✝).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l✝)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : b₁₂ ∈ l ∧ a₂ ∈ l ∧ b₂₃ ∈ l
⊢ False
Tactic:
have : a₁ ∈ l := hl.close_left hl'.1 hl'.2.1 hb₁₂
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 a₁ a₂ a₃ : V
l✝ : List 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
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l✝).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l✝).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l✝)
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : b₁₂ ∈ l ∧ a₂ ∈ l ∧ b₂₃ ∈ l
this : a₁ ∈ l
⊢ False