import Pretty.Supports.ResolvePareto

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

mutual
  lemma 
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
ResolveConcatOne_last
      (
h: ResolveConcatOne F d m_left i (MeasureSet.set ms h_not_empty)
h : 
ResolveConcatOne: {α : Type} → Factory α → Doc → Meas → ℕ → MeasureSet → Prop
ResolveConcatOne 
F: ?m.4
F 
d: ?m.11
d 
m_left: ?m.17
m_left 
i: ?m.24
i (
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: ?m.33
ms 
h_not_empty: ?m.42
h_not_empty))
      (
h_in: m ∈ ms
h_in : 
m: ?m.70
m ∈ 
ms: ?m.33
ms) : 
      
m: ?m.70
m.
last: {α : Type} → Meas → ℕ
last ≤ 
F: ?m.4
F.
W: {α : Type} → Factory α → ℕ
W := by
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

ms: List Meas

h_not_empty: ms ≠ []

m: Meas

h: ResolveConcatOne F d m_left i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcases 
h: ResolveConcatOne F d m_left i (MeasureSet.set ms h_not_empty)
h
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h✝: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

set
m.last ≤ F.W 
    
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

ms: List Meas

h_not_empty: ms ≠ []

m: Meas

h: ResolveConcatOne F d m_left i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase set 
h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)
h => 
      
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

m.last ≤ F.Whave := 
dedup_member: ∀ {α : Type} {m : Meas} {F : Factory α} {ms : List Meas}, m ∈ dedup F ms → m ∈ ms
dedup_member 
h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)
h_in
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

this: m ∈ List.map (fun m' => Meas.concat F m_left m') ms✝

m.last ≤ F.W 
      
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

m.last ≤ F.Wsimp at 
this: ?m.788
this
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

this: ∃ a, a ∈ ms✝ ∧ Meas.concat F m_left a = m

m.last ≤ F.W 
      
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

m.last ≤ F.Wlet ⟨
m': Meas
m', 
h_mem: m' ∈ ms✝
h_mem, 
h': Meas.concat F m_left m' = m
h'⟩ := 
this: ∃ a, a ∈ ms✝ ∧ Meas.concat F m_left a = m
this
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

this: ∃ a, a ∈ ms✝ ∧ Meas.concat F m_left a = m

m': Meas

h_mem: m' ∈ ms✝

h': Meas.concat F m_left m' = m

m.last ≤ F.W
      
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

m.last ≤ F.Wsubst 
h': Meas.concat F m_left m' = m
h'
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

m': Meas

h_mem: m' ∈ ms✝

h_in: Meas.concat F m_left m' ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

this: ∃ a, a ∈ ms✝ ∧ Meas.concat F m_left a = Meas.concat F m_left m'

(Meas.concat F m_left m').last ≤ F.W 
      
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

m.last ≤ F.Wsimp [
Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat]
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

m': Meas

h_mem: m' ∈ ms✝

h_in: Meas.concat F m_left m' ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

this: ∃ a, a ∈ ms✝ ∧ Meas.concat F m_left a = Meas.concat F m_left m'

m'.last ≤ F.W
      
α✝: Type

F: Factory α✝

d: Doc

m_left: Meas

i: ℕ

m: Meas

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)

h_not_empty: dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝) ≠ []

h_in: m ∈ dedup F (List.map (fun m' => Meas.concat F m_left m') ms✝)

m.last ≤ F.Wexact 
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
Resolve_last 
h: Resolve F d m_left.last i (MeasureSet.set ms✝ h_non_empty✝)
h 
h_mem: m' ∈ ms✝
h_mem
Goals accomplished! 🐙 

  lemma 
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
ResolveConcat_last 
      {
h_not_empty: ms ≠ []
h_not_empty : 
ms: ?m.122
ms ≠ 
[]: unknown metavariable '?_uniq.128'
[]}
      (
h: ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty)
h : 
ResolveConcat: {α : Type} → Factory α → List Meas → Doc → ℕ → MeasureSet → Prop
ResolveConcat 
F: ?m.135
F 
ms_in: ?m.150
ms_in 
d: ?m.165
d 
i: ?m.179
i (
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: ?m.122
ms 
h_not_empty: ms ≠ []
h_not_empty))
      (
h_in: m ∈ ms
h_in : 
m: ?m.218
m ∈ 
ms: ?m.122
ms) : 
      
m: ?m.218
m.
last: {α : Type} → Meas → ℕ
last ≤ 
F: ?m.135
F.
W: {α : Type} → Factory α → ℕ
W := by
Goals accomplished! 🐙 
    
α✝: Type

ms: List Meas

F: Factory α✝

ms_in: List Meas

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wgeneralize h_meas : 
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: List Meas
ms 
h_not_empty: ms ≠ []
h_not_empty = ml at 
h: ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty)
h
α✝: Type

ms: List Meas

F: Factory α✝

ms_in: List Meas

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

h: ResolveConcat F ms_in d i ml

m.last ≤ F.W
    
α✝: Type

ms: List Meas

F: Factory α✝

