import Pretty.Supports.Merge
import Pretty.Supports.DocSize
import Pretty.Defs.Resolve

mutual
  lemma 
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_print: ResolveConcatOne F d m i (MeasureSet.set msr h_non_empty)
h_print : 
ResolveConcatOne: {α : Type} → Factory α → Doc → Meas → ℕ → MeasureSet → Prop
ResolveConcatOne 
F: ?m.4
F 
d: ?m.11
d 
m: ?m.17
m 
i: ?m.24
i (
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
msr: ?m.33
msr 
h_non_empty: ?m.42
h_non_empty)) : 
      
pareto: {α : Type} → Factory α → List Meas → Prop
pareto 
F: ?m.4
F 
msr: ?m.33
msr := by
Goals accomplished! 🐙 
    
α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

h_print: ResolveConcatOne F d m i (MeasureSet.set msr h_non_empty)

pareto F msrcases 
h_print: ResolveConcatOne F d m i (MeasureSet.set msr h_non_empty)
h_print
α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

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

set
pareto F (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))
    
α✝: Type

F: Factory α✝

d: Doc

m: Meas

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

h_print: ResolveConcatOne F d m i (MeasureSet.set msr h_non_empty)

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

F: Factory α✝

d: Doc

m: Meas

i: ℕ

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

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

pareto F (dedup F (List.map (fun m' => Meas.concat F m m') ms✝))exact 
pareto_concat: ∀ {α : Type} {F : Factory α} {ms : List Meas} (m : Meas),
  pareto F ms → pareto F (dedup F (List.map (fun m' => Meas.concat F m m') ms))
pareto_concat 
_: Meas
_ (
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: Resolve F d m.last i (MeasureSet.set ms✝ h_non_empty✝)
h)
Goals accomplished! 🐙

  lemma 
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_print: ResolveConcat F ms d i (MeasureSet.set msr h_non_empty)
h_print : 
ResolveConcat: {α : Type} → Factory α → List Meas → Doc → ℕ → MeasureSet → Prop
ResolveConcat 
F: ?m.59
F 
ms: ?m.66
ms 
d: ?m.73
d 
i: ?m.79
i (
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
msr: ?m.88
msr 
h_non_empty: ?m.96
h_non_empty)) : 
      
pareto: {α : Type} → Factory α → List Meas → Prop
pareto 
F: ?m.59
F 
msr: ?m.88
msr := by
Goals accomplished! 🐙
    
    
α✝: Type

F: Factory α✝

ms: List Meas

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

h_print: ResolveConcat F ms d i (MeasureSet.set msr h_non_empty)

pareto F msrgeneralize h_gen : 
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
_: List Meas
_ 
_: ?m.536 ≠ []
_ = ms at 
h_print: ResolveConcat F ms d i (MeasureSet.set msr h_non_empty)
h_print
α✝: Type

F: Factory α✝

ms✝: List Meas

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms: MeasureSet

h_gen: MeasureSet.set msr h_non_empty = ms

h_print: ResolveConcat F ms✝ d i ms

pareto F msr
    
α✝: Type

F: Factory α✝

ms: List Meas

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

h_print: ResolveConcat F ms d i (MeasureSet.set msr h_non_empty)

pareto F msrcases 
h_print: ResolveConcat F ms✝ d i ms
h_print
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms: MeasureSet

h_gen: MeasureSet.set msr h_non_empty = ms

m✝: Meas

h_current✝: ResolveConcatOne F d m✝ i ms

one
pareto F msr
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr'✝ msr✝

cons
pareto F msr 
    
α✝: Type

F: Factory α✝

ms: List Meas

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

h_print: ResolveConcat F ms d i (MeasureSet.set msr h_non_empty)

pareto F msrcase one 
h_print: ResolveConcatOne F d m✝ i ms
h_print => 
      
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms: MeasureSet

h_gen: MeasureSet.set msr h_non_empty = ms

m✝: Meas

h_print: ResolveConcatOne F d m✝ i ms

pareto F msrsubst 
h_gen: MeasureSet.set msr h_non_empty = ms
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

m✝: Meas

h_print: ResolveConcatOne F d m✝ i (MeasureSet.set msr h_non_empty)

pareto F msr
      
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms: MeasureSet

