This set of lemmas states that a measure set from resolving will consist of measures whose last line length is bound by $W_F$

ink

theorem ResolveConcatOne_last : ∀ {α : Type} {F : Factory α} {d : Doc} {m_left : Meas} {i : ℕ} {ms : List Meas} {h_not_empty : ms ≠ []} {m : Meas}, ResolveConcatOne F d m_left i (MeasureSet.set ms h_not_empty) → m ∈ ms → m.last ≤ F.W

ink

theorem ResolveConcat_last : ∀ {α : Type} {ms : List Meas} {F : Factory α} {ms_in : List Meas} {d : Doc} {i : ℕ} {m : Meas} {h_not_empty : ms ≠ []}, ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty) → m ∈ ms → m.last ≤ F.W

ink

theorem Resolve_last : ∀ {α : Type} {ms : List Meas} {F : Factory α} {d : Doc} {c i : ℕ} {m : Meas} {h_not_empty : ms ≠ []}, Resolve F d c i (MeasureSet.set ms h_not_empty) → m ∈ ms → m.last ≤ F.W