ms_in: List Meas

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcases 
h: ResolveConcat F ms_in d i ml
h
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current✝: ResolveConcatOne F d m✝ i ml

one
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

msr✝: MeasureSet

m✝: Meas

msr'✝: MeasureSet

h_rest✝: ResolveConcat F ms✝ d i msr✝

h_current✝: ResolveConcatOne F d m✝ i msr'✝

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F msr'✝ msr✝

cons
m.last ≤ F.W 
    
α✝: Type

ms: List Meas

F: Factory α✝

ms_in: List Meas

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase one 
h_current: ResolveConcatOne F d m✝ i ml
h_current => 
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m.last ≤ F.Wsimp at 
h_in: m ∈ ms
h_in
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m.last ≤ F.W 
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m.last ≤ F.Wapply 
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
ResolveConcatOne_last
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

h
ResolveConcatOne F ?d ?m_left ?i (MeasureSet.set ?ms ?h_not_empty)
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

h_in
m ∈ ?ms
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

d
Doc
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m_left
Meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

i
ℕ
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

ms
List Meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

h_not_empty
?ms ≠ [] 
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m.last ≤ F.Wcase h => 
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

ResolveConcatOne F ?d ?m_left ?i (MeasureSet.set ?ms ?h_not_empty)subst 
h_meas: MeasureSet.set ms h_not_empty = ml
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

m✝: Meas

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms h_not_empty)

ResolveConcatOne F
  (?m.2912 (MeasureSet.set ms h_not_empty) (_ : MeasureSet.set ms h_not_empty = MeasureSet.set ms h_not_empty)
    h_current)
  (?m.2913 (MeasureSet.set ms h_not_empty) (_ : MeasureSet.set ms h_not_empty = MeasureSet.set ms h_not_empty)
    h_current)
  (?m.2914 (MeasureSet.set ms h_not_empty) (_ : MeasureSet.set ms h_not_empty = MeasureSet.set ms h_not_empty)
    h_current)
  (MeasureSet.set
    (?m.2915 (MeasureSet.set ms h_not_empty) (_ : MeasureSet.set ms h_not_empty = MeasureSet.set ms h_not_empty)
      h_current)
    (_ :
      ?m.2915 (MeasureSet.set ms h_not_empty) (_ : MeasureSet.set ms h_not_empty = MeasureSet.set ms h_not_empty)
          h_current ≠         []))
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

ResolveConcatOne F ?d ?m_left ?i (MeasureSet.set ?ms ?h_not_empty)apply 
h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms h_not_empty)
h_current
Goals accomplished! 🐙
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m.last ≤ F.Wcase h_in => 
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

m✝: Meas

h_current: ResolveConcatOne F d m✝ i ml

m ∈ msassumption
Goals accomplished! 🐙
    
α✝: Type

ms: List Meas

F: Factory α✝

ms_in: List Meas

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: ResolveConcat F ms_in d i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase cons 
ms': MeasureSet
ms' _ 
ms'': MeasureSet
ms'' 
h_rest: ResolveConcat F ms✝ d i ms'
h_rest 
h_current: ResolveConcatOne F d m✝ i ms''
h_current => 
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

ms': MeasureSet

m✝: Meas

ms'': MeasureSet

h_rest: ResolveConcat F ms✝ d i ms'

h_current: ResolveConcatOne F d m✝ i ms''

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' ms'

m.last ≤ F.Wcases 
ms': MeasureSet
ms'
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝¹ i ms''

m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

tainted
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝ i ms''

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h✝)

set
m.last ≤ F.W 
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

ms': MeasureSet

m✝: Meas

ms'': MeasureSet

h_rest: ResolveConcat F ms✝ d i ms'

h_current: ResolveConcatOne F d m✝ i ms''

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' ms'

m.last ≤ F.Wcase tainted => 
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝¹ i ms''

m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

m.last ≤ F.Wsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝¹ i ms''

m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = ms''

m.last ≤ F.W 
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝¹ i ms''

m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

m.last ≤ F.Wsubst 
h_meas: MeasureSet.set ms h_not_empty = ms''
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

m.last ≤ F.W 
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝¹ i ms''

m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

m.last ≤ F.Wdwi { 
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wapply 
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
ResolveConcatOne_last
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

h
ResolveConcatOne F ?d ?m_left ?i (MeasureSet.set ?ms ?h_not_empty)
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

h_in
m ∈ ?ms
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

d
Doc
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

m_left
Meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

i
ℕ
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

ms
List Meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_rest: ResolveConcat F ms✝ d i (MeasureSet.tainted m✝)

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.set ms h_not_empty)

h_not_empty
?ms ≠ [] }
Goals accomplished! 🐙
      
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

ms': MeasureSet

m✝: Meas

ms'': MeasureSet

h_rest: ResolveConcat F ms✝ d i ms'

h_current: ResolveConcatOne F d m✝ i ms''

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' ms'

m.last ≤ F.Wcase set => 
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝ i ms''

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wcases 
ms'': MeasureSet
ms''
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

m✝: Meas

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

tainted
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

set
m.last ≤ F.W 
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝ i ms''

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wcase tainted => 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

m✝: Meas

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