h_gen: MeasureSet.set msr h_non_empty = ms

m✝: Meas

h_print: ResolveConcatOne F d m✝ i ms

pareto F msrexact 
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_print: ResolveConcatOne F d m✝ i (MeasureSet.set msr h_non_empty)
h_print
Goals accomplished! 🐙 
    
α✝: Type

F: Factory α✝

ms: List Meas

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

h_print: ResolveConcat F ms d i (MeasureSet.set msr h_non_empty)

pareto F msrcase cons 
msr_left: MeasureSet
msr_left _ 
msr_right: MeasureSet
msr_right 
h_rest: ResolveConcat F ms✝ d i msr_left
h_rest 
h_print: ResolveConcatOne F d m✝ i msr_right
h_print => 
      
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

msr_left: MeasureSet

m✝: Meas

msr_right: MeasureSet

h_rest: ResolveConcat F ms✝ d i msr_left

h_print: ResolveConcatOne F d m✝ i msr_right

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right msr_left

pareto F msrcases 
msr_left: MeasureSet
msr_left
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝¹: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝¹ i msr_right

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.tainted m✝)

tainted
pareto F msr
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝ i msr_right

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.set ms✝ h✝)

set
pareto F msr 
      
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

msr_left: MeasureSet

m✝: Meas

msr_right: MeasureSet

h_rest: ResolveConcat F ms✝ d i msr_left

h_print: ResolveConcatOne F d m✝ i msr_right

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right msr_left

pareto F msrcase tainted => 
        
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝¹: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝¹ i msr_right

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.tainted m✝)

pareto F msrcases 
msr_right: MeasureSet
msr_right
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝², m✝¹: Meas

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

m✝: Meas

h_print: ResolveConcatOne F d m✝² i (MeasureSet.tainted m✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.tainted m✝¹)

tainted
pareto F msr
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹, m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

set
pareto F msr 
        
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝¹: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝¹ i msr_right

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.tainted m✝)

pareto F msrcase tainted => 
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝², m✝¹: Meas

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

m✝: Meas

h_print: ResolveConcatOne F d m✝² i (MeasureSet.tainted m✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.tainted m✝¹)

pareto F msrsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.tainted m✝¹)
h_gen
Goals accomplished! 🐙
        
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝¹: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝¹ i msr_right

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.tainted m✝)

pareto F msrcase set => 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹, m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

pareto F msrsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹, m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: msr = ms✝

pareto F msr  
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹, m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

pareto F msrsubst 
h_gen: msr = ms✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝¹, m✝: Meas

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

h✝: msr ≠ []

h_print: ResolveConcatOne F d m✝¹ i (MeasureSet.set msr h✝)

pareto F msr 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹, m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

pareto F msrexact 
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_print: ResolveConcatOne F d m✝¹ i (MeasureSet.set msr h✝)
h_print
Goals accomplished! 🐙 
      
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

msr_left: MeasureSet

m✝: Meas

msr_right: MeasureSet

h_rest: ResolveConcat F ms✝ d i msr_left

h_print: ResolveConcatOne F d m✝ i msr_right

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right msr_left

pareto F msrcase set => 
        
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝ i msr_right

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.set ms✝ h✝)

pareto F msrcases 
msr_right: MeasureSet
msr_right
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

tainted
pareto F msr
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

set
pareto F msr 
        
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝ i msr_right

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.set ms✝ h✝)

pareto F msrcase tainted => 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

pareto F msrsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: msr = ms✝

pareto F msr  
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

pareto F msrsubst 
h_gen: msr = ms✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝: List Meas

m✝¹, m✝: Meas

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

h✝: msr ≠ []

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

pareto F msr
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝¹: Meas

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

pareto F msrexact 
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 msr h✝)
h_rest
Goals accomplished! 🐙
        
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

ms✝¹: List Meas

m✝: Meas

msr_right: MeasureSet

h_print: ResolveConcatOne F d m✝ i msr_right

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F msr_right (MeasureSet.set ms✝ h✝)

pareto F msrcase set => 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

pareto F msrsimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: msr = merge F (ms✝, ms✝¹)

pareto F msr  
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

pareto F msrsubst 
h_gen: msr = merge F (ms✝, ms✝¹)
h_gen
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

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

pareto F (merge F (ms✝, ms✝¹)) 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

