Theorem: case2 (LeanCamCombi/SylvesterChvatal.lean)

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
State after:
no goals

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₂₃, hab⟩ := exists_simple_split_left hα.2.2.1 c₁2
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₃
hab : SimpleEdges.Adj a₂ b₂₃
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
⊢ False
Tactic:
have hb : NotCollinear a₁ 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'
  exact hα.2.2.2 l hl (by simp [hl'.1, hl'.2.1, hl.close_right hl'.2.1 hl'.2.2 hb₂₃])
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
⊢ 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'
  have : a₂ ∈ l := hl.close_left hl'.2.1 hl'.2.2 hb₂₃
  exact hα.2.2.2 l hl (by simp [*, -ha₁])
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
⊢ NotCollinear a₁ a₂ b₂₃
Tactic:
refine NotCollinear.mk fun l hl hl' => ?_
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₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : {a₁, a₂, b₂₃} ⊆ l
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : {a₁, 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'
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₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ a₂ ∈ l ∧ b₂₃ ∈ l
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ a₂ ∈ l ∧ b₂₃ ∈ l
⊢ False
Tactic:
exact hα.2.2.2 l hl (by simp [hl'.1, hl'.2.1, hl.close_right hl'.2.1 hl'.2.2 hb₂₃])
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ a₂ ∈ l ∧ b₂₃ ∈ l
⊢ {a₁, a₂, a₃} ⊆ l
Tactic:
simp [hl'.1, hl'.2.1, hl.close_right hl'.2.1 hl'.2.2 hb₂₃]
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
⊢ NotCollinear a₁ b₂₃ a₃
Tactic:
refine NotCollinear.mk fun l hl hl' ↦ ?_
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : {a₁, b₂₃, a₃} ⊆ l
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : {a₁, b₂₃, a₃} ⊆ l
⊢ False
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
  forall_eq] at hl'
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₂₃ ∈ l ∧ a₃ ∈ l
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₂₃ ∈ l ∧ a₃ ∈ l
⊢ False
Tactic:
have : a₂ ∈ l := hl.close_left hl'.2.1 hl'.2.2 hb₂₃
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₂₃ ∈ l ∧ a₃ ∈ l
this : a₂ ∈ l
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₂₃ ∈ l ∧ a₃ ∈ l
this : a₂ ∈ l
⊢ False
Tactic:
exact hα.2.2.2 l hl (by simp [*, -ha₁])
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
l : Set V
hl : l.IsLine
hl' : a₁ ∈ l ∧ b₂₃ ∈ l ∧ a₃ ∈ l
this : a₂ ∈ l
⊢ {a₁, a₂, a₃} ⊆ l
Tactic:
simp [*, -ha₁]
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
⊢ False
Tactic:
let P' : List V := a₁ :: b₂₃ :: a₃ :: l
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
⊢ False
Tactic:
have hP' : Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength := by
  simp only [List.pathLength, Delta]; linarith [hb₂₃.dist]
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
hP' : Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
hP' : Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
⊢ False
Tactic:
have hd : 0 < Delta a₁ a₂ b₂₃ := Delta_pos_of hb
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
hP' : Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₁ a₂ b₂₃
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
hP' : Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₁ a₂ b₂₃
⊢ False
Tactic:
have hP'lt : P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength := by linarith
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
⊢ False
Tactic:
replace hP'ns : ¬ P'.Special a b d := fun hP' ↦ by linarith [hPmin _ hP']
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
⊢ False

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
⊢ False
Tactic:
simp only [ne_eq, not_false_eq_true, List.getLast_cons] at hPd
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
⊢ False

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
⊢ False
Tactic:
have ha₃b₂₃ : a₃ ≠ b₂₃ := hb₂₃.ne23.symm
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
ha₃b₂₃ : a₃ ≠ b₂₃
⊢ False

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
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))
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
ha₃b₂₃ : a₃ ≠ b₂₃
hP'₂ : P'.pathLength ≤ [a₁, b, d].pathLength
⊢ False

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
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
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃ := ⟨c₁1, hab, hP'ns.1.symm, hb⟩
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
⊢ False

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
⊢ False
Tactic:
replace := habc_min _ _ _ this
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
⊢ False

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
⊢ False
Tactic:
have h9 := eqn_9 habc hacd hbd' hbd hPmin
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ False

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ False
Tactic:
suffices dist a d ≤ P'.pathLength by linarith
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ dist a d ≤ P'.pathLength

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ dist a d ≤ P'.pathLength
Tactic:
have : List.Sublist [a, d] P' := by
  rw [← ha₁, List.cons_sublist_cons, List.singleton_sublist]
  have : d ∈ a₃ :: l := by rw [← hPd]; exact List.getLast_mem _
  rw [List.mem_cons]
  simp only [this, or_true]
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : [a, d].Sublist P'
⊢ dist a d ≤ P'.pathLength

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : [a, d].Sublist P'
⊢ dist a d ≤ P'.pathLength
Tactic:
have := List.Sublist.pathLength_sublist this
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this✝ : [a, d].Sublist P'
this : [a, d].pathLength ≤ P'.pathLength
⊢ dist a d ≤ P'.pathLength

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this✝ : [a, d].Sublist P'
this : [a, d].pathLength ≤ P'.pathLength
⊢ dist a d ≤ P'.pathLength
Tactic:
rwa [List.pathLength, List.pathLength, add_zero] at this
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
⊢ Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
Tactic:
simp only [List.pathLength, Delta]
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
⊢ dist a₁ a₂ + dist a₂ b₂₃ - dist a₁ b₂₃ =
    dist a₁ a₂ + (dist a₂ a₃ + (a₃ :: l).pathLength) - (dist a₁ b₂₃ + (dist b₂₃ a₃ + (a₃ :: l).pathLength))

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
⊢ dist a₁ a₂ + dist a₂ b₂₃ - dist a₁ b₂₃ =
    dist a₁ a₂ + (dist a₂ a₃ + (a₃ :: l).pathLength) - (dist a₁ b₂₃ + (dist b₂₃ a₃ + (a₃ :: l).pathLength))