m✝: Meas

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.tainted m✝)

h_meas: ms = ms✝

m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

m✝: Meas

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsubst 
h_meas: ms = ms✝
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝: List Meas

m✝¹, m✝: Meas

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.tainted m✝)

h✝: ms ≠ []

h_rest: ResolveConcat F ms✝ d i (MeasureSet.set ms h✝)

m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

m✝: Meas

h_current: ResolveConcatOne F d m✝¹ i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wapply 
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
ResolveConcat_last 
h_rest: ResolveConcat F ms✝ d i (MeasureSet.set ms h✝)
h_rest 
h_in: m ∈ ms
h_in
Goals accomplished! 🐙
        
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝¹: List Meas

m✝: Meas

ms'': MeasureSet

h_current: ResolveConcatOne F d m✝ i ms''

ms✝: List Meas

h✝: ms✝ ≠ []

h_rest: ResolveConcat F ms✝¹ d i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wcase set => 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

m.last ≤ F.Wsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: ms = merge F (ms✝, ms✝¹)

m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

m.last ≤ F.Wsubst 
h_meas: ms = merge F (ms✝, ms✝¹)
h_meas
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

m.last ≤ F.Whave := 
merge_pareto_subset: ∀ {α : Type} {m : Meas} {F : Factory α} {ms₁ ms₂ : List Meas},
  m ∈ merge F (ms₁, ms₂) → pareto F ms₁ → pareto F ms₂ → m ∈ ms₁ ∨ m ∈ ms₂
merge_pareto_subset 
h_in: m ∈ merge F (ms✝, ms✝¹)
h_in (
ResolveConcatOne_pareto: ∀ {α : Type} {F : Factory α} {d : Doc} {m : Meas} {i : ℕ} {msr : List Meas} {h_non_empty : msr ≠ []},
  ResolveConcatOne F d m i (MeasureSet.set msr h_non_empty) → pareto F msr
ResolveConcatOne_pareto 
h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)
h_current) (
ResolveConcat_pareto: ∀ {α : Type} {F : Factory α} {ms : List Meas} {d : Doc} {i : ℕ} {msr : List Meas} {h_non_empty : msr ≠ []},
  ResolveConcat F ms d i (MeasureSet.set msr h_non_empty) → pareto F msr
ResolveConcat_pareto 
h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)
h_rest)
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

this: m ∈ ms✝ ∨ m ∈ ms✝¹

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

m.last ≤ F.Wcases 
this: ?m.7882
this
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝²: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝²)

ms✝: List Meas

h✝¹: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝¹)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h✝: m ∈ ms✝

inl
m.last ≤ F.W
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝²: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝²)

ms✝: List Meas

h✝¹: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝¹)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h✝: m ∈ ms✝¹

inr
m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

m.last ≤ F.Wcase inl 
h_in': ?m.7933
h_in' => 
            
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

m.last ≤ F.Wdwi { 
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

m.last ≤ F.Wapply 
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
ResolveConcatOne_last
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

h
ResolveConcatOne F ?d ?m_left ?i (MeasureSet.set ?ms ?h_not_empty)
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

h_in
m ∈ ?ms
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

d
Doc
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

m_left
Meas
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

i
ℕ
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

ms
List Meas
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

h_not_empty
?ms ≠ [] }
Goals accomplished! 🐙
          
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

m.last ≤ F.Wcase inr 
h_in': ?m.7934
h_in' =>
            
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

m: Meas

ms✝²: List Meas

m✝: Meas

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)

ms✝: List Meas

h✝: ms✝ ≠ []

h_current: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝¹

m.last ≤ F.Wapply 
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
ResolveConcat_last 
h_rest: ResolveConcat F ms✝² d i (MeasureSet.set ms✝¹ h✝¹)
h_rest 
h_in': ?m.7934
h_in'
Goals accomplished! 🐙
      
  lemma 
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
Resolve_last
      {
h_not_empty: ms ≠ []
h_not_empty : 
ms: ?m.281
ms ≠ 
[]: List ?m.383
[]}
      (
h: Resolve F d c i (MeasureSet.set ms h_not_empty)
h : 
Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve 
F: ?m.294
F 
d: ?m.309
d 
c: ?m.323
c 
i: ?m.337
i (
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: ?m.281
ms 
h_not_empty: ms ≠ []
h_not_empty)) 
      (
h_in: m ∈ ms
h_in : 
m: ?m.377
m ∈ 
ms: ?m.281
ms) : 
      
m: ?m.377
m.
last: {α : Type} → Meas → ℕ
last ≤ 
F: ?m.294
F.
W: {α : Type} → Factory α → ℕ
W := by
Goals accomplished! 🐙 
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcases 
d: Doc
d
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

s✝: String

h: Resolve F (Doc.text s✝) c i (MeasureSet.set ms h_not_empty)

text
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

h: Resolve F Doc.nl c i (MeasureSet.set ms h_not_empty)

nl
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

d₁✝, d₂✝: Doc

h: Resolve F (Doc.concat d₁✝ d₂✝) c i (MeasureSet.set ms h_not_empty)

concat
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

d✝: Doc