pareto F msrapply 
merge_preserves_pareto: ∀ {α : Type} {F : Factory α} {ms₁ ms₂ : List Meas}, pareto F ms₁ → pareto F ms₂ → pareto F (merge F (ms₁, ms₂))
merge_preserves_pareto
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

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

h_pareto₁
pareto F ms✝
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

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

h_pareto₂
pareto F ms✝¹ 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

pareto F msrcase h_pareto₁ => 
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

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

pareto F ms✝exact 
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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)
h_print
Goals accomplished! 🐙 
          
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

msr: List Meas

h_non_empty: msr ≠ []

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

h_gen: MeasureSet.set msr h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.set ms✝¹ h✝¹)

pareto F msrcase h_pareto₂ => 
α✝: Type

F: Factory α✝

d: Doc

i: ℕ

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_print: ResolveConcatOne F d m✝ i (MeasureSet.set ms✝ h✝)

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

pareto F ms✝¹exact 
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
Goals accomplished! 🐙

  theorem 
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_print: Resolve F d c i (MeasureSet.set ms h_non_empty)
h_print : 
Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve 
F: ?m.113
F 
d: ?m.120
d 
c: ?m.126
c 
i: ?m.132
i (
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
ms: ?m.141
ms 
h_non_empty: ?m.150
h_non_empty)) : 
      
pareto: {α : Type} → Factory α → List Meas → Prop
pareto 
F: ?m.113
F 
ms: ?m.141
ms := by
Goals accomplished! 🐙 
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

h_print: Resolve F d c i (MeasureSet.set ms h_non_empty)

pareto F msgeneralize h_gen : 
MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set 
_: List Meas
_ 
_: ?m.1480 ≠ []
_ = ms at 
h_print: Resolve F d c i (MeasureSet.set ms h_non_empty)
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

h_print: Resolve F d c i (MeasureSet.set ms h_non_empty)

pareto F msmatch 
d: Doc
d with
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝| 
Doc.text: String → Doc
Doc.text _ =>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

s✝: String

h_print: Resolve F (Doc.text s✝) c i ms

pareto F ms✝ 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝subst 
h_gen: MeasureSet.set ms✝ h_non_empty = ms
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

s✝: String

h_print: Resolve F (Doc.text s✝) c i (MeasureSet.set ms h_non_empty)

pareto F ms
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

s✝: String

h_print: Resolve F (Doc.text s✝) c i ms

pareto F ms✝cases 
h_print: Resolve F (Doc.text s✝) c i (MeasureSet.set ms h_non_empty)
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

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_non_empty: [m✝] ≠ []

text_set
pareto F [m✝] 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

s✝: String

h_print: Resolve F (Doc.text s✝) c i ms

pareto F ms✝case text_set => 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

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_non_empty: [m✝] ≠ []

pareto F [m✝]apply 
pareto_one: ∀ {α : Type} {F : Factory α} (m : Meas), pareto F [m]
pareto_one
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝| 
Doc.nl: Doc
Doc.nl =>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F Doc.nl c i ms

pareto F ms✝ 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝subst 
h_gen: MeasureSet.set ms✝ h_non_empty = ms
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

h_print: Resolve F Doc.nl c i (MeasureSet.set ms h_non_empty)

pareto F ms
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F Doc.nl c i ms

pareto F ms✝cases 
h_print: Resolve F Doc.nl c i (MeasureSet.set ms h_non_empty)
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

h_non_empty: [m✝] ≠ []

line_set
pareto F [m✝]
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F Doc.nl c i ms

pareto F ms✝case line_set => 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

h_non_empty: [m✝] ≠ []

pareto F [m✝]apply 
pareto_one: ∀ {α : Type} {F : Factory α} (m : Meas), pareto F [m]
pareto_one
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝| 
Doc.nest: ℕ → Doc → Doc
Doc.nest 
n: ℕ
n 
d': Doc
d' =>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

n: ℕ

d': Doc

h_print: Resolve F (Doc.nest n d') c i ms

pareto F ms✝
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝dwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

n: ℕ

d': Doc

h_print: Resolve F (Doc.nest n d') c i ms

pareto F ms✝cases 
h_print: Resolve F (Doc.nest n d') c i ms
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: MeasureSet

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) ms✝

nest
pareto F ms }
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: MeasureSet

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) ms✝

