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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
⊢ False
Tactic:
have hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength := by
  simp only [List.pathLength, Delta]; linarith [hb₁₂.dist]
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
⊢ False
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₃
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₂
hb : NotCollinear b₁₂ a₂ a₃
P' : List V := a₁ :: b₁₂ :: a₃ :: l
hP' : Delta b₁₂ a₂ a₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
⊢ False
Tactic:
have hd : 0 < Delta b₁₂ a₂ a₃ := Delta_pos_of 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₂
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₃
⊢ False
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₃
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₂
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₃
⊢ False
Tactic:
have hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength := by linarith
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₂
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
⊢ False
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₃
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₂
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
⊢ False
Tactic:
replace hP'ns : ¬ P'.Special a b d := fun hP' ↦ by linarith [hPmin _ hP']
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₂
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'
⊢ False
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₃
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₂
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'
⊢ False
Tactic:
simp only [ne_eq, not_false_eq_true, List.getLast_cons] at 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
hP'ns : ¬List.Special a b d P'
hPd : (a₃ :: l).getLast ⋯ = d
⊢ False
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
⊢ False
Tactic:
have hP'₁ : NotCollinear a₁ b₁₂ a₃ := 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'
  exact hα.2.2.2 l hl (by simp [hl'.1, hl.close_right hl'.1 hl'.2.1 hb₁₂, hl'.2.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₃
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₃
⊢ False
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₃
⊢ False
Tactic:
have ha₃b₁₂ : a₃ ≠ b₁₂ := by
  rintro rfl
  refine hα.2.2.2 (Line a₁ a₃) (Line_isLine hb₁₂.ne12) ?_
  simp [right_extend_mem_Line 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₂
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₁₂
⊢ False
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₁₂
⊢ False
Tactic:
have hP'₂ : P'.pathLength ≤ (a₁ :: b :: d :: []).pathLength :=
  ha₁ ▸ hP'lt.le.trans (hPmin _ (abd_special habc hacd hbd' hbd))
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
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
⊢ False
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
hP'₃ : List.Chain' (fun x x_1 => x ≠ x_1) P'
⊢ False
Tactic:
simp only [List.Special, hP'₁, List.getLast_cons_cons, List.getLast_cons_cons, hPd,
  hP'₂, hP'₃, ← ha₁, and_true, true_and, not_or, not_not] at hP'ns
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₃
⊢ False
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₃
⊢ False
Tactic:
have : SimpleTriangle b₁₂ a₂ a₃ := ⟨hba, c₁2, hP'ns.2.symm, 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₂
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 : SimpleTriangle b₁₂ a₂ a₃
⊢ False
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 : SimpleTriangle b₁₂ a₂ a₃
⊢ False
Tactic:
replace := habc_min _ _ _ this
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₃
⊢ False