h: Resolve F (Doc.nest n✝ d✝) c i (MeasureSet.set ms h_not_empty)

nest
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

d✝: Doc

h: Resolve F (Doc.align d✝) c i (MeasureSet.set ms h_not_empty)

align
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

d₁✝, d₂✝: Doc

h: Resolve F (Doc.choice d₁✝ d₂✝) c i (MeasureSet.set ms h_not_empty)

choice
m.last ≤ F.W
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase text => 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

s✝: String

h: Resolve F (Doc.text s✝) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcases 
h: Resolve F (Doc.text s✝) c i (MeasureSet.set ms h_not_empty)
h
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c✝: c + String.length s✝ ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

text_set
m.last ≤ F.W 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

s✝: String

h: Resolve F (Doc.text s✝) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase text_set 
h_c: c + String.length s✝ ≤ F.W
h_c 
h_i: i ≤ F.W
h_i 
h_meas: MeasRender F (Doc.text s✝) c i m✝
h_meas => 
        
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wsimp at 
h_in: m ∈ [m✝]
h_in
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m = m✝

m.last ≤ F.W 
        
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wsubst 
h_in: m = m✝
h_in
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m

h_not_empty: [m] ≠ []

m.last ≤ F.W
        
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wcases 
h_meas: MeasRender F (Doc.text s✝) c i m
h_meas
α✝: Type

F: Factory α✝

c, i: ℕ

s✝: String

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_not_empty: [{ last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝,
      x := c + String.length s✝, y := i }] ≠   []

text
{ last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝,
      x := c + String.length s✝, y := i }.last ≤   F.W 
        
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wsimp
α✝: Type

F: Factory α✝

c, i: ℕ

s✝: String

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_not_empty: [{ last := c + String.length s✝, cost := Factory.text F c (String.length s✝), doc := Doc.text s✝,
      x := c + String.length s✝, y := i }] ≠   []

text
c + String.length s✝ ≤ F.W
        
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

s✝: String

m✝: Meas

h_c: c + String.length s✝ ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F (Doc.text s✝) c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wassumption
Goals accomplished! 🐙
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase nl => 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

h: Resolve F Doc.nl c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcases 
h: Resolve F Doc.nl c i (MeasureSet.set ms h_not_empty)
h
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h✝: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

line_set
m.last ≤ F.W 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

h: Resolve F Doc.nl c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase line_set 
h_c: c ≤ F.W
h_c 
h_i: i ≤ F.W
h_i 
h_meas: MeasRender F Doc.nl c i m✝
h_meas => 
        
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wsimp at 
h_in: m ∈ [m✝]
h_in
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m = m✝

m.last ≤ F.W 
        
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wsubst 
h_in: m = m✝
h_in
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m

h_not_empty: [m] ≠ []

m.last ≤ F.W
        
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wcases 
h_meas: MeasRender F Doc.nl c i m
h_meas
α✝: Type

F: Factory α✝

c, i: ℕ

h_c: c ≤ F.W

h_i: i ≤ F.W

h_not_empty: [{ last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }] ≠ []

nl
{ last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.last ≤ F.W 
        
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wsimp
α✝: Type

F: Factory α✝

c, i: ℕ

h_c: c ≤ F.W

h_i: i ≤ F.W

h_not_empty: [{ last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }] ≠ []

nl
i ≤ F.W
        
α✝: Type

F: Factory α✝

c, i: ℕ

m, m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

h_meas: MeasRender F Doc.nl c i m✝

h_not_empty: [m✝] ≠ []

h_in: m ∈ [m✝]

m.last ≤ F.Wassumption
Goals accomplished! 🐙
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase nest 
n: Type
n _ 
ih: Doc
ih => 
      
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

h: Resolve F (Doc.nest n✝ ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wgeneralize h_meas : 
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: List Meas
ms 
h_not_empty: ms ≠ []
h_not_empty = ml at 
h: Resolve F (Doc.nest n✝ ih) c i (MeasureSet.set ms h_not_empty)
h
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

h: Resolve F (Doc.nest n✝ ih) c i ml

m.last ≤ F.W
      
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

h: Resolve F (Doc.nest n✝ ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcases 
h: Resolve F (Doc.nest n✝ ih) c i ml
h
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: MeasureSet

h✝: Resolve F ih c (i + n✝) ms✝

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) ms✝

nest
m.last ≤ F.W
      
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

h: Resolve F (Doc.nest n✝ ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase nest 
ms': MeasureSet
ms' 
h: Resolve F ih c (i + n✝) ms'
h  => 
        
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms': MeasureSet

h: Resolve F ih c (i + n✝) ms'

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) ms'

m.last ≤ F.Wcases 
ms': MeasureSet
ms'
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

m✝: Meas

h: Resolve F ih c (i + n✝) (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.tainted m✝)

tainted
m.last ≤ F.W
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

set
m.last ≤ F.W 
        
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms': MeasureSet

h: Resolve F ih c (i + n✝) ms'

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) ms'

m.last ≤ F.Wcase tainted => 
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

m✝: Meas

h: Resolve F ih c (i + n✝) (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.tainted m✝)

m.last ≤ F.Wsimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.tainted m✝)
h_meas
Goals accomplished! 🐙
        
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms': MeasureSet