nest
pareto F ms 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

n: ℕ

d': Doc

h_print: Resolve F (Doc.nest n d') c i ms

pareto F ms✝case nest 
ms': MeasureSet
ms' 
h': Resolve F d' c (i + n) ms'
h' => 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms': MeasureSet

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) ms'

pareto F msdwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms': MeasureSet

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) ms'

pareto F mscases 
ms': MeasureSet
ms'
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.tainted m✝)

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)

set
pareto F ms }
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)

set
pareto F ms 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms': MeasureSet

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) ms'

pareto F mscase set => 
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)

pareto F mssimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift] at 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

pareto F ms
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)

pareto F mssubst 
h_gen: ms = List.map (Meas.adjust_nest n) ms✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

pareto F (List.map (Meas.adjust_nest n) ms✝)
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)

pareto F msapply 
pareto_map_lift_nest: ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.map (Meas.adjust_nest n) ms)
pareto_map_lift_nest
α✝: Type

F: Factory α✝

d: Doc

c, i, n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

h
pareto F ms✝
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

n: ℕ

d': Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_nest n) (MeasureSet.set ms✝ h✝)

pareto F msexact 
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': Resolve F d' c (i + n) (MeasureSet.set ms✝ h✝)
h'
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝| 
Doc.align: Doc → Doc
Doc.align 
d': Doc
d' =>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d': Doc

h_print: Resolve F (Doc.align d') c i ms

pareto F ms✝
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝cases 
h_print: Resolve F (Doc.align d') c i ms
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_bad✝: i > F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝)

align_taint
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms✝: MeasureSet

h✝: Resolve F d' c c ms✝

h_ok✝: i ≤ F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) ms✝

align
pareto F ms 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d': Doc

h_print: Resolve F (Doc.align d') c i ms

pareto F ms✝case align 
ms': MeasureSet
ms' 
h': Resolve F d' c c ms'
h' _ => 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms': MeasureSet

h': Resolve F d' c c ms'

h_ok✝: i ≤ F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) ms'

pareto F msdwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms': MeasureSet

h': Resolve F d' c c ms'

h_ok✝: i ≤ F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) ms'

pareto F mscases 
ms': MeasureSet
ms'
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.tainted m✝)

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

set
pareto F ms }
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

set
pareto F ms 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms': MeasureSet

h': Resolve F d' c c ms'

h_ok✝: i ≤ F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) ms'

pareto F mscase set => 
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

pareto F mssimp [
MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift] at 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

pareto F ms
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

pareto F mssubst 
h_gen: ms = List.map (Meas.adjust_align i) ms✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

pareto F (List.map (Meas.adjust_align i) ms✝)
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

pareto F msapply 
pareto_map_lift_align: ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.map (Meas.adjust_align n) ms)
pareto_map_lift_align
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

h
pareto F ms✝
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_ok✝: i ≤ F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.set ms✝ h✝)

pareto F msexact 
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': Resolve F d' c c (MeasureSet.set ms✝ h✝)
h'
Goals accomplished! 🐙
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d': Doc

h_print: Resolve F (Doc.align d') c i ms

pareto F ms✝case align_taint 
ms': MeasureSet
ms' _ _ => 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms': MeasureSet

h✝: Resolve F d' c c ms'

h_bad✝: i > F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms')

pareto F msdwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

ms': MeasureSet

h✝: Resolve F d' c c ms'

h_bad✝: i > F.W

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms')

pareto F mscases 
ms': MeasureSet
ms'
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_bad✝: i > F.W

m✝: Meas

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

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

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d': Doc

h_bad✝: i > F.W

ms✝: List Meas

h✝¹: ms✝ ≠ []

h✝: Resolve F d' c c (MeasureSet.set ms✝ h✝¹)

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms✝ h✝¹))

set
pareto F ms }
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝| 
Doc.choice: Doc → Doc → Doc
Doc.choice 
d₁: Doc
d₁ 
d₂: Doc
d₂ =>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d₁, d₂: Doc

h_print: Resolve F (Doc.choice d₁ d₂) c i ms

pareto F ms✝ 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝dwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d₁, d₂: Doc

h_print: Resolve F (Doc.choice d₁ d₂) c i ms

