replace hP'ns : ¬ P'.Special a b d := fun hP' ↦ by linarith [hPmin _ hP']
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
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