Theorem: eqn_9 (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 : V
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ P.pathLength < dist a d + Delta a b c
Tactic:
refine (hP' [a, b, d] (abd_special habc hacd hbd' hbd)).trans_lt ?_
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 : V
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ [a, b, d].pathLength < dist a d + Delta a b c

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 : V
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ [a, b, d].pathLength < dist a d + Delta a b c
Tactic:
rw [List.pathLength, List.pathLength, List.pathLength, add_zero]
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 : V
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ dist a b + dist b d < dist a d + Delta a b c

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 : V
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ dist a b + dist b d < dist a d + Delta a b c
Tactic:
exact eqn_8 habc hacd
State after:
no goals