pareto F ms✝cases 
h_print: Resolve F (Doc.choice d₁ d₂) c i ms
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝, ms'✝: MeasureSet

h_left✝: Resolve F d₁ c i ms✝

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F ms✝ ms'✝

choice
pareto F ms }
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝, ms'✝: MeasureSet

h_left✝: Resolve F d₁ c i ms✝

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F ms✝ ms'✝

choice
pareto F ms 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d₁, d₂: Doc

h_print: Resolve F (Doc.choice d₁ d₂) c i ms

pareto F ms✝case choice 
ms: MeasureSet
ms 
ms': MeasureSet
ms' 
h_left: Resolve F d₁ c i ms
h_left 
h_right: Resolve F d₂ c i ms'
h_right => 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

d₁, d₂: Doc

ms, ms': MeasureSet

h_left: Resolve F d₁ c i ms

h_right: Resolve F d₂ c i ms'

h_gen: MeasureSet.set ms✝ h_non_empty = MeasureSet.union F ms ms'

pareto F ms✝cases 
ms: MeasureSet
ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) ms'

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) ms'

set
pareto F ms 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

d₁, d₂: Doc

ms, ms': MeasureSet

h_left: Resolve F d₁ c i ms

h_right: Resolve F d₂ c i ms'

h_gen: MeasureSet.set ms✝ h_non_empty = MeasureSet.union F ms ms'

pareto F ms✝case tainted => 
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) ms'

pareto F mscases 
ms': MeasureSet
ms'
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝¹: Meas

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

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝¹) (MeasureSet.tainted m✝)

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

set
pareto F ms
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) ms'

pareto F mscase tainted => 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝¹: Meas

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

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝¹) (MeasureSet.tainted m✝)

pareto F mssimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝¹) (MeasureSet.tainted m✝)
h_gen
Goals accomplished! 🐙 
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) ms'

pareto F mscase set => 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

pareto F mssimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: ms = ms✝

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

pareto F mssubst 
h_gen: ms = ms✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

h✝: ms ≠ []

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

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.tainted m✝) (MeasureSet.set ms✝ h✝)

pareto F msexact 
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 d₂ c i (MeasureSet.set ms h✝)
h_right
Goals accomplished! 🐙
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

d₁, d₂: Doc

ms, ms': MeasureSet

h_left: Resolve F d₁ c i ms

h_right: Resolve F d₂ c i ms'

h_gen: MeasureSet.set ms✝ h_non_empty = MeasureSet.union F ms ms'

pareto F ms✝case set => 
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) ms'

pareto F mscases 
ms': MeasureSet
ms'
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)

set
pareto F ms
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) ms'

pareto F mscase tainted => 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

pareto F mssimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: ms = ms✝

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

pareto F mssubst 
h_gen: ms = ms✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

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

h✝: ms ≠ []

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

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

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

m✝: Meas

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) (MeasureSet.tainted m✝)

pareto F msexact 
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 d₁ c i (MeasureSet.set ms h✝)
h_left
Goals accomplished! 🐙
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms': MeasureSet

h_right: Resolve F d₂ c i ms'

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝ h✝) ms'

pareto F mscase set => 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)

pareto F mssimp [
MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union] at 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)

pareto F mshave := 
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 d₁ c i (MeasureSet.set ms✝¹ h✝¹)
h_left
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

this: pareto F ms✝¹

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)

pareto F mshave := 
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 d₂ c i (MeasureSet.set ms✝ h✝)
h_right
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

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

this✝: pareto F ms✝¹

this: pareto F ms✝

pareto F ms 
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)

pareto F mssubst 
h_gen: ms = merge F (ms✝¹, ms✝)
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

pareto F (merge F (ms✝¹, ms✝))
            
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.union F (MeasureSet.set ms✝¹ h✝¹) (MeasureSet.set ms✝ h✝)

pareto F msapply 
merge_preserves_pareto: ∀ {α : Type} {F : Factory α} {ms₁ ms₂ : List Meas}, pareto F ms₁ → pareto F ms₂ → pareto F (merge F (ms₁, ms₂))
merge_preserves_pareto
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

h_pareto₁
pareto F ms✝¹
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

h_pareto₂
pareto F ms✝ 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

pareto F (merge F (ms✝¹, ms✝))<;>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