h: Resolve F ih c (i + n✝) ms'

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) ms'

m.last ≤ F.Wcase set => 
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)
h_meas
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: ms = List.map (Meas.adjust_nest n✝) ms✝

m.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsubst 
h_meas: ms = List.map (Meas.adjust_nest n✝) ms✝
h_meas
n: Type

F: Factory n

c, i: ℕ

m: Meas

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

h_in: m ∈ List.map (Meas.adjust_nest n✝) ms✝

m.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp at 
h_in: m ∈ List.map (Meas.adjust_nest n✝) ms✝
h_in
n: Type

F: Factory n

c, i: ℕ

m: Meas

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = m

m.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wlet ⟨
m': Meas
m', 
h_left: m' ∈ ms✝
h_left, 
h_right: Meas.adjust_nest n✝ m' = m
h_right⟩ := 
h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = m
h_in
n: Type

F: Factory n

c, i: ℕ

m: Meas

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = m

m': Meas

h_left: m' ∈ ms✝

h_right: Meas.adjust_nest n✝ m' = m

m.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Whave 
ih: ?m.15243
ih := 
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
Resolve_last 
h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)
h 
h_left: m' ∈ ms✝
h_left
n: Type

F: Factory n

c, i: ℕ

m: Meas

n✝: ℕ

ih✝: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = m

m': Meas

h_left: m' ∈ ms✝

h_right: Meas.adjust_nest n✝ m' = m

ih: m'.last ≤ F.W

m.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [
Meas.adjust_nest: {α : Type} → ℕ → Meas → Meas
Meas.adjust_nest] at 
h_right: Meas.adjust_nest n✝ m' = m
h_right
n: Type

F: Factory n

c, i: ℕ

m: Meas

n✝: ℕ

ih✝: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = m

m': Meas

h_left: m' ∈ ms✝