Tactic:
linarith [hb₂₃.dist]
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := a₁ :: b₂₃ :: a₃ :: l
hP' : Delta a₁ a₂ b₂₃ = (a₁ :: a₂ :: a₃ :: l).pathLength - P'.pathLength
hd : 0 < Delta a₁ a₂ b₂₃
⊢ P'.pathLength < (a₁ :: a₂ :: a₃ :: l).pathLength
Tactic:
linarith
State after:
no goals

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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' : List.Special a b d P'
⊢ False
Tactic:
linarith [hPmin _ hP']
State after:
no goals

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
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
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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
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'

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₃
hab : SimpleEdges.Adj a₂ b₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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'
hPd : (a₃ :: l).getLast ⋯ = d
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₁, true_and, not_false_eq_true, ne_eq,
  ha₃b₂₃.symm, hPc.2.2, hP'₁.2, hP'₁.1]
State after:
no goals

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : dist a d ≤ P'.pathLength
⊢ False
Tactic:
linarith
State after:
no goals

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ 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]
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ d ∈ b₂₃ :: a₃ :: l

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
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 _
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : d ∈ a₃ :: l
⊢ d ∈ b₂₃ :: a₃ :: l

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
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]
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
this : d ∈ a₃ :: l
⊢ d = b₂₃ ∨ d ∈ a₃ :: l

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
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]
State after:
no goals

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ d ∈ a₃ :: l
Tactic:
rw [← hPd]
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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ (a₃ :: l).getLast ⋯ ∈ a₃ :: l

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₂₃
hb : NotCollinear a₁ a₂ b₂₃
hP'₁ : NotCollinear a₁ b₂₃ a₃
P' : List V := 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
hPd : (a₃ :: l).getLast ⋯ = d
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 a₁ a₂ b₂₃
h9 : (a₁ :: a₂ :: a₃ :: l).pathLength < dist a d + Delta a b c
⊢ (a₃ :: l).getLast ⋯ ∈ a₃ :: l
Tactic:
exact List.getLast_mem _
State after:
no goals