h_pareto₁
pareto F ms✝¹
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

h_pareto₂
pareto F ms✝ 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝¹: List Meas

h✝¹: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

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

this✝: pareto F ms✝¹

this: pareto F ms✝

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

pareto F (merge F (ms✝¹, ms✝))assumption
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝| 
Doc.concat: Doc → Doc → Doc
Doc.concat 
d₁: Doc
d₁ 
d₂: Doc
d₂ =>
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d₁, d₂: Doc

h_print: Resolve F (Doc.concat d₁ d₂) c i ms

pareto F ms✝ 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

h_print: Resolve F d c i ms

pareto F ms✝dwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d₁, d₂: Doc

h_print: Resolve F (Doc.concat d₁ d₂) c i ms

pareto F ms✝cases 
h_print: Resolve F (Doc.concat d₁ d₂) c i ms
h_print
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

m✝: Meas

ms'✝: MeasureSet

m'✝: Meas

h_taint✝: MeasureSet.taint ms'✝ = MeasureSet.tainted m'✝

h_right✝: Resolve F d₂ m✝.last i ms'✝

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

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.tainted (Meas.concat F m✝ m'✝)

concat_taint
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝¹: List Meas

h_non_empty: ms✝¹ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝¹ h_non_empty = ms

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

h✝: ResolveConcat F ms✝ d₂ i ms

concat_set
pareto F ms✝¹ }
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝¹: List Meas

h_non_empty: ms✝¹ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝¹ h_non_empty = ms

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

h✝: ResolveConcat F ms✝ d₂ i ms

concat_set
pareto F ms✝¹ 
      
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝: List Meas

h_non_empty: ms✝ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝ h_non_empty = ms

d₁, d₂: Doc

h_print: Resolve F (Doc.concat d₁ d₂) c i ms

pareto F ms✝case concat_set 
h_left: Resolve F d₁ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left 
h_print: ResolveConcat F ms✝ d₂ i ms
h_print => 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝¹: List Meas

h_non_empty: ms✝¹ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝¹ h_non_empty = ms

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

h_print: ResolveConcat F ms✝ d₂ i ms

pareto F ms✝¹dwi { 
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝¹: List Meas

h_non_empty: ms✝¹ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝¹ h_non_empty = ms

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

h_print: ResolveConcat F ms✝ d₂ i ms

pareto F ms✝¹cases 
ms: MeasureSet
ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

m✝: Meas

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.tainted m✝

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

tainted
pareto F ms
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.set ms✝ h✝

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

set
pareto F ms }
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.set ms✝ h✝

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

set
pareto F ms 
        
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms✝¹: List Meas

h_non_empty: ms✝¹ ≠ []

ms: MeasureSet

h_gen: MeasureSet.set ms✝¹ h_non_empty = ms

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

h_print: ResolveConcat F ms✝ d₂ i ms

pareto F ms✝¹case set => 
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.set ms✝ h✝

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

pareto F mscases 
h_gen: MeasureSet.set ms h_non_empty = MeasureSet.set ms✝ h✝
h_gen
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝: List Meas

h_non_empty✝: ms✝ ≠ []

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

h✝: ms ≠ []

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

refl
pareto F ms
          
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: List Meas

h_non_empty: ms ≠ []

d₁, d₂: Doc

ms✝¹: List Meas

h_non_empty✝: ms✝¹ ≠ []

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

ms✝: List Meas

h✝: ms✝ ≠ []

h_gen: MeasureSet.set ms h_non_empty = MeasureSet.set ms✝ h✝

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

pareto F msexact 
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_print: ResolveConcat F ms✝ d₂ i (MeasureSet.set ms h✝)
h_print
Goals accomplished! 🐙 
end
termination_by 
  ResolveConcatOne_pareto => (
d: Doc
d.
size: Doc → ℕ
size, 
1: ?m.28571
1, 
0: ?m.28582
0)
  ResolveConcat_pareto => (
d: Doc
d.
size: Doc → ℕ
size, 
2: ?m.28937
2, 
ms: List Meas
ms.
length: {α : Type ?u.28942} → List α → ℕ
length)
  Resolve_pareto => (
d: Doc
d.
size: Doc → ℕ
size, 
0: ?m.28779
0, 
0: ?m.28790
0)