h_right: { last := m'.last, cost := m'.cost, doc := Doc.nest n✝ m'.doc, x := m'.x, y := m'.y } = m

ih: m'.last ≤ F.W

m.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wcases 
m: Meas
m
n: Type

F: Factory n

c, i, n✝: ℕ

ih✝: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

m': Meas

h_left: m' ∈ ms✝

ih: m'.last ≤ F.W

last✝: ℕ

cost✝: n

doc✝: Doc

x✝, y✝: ℕ

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

h_right: { last := m'.last, cost := m'.cost, doc := Doc.nest n✝ m'.doc, x := m'.x, y := m'.y } =   { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

mk
{ last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }.last ≤ F.W 
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp at 
h_right: { last := m'.last, cost := m'.cost, doc := Doc.nest n✝ m'.doc, x := m'.x, y := m'.y } =   { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }
h_right ⊢
n: Type

F: Factory n

c, i, n✝: ℕ

ih✝: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

m': Meas

h_left: m' ∈ ms✝

ih: m'.last ≤ F.W

last✝: ℕ

cost✝: n

doc✝: Doc

x✝, y✝: ℕ

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

h_right: m'.last = last✝ ∧ m'.cost = cost✝ ∧ Doc.nest n✝ m'.doc = doc✝ ∧ m'.x = x✝ ∧ m'.y = y✝

mk
last✝ ≤ F.W 
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [← 
h_right: m'.last = last✝ ∧ m'.cost = cost✝ ∧ Doc.nest n✝ m'.doc = doc✝ ∧ m'.x = x✝ ∧ m'.y = y✝
h_right.
left: ∀ {a b : Prop}, a ∧ b → a
left]
n: Type

F: Factory n

c, i, n✝: ℕ

ih✝: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c (i + n✝) (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_nest n✝) ms✝ ≠ []

m': Meas

h_left: m' ∈ ms✝

ih: m'.last ≤ F.W

last✝: ℕ

cost✝: n

doc✝: Doc

x✝, y✝: ℕ

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_nest n✝ a = { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

h_right: m'.last = last✝ ∧ m'.cost = cost✝ ∧ Doc.nest n✝ m'.doc = doc✝ ∧ m'.x = x✝ ∧ m'.y = y✝

mk
m'.last ≤ F.W
          
n: Type

ms: List Meas

F: Factory n

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

n✝: ℕ

ih: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c (i + n✝) (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_nest n✝) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wassumption
Goals accomplished! 🐙
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase align 
ih: Doc
ih => 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h: Resolve F (Doc.align ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wgeneralize h_meas : 
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: List Meas
ms 
h_not_empty: ms ≠ []
h_not_empty = ml at 
h: Resolve F (Doc.align ih) c i (MeasureSet.set ms h_not_empty)
h
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

h: Resolve F (Doc.align ih) c i ml

m.last ≤ F.W
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h: Resolve F (Doc.align ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcases 
h: Resolve F (Doc.align ih) c i ml
h
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

ms✝: MeasureSet

h✝: Resolve F ih c c ms✝

h_bad✝: i > F.W

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)

align_taint
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

ms✝: MeasureSet

h✝: Resolve F ih c c ms✝

h_ok✝: i ≤ F.W

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) ms✝

align
m.last ≤ F.W
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h: Resolve F (Doc.align ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase align 
ms': MeasureSet
ms' 
h: Resolve F ih c c ms'
h _ => 
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

ms': MeasureSet

h: Resolve F ih c c ms'

h_ok✝: i ≤ F.W

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) ms'

m.last ≤ F.Wcases 
ms': MeasureSet
ms'
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

m✝: Meas

h: Resolve F ih c c (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.tainted m✝)

tainted
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

set
m.last ≤ F.W 
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

ms': MeasureSet

h: Resolve F ih c c ms'

h_ok✝: i ≤ F.W

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) ms'

m.last ≤ F.Wcase tainted => 
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

m✝: Meas

h: Resolve F ih c c (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.tainted m✝)

m.last ≤ F.Wsimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.tainted m✝)
h_meas
Goals accomplished! 🐙
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

ms': MeasureSet

h: Resolve F ih c c ms'

h_ok✝: i ≤ F.W

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) ms'

m.last ≤ F.Wcase set => 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: ms = List.map (Meas.adjust_align i) ms✝

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsubst 
h_meas: ms = List.map (Meas.adjust_align i) ms✝
h_meas
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

h_in: m ∈ List.map (Meas.adjust_align i) ms✝

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp at 
h_in: m ∈ List.map (Meas.adjust_align i) ms✝
h_in
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = m

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wlet ⟨
m': Meas
m', 
h_left: m' ∈ ms✝
h_left, 
h_right: Meas.adjust_align i m' = m
h_right⟩ := 
h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = m
h_in
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = m

m': Meas

h_left: m' ∈ ms✝

h_right: Meas.adjust_align i m' = m

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Whave 
ih: ?m.17991
ih := 
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
Resolve_last 
h: Resolve F ih c c (MeasureSet.set ms✝ h✝)
h 
h_left: m' ∈ ms✝
h_left
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih✝: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = m

m': Meas

h_left: m' ∈ ms✝

h_right: Meas.adjust_align i m' = m

ih: m'.last ≤ F.W

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [
Meas.adjust_align: {α : Type} → ℕ → Meas → Meas
Meas.adjust_align] at 
h_right: Meas.adjust_align i m' = m
h_right
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih✝: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = m

m': Meas

h_left: m' ∈ ms✝

h_right: { last := m'.last, cost := m'.cost, doc := Doc.align m'.doc, x := m'.x, y := max i m'.y } = m

ih: m'.last ≤ F.W

m.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wcases 
m: Meas
m
α✝: Type

F: Factory α✝

c, i: ℕ

ih✝: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

m': Meas

h_left: m' ∈ ms✝

ih: m'.last ≤ F.W

last✝: ℕ

cost✝: α✝

doc✝: Doc

x✝, y✝: ℕ

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

h_right: { last := m'.last, cost := m'.cost, doc := Doc.align m'.doc, x := m'.x, y := max i m'.y } =   { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

mk
{ last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp at 
h_right: { last := m'.last, cost := m'.cost, doc := Doc.align m'.doc, x := m'.x, y := max i m'.y } =   { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }
h_right ⊢
α✝: Type

F: Factory α✝

c, i: ℕ

ih✝: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

m': Meas

h_left: m' ∈ ms✝

ih: m'.last ≤ F.W

last✝: ℕ

cost✝: α✝

doc✝: Doc

x✝, y✝: ℕ

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

h_right: m'.last = last✝ ∧ m'.cost = cost✝ ∧ Doc.align m'.doc = doc✝ ∧ m'.x = x✝ ∧ max i m'.y = y✝

mk
last✝ ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wsimp [← 
h_right: m'.last = last✝ ∧ m'.cost = cost✝ ∧ Doc.align m'.doc = doc✝ ∧ m'.x = x✝ ∧ max i m'.y = y✝
h_right.
left: ∀ {a b : Prop}, a ∧ b → a
left]
α✝: Type

F: Factory α✝

c, i: ℕ

ih✝: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih✝ c c (MeasureSet.set ms✝ h✝)

h_not_empty: List.map (Meas.adjust_align i) ms✝ ≠ []

m': Meas

h_left: m' ∈ ms✝

ih: m'.last ≤ F.W

last✝: ℕ

cost✝: α✝

doc✝: Doc

x✝, y✝: ℕ

h_in: ∃ a, a ∈ ms✝ ∧ Meas.adjust_align i a = { last := last✝, cost := cost✝, doc := doc✝, x := x✝, y := y✝ }

h_right: m'.last = last✝ ∧ m'.cost = cost✝ ∧ Doc.align m'.doc = doc✝ ∧ m'.x = x✝ ∧ max i m'.y = y✝

mk
m'.last ≤ F.W
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

m.last ≤ F.Wassumption
Goals accomplished! 🐙
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h: Resolve F (Doc.align ih) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase align_taint 
ms: MeasureSet
ms 
h: Resolve F ih c c ms
h _ => 
        
α✝: Type

ms✝: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms✝ ≠ []

h_in: m ∈ ms✝

ih: Doc

ms: MeasureSet

h: Resolve F ih c c ms

h_bad✝: i > F.W

h_meas: MeasureSet.set ms✝ h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms)

m.last ≤ F.Wcases 
ms: MeasureSet
ms
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_bad✝: i > F.W

m✝: Meas

h: Resolve F ih c c (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.tainted m✝))

tainted
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_bad✝: i > F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms✝ h✝))

set
m.last ≤ F.W 
        
α✝: Type

ms✝: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms✝ ≠ []

h_in: m ∈ ms✝

ih: Doc

ms: MeasureSet

h: Resolve F ih c c ms

h_bad✝: i > F.W

h_meas: MeasureSet.set ms✝ h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms)

