internlm/Lean-Github huggingface dataset:
Theorem: case3
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₃
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₃
hPd : (a₃ :: l).getLast ⋯ = d
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ a₃
P' : List V := a₁ :: a₃ :: a₃ :: l
hP' : Delta a₃ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ a₃ a₃
⊢ False
Tactic:
refine hα.2.2.2 (Line a₁ a₃) (Line_isLine hb₁₂.ne12) ?_
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₃
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₃
hPd : (a₃ :: l).getLast ⋯ = d
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ a₃
P' : List V := a₁ :: a₃ :: a₃ :: l
hP' : Delta a₃ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ a₃ a₃
⊢ {a₁, a₂, a₃} ⊆ Line a₁ a₃
Theorem: case3
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₃
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₃
hPd : (a₃ :: l).getLast ⋯ = d
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ a₃
P' : List V := a₁ :: a₃ :: a₃ :: l
hP' : Delta a₃ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ a₃ a₃
⊢ {a₁, a₂, a₃} ⊆ Line a₁ a₃
Tactic:
simp [right_extend_mem_Line hb₁₂]
Proof state after:
no goals
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
⊢ List.Chain' (fun x x_1 => x ≠ x_1) P'
Tactic:
simp only [P', ne_eq, List.chain'_cons] at hPc
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₃
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hPc : ¬a₁ = a₂ ∧ ¬a₂ = a₃ ∧ List.Chain' (fun x x_1 => ¬x = x_1) (a₃ :: l)
⊢ List.Chain' (fun x x_1 => x ≠ x_1) P'
Theorem: case3
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₃
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : SimpleEdges.Adj a₂ a₃
b₁₂ : V
hb₁₂ : sbtw a₁ b₁₂ a₂
hba : SimpleEdges.Adj b₁₂ a₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hPc : ¬a₁ = a₂ ∧ ¬a₂ = a₃ ∧ List.Chain' (fun x x_1 => ¬x = x_1) (a₃ :: l)
⊢ List.Chain' (fun x x_1 => x ≠ x_1) P'
Tactic:
simp only [P', List.chain'_cons, and_true, ← ha₁, hb₁₂.ne12, true_and, not_false_eq_true, ne_eq,
  ha₃b₁₂.symm, hPc.2.2, hP'₁.2]
Proof state after:
no goals
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this✝ : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : dist a d ≤ P'.pathLength
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ [a, d].Sublist P'
Tactic:
rw [← ha₁, List.cons_sublist_cons, List.singleton_sublist]
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ d ∈ b₁₂ :: a₃ :: l
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ d ∈ b₁₂ :: a₃ :: l
Tactic:
have : d ∈ a₃ :: l := by rw [← hPd]; exact List.getLast_mem _
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this✝ : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : d ∈ a₃ :: l
⊢ d ∈ b₁₂ :: a₃ :: l
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this✝ : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : d ∈ a₃ :: l
⊢ d ∈ b₁₂ :: a₃ :: l
Tactic:
rw [List.mem_cons]
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this✝ : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : d ∈ a₃ :: l
⊢ d = b₁₂ ∨ d ∈ a₃ :: l
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this✝ : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : d ∈ a₃ :: l
⊢ d = b₁₂ ∨ d ∈ a₃ :: l
Tactic:
simp only [this, or_true]
Proof state after:
no goals
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ d ∈ a₃ :: l
Tactic:
rw [← hPd]
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ (a₃ :: l).getLast ⋯ ∈ a₃ :: l
Theorem: case3
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ a₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ a₃
ha₃b₁₂ : a₃ ≠ b₁₂
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
hP'ns : SimpleEdges.Adj a₁ b₁₂ ∧ SimpleEdges.Adj b₁₂ a₃
this : Delta a b c ≤ Delta b₁₂ a₂ a₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ (a₃ :: l).getLast ⋯ ∈ a₃ :: l
Tactic:
exact List.getLast_mem _
Proof state after:
no goals
Theorem: two_implies_three
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, SimpleTriangle x y z
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
let S : Set (V × V × V) := setOf (fun ⟨x, y, z⟩ => SimpleTriangle x y z)
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Theorem: two_implies_three
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Theorem: two_implies_three
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
obtain ⟨⟨a, b, c⟩, (habc : SimpleTriangle a b c), hmin⟩ :=
  S.toFinite.exists_minimal_wrt (fun ⟨x, y, z⟩ => Delta x y z) 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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Theorem: two_implies_three
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
replace hmin : ∀ a' b' c' : V, SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c' := by
  intro a' b' c' h
  by_contra! h'
  exact h'.ne' (hmin (a', b', c') h 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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Theorem: two_implies_three
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
⊢ ∃ a b, a ≠ b ∧ Line a b = {a, b}
Tactic:
refine ⟨a, c, habc.2.2.1.1.symm, ?_⟩
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, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
⊢ Line a c = {a, c}