internlm/Lean-Github huggingface dataset:
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₂₃
hb : NotCollinear b₁₂ a₂ b₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP'✝ : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP' : List.Special a b d P'
⊢ False
Tactic:
linarith [hPmin _ hP']
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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l).getLast ⋯ = d
⊢ NotCollinear a₁ b₁₂ 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : {a₁, b₁₂, 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : {a₁, b₁₂, 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₁₂ ∈ 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₁₂ ∈ l ∧ b₂₃ ∈ l
⊢ False
Tactic:
have ha₂ : a₂ ∈ l := hl.close_right 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₁₂ ∈ l ∧ b₂₃ ∈ l
ha₂ : a₂ ∈ 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₁₂ ∈ l ∧ b₂₃ ∈ l
ha₂ : a₂ ∈ l
⊢ False
Tactic:
exact hα.2.2.2 l hl (by simp [hl'.1, ha₂, hl.close_right ha₂ hl'.2.2 hb₂₃])
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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l✝
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l✝).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l✝).pathLength
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l✝).getLast ⋯ = d
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₁₂ ∈ l ∧ b₂₃ ∈ l
ha₂ : a₂ ∈ l
⊢ {a₁, a₂, a₃} ⊆ l
Tactic:
simp [hl'.1, ha₂, hl.close_right ha₂ hl'.2.2 hb₂₃]
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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
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₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
⊢ a₃ ≠ b₁₂
Tactic:
rintro rfl
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hPd : (a₃ :: l).getLast ⋯ = d
ha₃b₂₃ : a₃ ≠ b₂₃
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ b₂₃
P' : List V := a₁ :: a₃ :: b₂₃ :: a₃ :: l
hP' : Delta a₃ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ 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₃
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hPd : (a₃ :: l).getLast ⋯ = d
ha₃b₂₃ : a₃ ≠ b₂₃
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ b₂₃
P' : List V := a₁ :: a₃ :: b₂₃ :: a₃ :: l
hP' : Delta a₃ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ a₃ b₂₃
⊢ 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₃
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
hPd : (a₃ :: l).getLast ⋯ = d
ha₃b₂₃ : a₃ ≠ b₂₃
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ b₂₃
P' : List V := a₁ :: a₃ :: b₂₃ :: a₃ :: l
hP' : Delta a₃ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ a₃ b₂₃
⊢ {a₁, a₂, a₃} ⊆ Line a₁ a₃
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₃
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hPd : (a₃ :: l).getLast ⋯ = d
ha₃b₂₃ : a₃ ≠ b₂₃
hb₁₂ : sbtw a₁ a₃ a₂
hba : SimpleEdges.Adj a₃ a₂
hb : NotCollinear a₃ a₂ b₂₃
P' : List V := a₁ :: a₃ :: b₂₃ :: a₃ :: l
hP' : Delta a₃ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₃ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hP'ns : ¬List.Special a b d P'
hP'₁ : NotCollinear a₁ a₃ b₂₃
⊢ {a₁, a₂, a₃} ⊆ Line a₁ a₃
Tactic:
simp [right_extend_mem_Line hb₁₂]
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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
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₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
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₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear b₁₂ a₂ b₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
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₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
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: 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
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₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
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, ha₃b₂₃.symm, hPc.2.2, hP'₁.2]
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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
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₁₂ b₂₃
this✝ : Delta a b c ≤ Delta b₁₂ a₂ b₂₃
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: 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₃
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₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
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₁₂ b₂₃
this : Delta a b c ≤ Delta b₁₂ a₂ b₂₃
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₂
b₂₃ : V
hb₂₃ : sbtw a₂ b₂₃ a₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear b₁₂ a₂ b₂₃
P' : List V := a₁ :: b₁₂ :: b₂₃ :: a₃ :: l
hP' : Delta b₁₂ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta b₁₂ a₂ b₂₃
hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
hPd : (a₃ :: l).getLast ⋯ = d
hP'₁ : NotCollinear a₁ b₁₂ b₂₃
ha₃b₂₃ : a₃ ≠ b₂₃
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₁₂ b₂₃
this : Delta a b c ≤ Delta b₁₂ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ d ∈ b₁₂ :: b₂₃ :: a₃ :: l