m.last ≤ F.Wcase set | tainted => 
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih: Doc

h_bad✝: i > F.W

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F ih c c (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms✝ h✝))

m.last ≤ F.Wsimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift, 
MeasureSet.taint: {α : Type} → MeasureSet → MeasureSet
MeasureSet.taint] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms✝ h✝))
h_meas
Goals accomplished! 🐙
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase choice 
ih₁: Doc
ih₁ 
ih₂: Doc
ih₂ => 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

h: Resolve F (Doc.choice ih₁ ih₂) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wgeneralize h_meas : 
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: List Meas
ms 
h_not_empty: ms ≠ []
h_not_empty = ml at 
h: Resolve F (Doc.choice ih₁ ih₂) c i (MeasureSet.set ms h_not_empty)
h
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ml: MeasureSet

h_meas: MeasureSet.set ms h_not_empty = ml

h: Resolve F (Doc.choice ih₁ ih₂) c i ml

m.last ≤ F.W
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

h: Resolve F (Doc.choice ih₁ ih₂) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcases 
h: Resolve F (Doc.choice ih₁ ih₂) c i ml
h
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝, ms'✝: MeasureSet

h_left✝: Resolve F ih₁ c i ms✝

h_right✝: Resolve F ih₂ c i ms'✝

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms✝ ms'✝

choice
m.last ≤ F.W
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

h: Resolve F (Doc.choice ih₁ ih₂) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase choice 
ms'': MeasureSet
ms'' 
ms': MeasureSet
ms' 
h_left: Resolve F ih₁ c i ms''
h_left 
h_right: Resolve F ih₂ c i ms'
h_right => 
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'', ms': MeasureSet

h_left: Resolve F ih₁ c i ms''

h_right: Resolve F ih₂ c i ms'

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' ms'

m.last ≤ F.Wcases 
ms': MeasureSet
ms'
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

m✝: Meas

h_right: Resolve F ih₂ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

tainted
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

ms✝: List Meas

h✝: ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h✝)

set
m.last ≤ F.W 
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'', ms': MeasureSet

h_left: Resolve F ih₁ c i ms''

h_right: Resolve F ih₂ c i ms'

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' ms'

m.last ≤ F.Wcase tainted => 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

m✝: Meas

h_right: Resolve F ih₂ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

m.last ≤ F.Wsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

m✝: Meas

h_right: Resolve F ih₂ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = ms''

m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

m✝: Meas

h_right: Resolve F ih₂ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

m.last ≤ F.Wsubst 
h_meas: MeasureSet.set ms h_not_empty = ms''
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

m✝: Meas

h_right: Resolve F ih₂ c i (MeasureSet.tainted m✝)

h_left: Resolve F ih₁ c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

m✝: Meas

h_right: Resolve F ih₂ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.tainted m✝)

m.last ≤ F.Wexact 
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
Resolve_last 
h_left: Resolve F ih₁ c i (MeasureSet.set ms h_not_empty)
h_left 
h_in: m ∈ ms
h_in
Goals accomplished! 🐙
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'', ms': MeasureSet

h_left: Resolve F ih₁ c i ms''

h_right: Resolve F ih₂ c i ms'

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' ms'

m.last ≤ F.Wcase set 
h_not_empty': ms✝ ≠ []
h_not_empty' => 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h_not_empty')

m.last ≤ F.Wcases 
ms'': MeasureSet
ms''
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

m✝: Meas

h_left: Resolve F ih₁ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h_not_empty')

tainted
m.last ≤ F.W
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

set
m.last ≤ F.W 
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h_not_empty')

m.last ≤ F.Wcase tainted => 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

m✝: Meas

h_left: Resolve F ih₁ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h_not_empty')

m.last ≤ F.Wsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h_not_empty')
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

m✝: Meas

h_left: Resolve F ih₁ c i (MeasureSet.tainted m✝)

h_meas: ms = ms✝

m.last ≤ F.W 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

m✝: Meas

h_left: Resolve F ih₁ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h_not_empty')

m.last ≤ F.Wsubst 
h_meas: ms = ms✝
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

m✝: Meas

h_left: Resolve F ih₁ c i (MeasureSet.tainted m✝)

h_not_empty': ms ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms h_not_empty')

m.last ≤ F.W 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

m✝: Meas

h_left: Resolve F ih₁ c i (MeasureSet.tainted m✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h_not_empty')

m.last ≤ F.Wexact 
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
Resolve_last 
h_right: Resolve F ih₂ c i (MeasureSet.set ms h_not_empty')
h_right 
h_in: m ∈ ms
h_in
Goals accomplished! 🐙
          
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms'': MeasureSet

h_left: Resolve F ih₁ c i ms''

ms✝: List Meas

h_not_empty': ms✝ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝ h_not_empty')

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F ms'' (MeasureSet.set ms✝ h_not_empty')

m.last ≤ F.Wcase set => 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

m.last ≤ F.Wsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')
h_meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: ms = merge F (ms✝, ms✝¹)

m.last ≤ F.W 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

m.last ≤ F.Wsubst 
h_meas: ms = merge F (ms✝, ms✝¹)
h_meas
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

m.last ≤ F.W 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

m.last ≤ F.Whave := 
merge_pareto_subset: ∀ {α : Type} {m : Meas} {F : Factory α} {ms₁ ms₂ : List Meas},
  m ∈ merge F (ms₁, ms₂) → pareto F ms₁ → pareto F ms₂ → m ∈ ms₁ ∨ m ∈ ms₂
merge_pareto_subset 
h_in: m ∈ merge F (ms✝, ms✝¹)
h_in (
Resolve_pareto: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : List Meas} {h_non_empty : ms ≠ []},
  Resolve F d c i (MeasureSet.set ms h_non_empty) → pareto F ms
Resolve_pareto 
h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)
h_left) (
Resolve_pareto: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : List Meas} {h_non_empty : ms ≠ []},
  Resolve F d c i (MeasureSet.set ms h_non_empty) → pareto F ms
Resolve_pareto 
h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')
h_right)
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

this: m ∈ ms✝ ∨ m ∈ ms✝¹

m.last ≤ F.W
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

m.last ≤ F.Wcases 
this: ?m.23478
this
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝¹: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝¹)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h✝: m ∈ ms✝

inl
m.last ≤ F.W
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝¹: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝¹)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h✝: m ∈ ms✝¹

inr
m.last ≤ F.W
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

m.last ≤ F.Wcase inl 
h_in': ?m.23534
h_in' => 
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝

m.last ≤ F.Wexact 
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
Resolve_last 
h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)
h_left 
h_in': ?m.23534
h_in'
Goals accomplished! 🐙 
            
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_meas: MeasureSet.set ms h_not_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h_not_empty')

m.last ≤ F.Wcase inr 
h_in': ?m.23535
h_in' => 
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

ih₁, ih₂: Doc

ms✝¹: List Meas

h_not_empty': ms✝¹ ≠ []

h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')

ms✝: List Meas

h✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h✝)

h_not_empty: merge F (ms✝, ms✝¹) ≠ []

h_in: m ∈ merge F (ms✝, ms✝¹)

h_in': m ∈ ms✝¹

m.last ≤ F.Wexact 
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
Resolve_last 
h_right: Resolve F ih₂ c i (MeasureSet.set ms✝¹ h_not_empty')
h_right 
h_in': ?m.23535
h_in'
Goals accomplished! 🐙 
    
α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h: Resolve F d c i (MeasureSet.set ms h_not_empty)

h_in: m ∈ ms

m.last ≤ F.Wcase concat 
ih₁: Doc
ih₁ _ => 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

h: Resolve F (Doc.concat ih₁ d₂✝) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcases 
h: Resolve F (Doc.concat ih₁ d₂✝) c i (MeasureSet.set ms h_not_empty)
h
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left✝: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h✝: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

concat_set
m.last ≤ F.W 
      
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

h: Resolve F (Doc.concat ih₁ d₂✝) c i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wcase concat_set 
h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left 
h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)
h_right =>
        
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wdwi { 
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

m.last ≤ F.Wapply 
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
ResolveConcat_last
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

h
ResolveConcat F ?ms_in ?d ?i (MeasureSet.set ?ms ?h_not_empty)
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

h_in
m ∈ ?ms
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

ms
List Meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

ms_in
List Meas
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

d
Doc
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

i
ℕ
α✝: Type

ms: List Meas

F: Factory α✝

c, i: ℕ

m: Meas

h_not_empty: ms ≠ []

h_in: m ∈ ms

ih₁, d₂✝: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

h_left: Resolve F ih₁ c i (MeasureSet.set ms✝ h_non_empty✝)

h_right: ResolveConcat F ms✝ d₂✝ i (MeasureSet.set ms h_not_empty)

h_not_empty
?ms ≠ [] }
Goals accomplished! 🐙
end
termination_by 
  ResolveConcatOne_last => (
d: Doc
d.
size: Doc → ℕ
size, 
1: ?m.35150
1, 
0: ?m.35161
0)
  ResolveConcat_last => (
d: Doc
d.
size: Doc → ℕ
size, 
2: ?m.35592
2, 
ms_in: List Meas
ms_in.
length: {α : Type ?u.35597} → List α → ℕ
length)
  Resolve_last => (
d: Doc
d.
size: Doc → ℕ
size, 
0: ?m.35396
0, 
0: ?m.35407
0)