import Pretty.Defs.Resolve
import Pretty.Claims.MeasRender
import Pretty.Supports.ResolvePareto

theorem Resolve_optimal_text: ∀ {α : Type} {F : Factory α} {s : String} {c i : ℕ} {ml : MeasureSet} {D : List Doc} {d_choiceless : Doc} {m : Meas},
  Resolve F (Doc.text s) c i ml →
    Widen (Doc.text s) D →
      d_choiceless ∈ D →
        MeasRender F d_choiceless c i m →
          m.y ≤ F.W →
            m.x ≤ F.W → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true
Resolve_optimal_text
      (h_print: Resolve F (Doc.text s) c i ml
h_print : Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: ?m.4
F (Doc.text: String → Doc
Doc.text s: ?m.11
s) c: ?m.17
c i: ?m.23
i ml: ?m.29
ml)
      (h_widen: Widen (Doc.text s) D
h_widen : Widen: Doc → List Doc → Prop
Widen (Doc.text: String → Doc
Doc.text s: ?m.11
s) D: ?m.38
D) (h_mem: d_choiceless ∈ D
h_mem : d_choiceless: ?m.63
d_choiceless ∈ D: ?m.38
D) 
      (h_render: MeasRender F d_choiceless c i m
h_render : MeasRender: {α : Type} → Factory α → Doc → ℕ → ℕ → Meas → Prop
MeasRender F: ?m.4
F d_choiceless: ?m.63
d_choiceless c: ?m.17
c i: ?m.23
i m: ?m.102
m)
      (h_y: m.y ≤ F.W
h_y : m: ?m.102
m.y: {α : Type} → Meas → ℕ
y ≤ F: ?m.4
F.W: {α : Type} → Factory α → ℕ
W) (h_x: m.x ≤ F.W
h_x : m: ?m.102
m.x: {α : Type} → Meas → ℕ
x ≤ F: ?m.4
F.W: {α : Type} → Factory α → ℕ
W) :
      ∃ ms: ?m.164
ms h: ?m.169
h, ml: ?m.29
ml = MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: ?m.164
ms h: ?m.169
h ∧ ∃ m_better: ?m.204
m_better, m_better: ?m.204
m_better ∈ ms: ?m.164
ms ∧ dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: ?m.4
F m_better: ?m.204
m_better m: ?m.102
m := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

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

h_widen: Widen (Doc.text s) D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_widen: Widen (Doc.text s) D
h_widenα✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

d_choiceless: Doc

m: Meas

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

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_mem: d_choiceless ∈ [Doc.text s]

text∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
  α✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

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

h_widen: Widen (Doc.text s) D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesimp at h_mem: d_choiceless ∈ [Doc.text s]
h_memα✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

d_choiceless: Doc

m: Meas

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

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_mem: d_choiceless = Doc.text s

text∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
  α✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

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

h_widen: Widen (Doc.text s) D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesubst h_mem: d_choiceless = Doc.text s
h_memα✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

m: Meas

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

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

text∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true
  α✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

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

h_widen: Widen (Doc.text s) D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_print: Resolve F (Doc.text s) c i ml
h_printα✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

h_bad✝: c + String.length s > F.W ∨ i > F.W

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

text.text_taint∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true
α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

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

h_i✝: i ≤ F.W

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

text.text_set∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
  α✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

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

h_widen: Widen (Doc.text s) D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase text_set h': MeasRender F (Doc.text s) c i m✝
h' => 
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

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

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truehave := MeasRender_deterministic: ∀ {α : Type} {d : Doc} {c i : ℕ} {F : Factory α} {m₁ m₂ : Meas}, MeasRender F d c i m₁ → MeasRender F d c i m₂ → m₁ = m₂
MeasRender_deterministic h_render: MeasRender F (Doc.text s) c i m
h_render h': MeasRender F (Doc.text s) c i m✝
h'α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

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

h_i✝: i ≤ F.W

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

this: m = m✝

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

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

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesubst this: ?m.1128
thisα✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

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

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m] (_ : ¬[m] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

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

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = trueexists [m: Meas
m], (α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

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

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m] (_ : ¬[m] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

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

h_i✝: i ≤ F.W

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

[m] ≠ []simp
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

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

h_i✝: i ≤ F.W

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

MeasureSet.set [m] (_ : ¬[m] = []) = MeasureSet.set [m] (_ : ¬[m] = []) ∧   ∃ m_better, m_better ∈ [m] ∧ dominates F m_better m = true
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

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

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesimp [dominates_refl: ∀ {α : Type} {m : Meas} (F : Factory α), dominates F m m = true
dominates_refl]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

s: String

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

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

h_widen: Widen (Doc.text s) D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase text_taint h_bad: c + String.length s > F.W ∨ i > F.W
h_bad h_render': MeasRender F (Doc.text s) c i m✝
h_render' => 
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_render: MeasRender F (Doc.text s) c i m
h_renderα✝: Type

F: Factory α✝

s: String

c, i: ℕ

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

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

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

text∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better
            { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s,
              x := c + String.length s, y := i } =           true
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesimp at h_y: { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s, x := c + String.length s,
      y := i }.y ≤   F.W
h_y h_x: { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s, x := c + String.length s,
      y := i }.x ≤   F.W
h_xα✝: Type

F: Factory α✝

s: String

c, i: ℕ

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

h_y: i ≤ F.W

h_x: c + String.length s ≤ F.W

text∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better
            { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s,
              x := c + String.length s, y := i } =           true 
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_bad: c + String.length s > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

s: String

c, i: ℕ

m✝: Meas

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

h_y: i ≤ F.W

h_x: c + String.length s ≤ F.W

h✝: c + String.length s > F.W

text.inl∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better
            { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s,
              x := c + String.length s, y := i } =           true
α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m✝: Meas

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

h_y: i ≤ F.W

h_x: c + String.length s ≤ F.W

h✝: i > F.W

text.inr∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better
            { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s,
              x := c + String.length s, y := i } =           true 
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase inl h_bad: ?m.5225
h_bad => α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m✝: Meas

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

h_y: i ≤ F.W

h_x: c + String.length s ≤ F.W

h_bad: c + String.length s > F.W

∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better
            { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s,
              x := c + String.length s, y := i } =           truelinarith
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

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

m✝: Meas

h_bad: c + String.length s > F.W ∨ i > F.W

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

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase inr h_bad: ?m.5226
h_bad => α✝: Type

F: Factory α✝

s: String

c, i: ℕ

m✝: Meas

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

h_y: i ≤ F.W

h_x: c + String.length s ≤ F.W

h_bad: i > F.W

∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better
            { last := c + String.length s, cost := Factory.text F c (String.length s), doc := Doc.text s,
              x := c + String.length s, y := i } =           truelinarith
Goals accomplished! 🐙

theorem Resolve_optimal_nl: ∀ {α : Type} {F : Factory α} {c i : ℕ} {ml : MeasureSet} {D : List Doc} {d_choiceless : Doc} {m : Meas},
  Resolve F Doc.nl c i ml →
    Widen Doc.nl D →
      d_choiceless ∈ D →
        MeasRender F d_choiceless c i m →
          m.y ≤ F.W →
            m.x ≤ F.W → ∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true
Resolve_optimal_nl
      (h_print: Resolve F Doc.nl c i ml
h_print : Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: ?m.8959
F Doc.nl: Doc
Doc.nl c: ?m.8966
c i: ?m.8972
i ml: ?m.8978
ml)
      (h_widen: Widen Doc.nl D
h_widen : Widen: Doc → List Doc → Prop
Widen Doc.nl: Doc
Doc.nl D: ?m.8987
D) (h_mem: d_choiceless ∈ D
h_mem : d_choiceless: ?m.9012
d_choiceless ∈ D: ?m.8987
D) 
      (h_render: MeasRender F d_choiceless c i m
h_render : MeasRender: {α : Type} → Factory α → Doc → ℕ → ℕ → Meas → Prop
MeasRender F: ?m.8959
F d_choiceless: ?m.9012
d_choiceless c: ?m.8966
c i: ?m.8972
i m: ?m.9051
m)
      (h_y: m.y ≤ F.W
h_y : m: ?m.9051
m.y: {α : Type} → Meas → ℕ
y ≤ F: ?m.8959
F.W: {α : Type} → Factory α → ℕ
W) (h_x: m.x ≤ F.W
h_x : m: ?m.9051
m.x: {α : Type} → Meas → ℕ
x ≤ F: ?m.8959
F.W: {α : Type} → Factory α → ℕ
W) :
      ∃ ms: ?m.9113
ms h: ?m.9118
h, ml: ?m.8978
ml = MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: ?m.9113
ms h: ?m.9118
h ∧ ∃ m_better: ?m.9153
m_better, m_better: ?m.9153
m_better ∈ ms: ?m.9113
ms ∧ dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: ?m.8959
F m_better: ?m.9153
m_better m: ?m.9051
m := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_widen: Widen Doc.nl D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_widen: Widen Doc.nl D
h_widenα✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_mem: d_choiceless ∈ [Doc.nl]

nl∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
  α✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_widen: Widen Doc.nl D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesimp at h_mem: d_choiceless ∈ [Doc.nl]
h_memα✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_mem: d_choiceless = Doc.nl

nl∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
  α✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_widen: Widen Doc.nl D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesubst h_mem: d_choiceless = Doc.nl
h_memα✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

m: Meas

h_print: Resolve F Doc.nl c i ml

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

nl∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true
  α✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_widen: Widen Doc.nl D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_print: Resolve F Doc.nl c i ml
h_printα✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_bad✝: c > F.W ∨ i > F.W

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

nl.line_taint∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true
α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

nl.line_set∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
  α✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_widen: Widen Doc.nl D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase line_set h': MeasRender F Doc.nl c i m✝
h' => 
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truehave := MeasRender_deterministic: ∀ {α : Type} {d : Doc} {c i : ℕ} {F : Factory α} {m₁ m₂ : Meas}, MeasRender F d c i m₁ → MeasRender F d c i m₂ → m₁ = m₂
MeasRender_deterministic h_render: MeasRender F Doc.nl c i m
h_render h': MeasRender F Doc.nl c i m✝
h'α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

this: m = m✝

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesubst this: ?m.9998
thisα✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h': MeasRender F Doc.nl c i m

∃ ms h,
  MeasureSet.set [m] (_ : ¬[m] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = true 
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = trueexists [m: Meas
m], (α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h': MeasRender F Doc.nl c i m

∃ ms h,
  MeasureSet.set [m] (_ : ¬[m] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h': MeasRender F Doc.nl c i m

[m] ≠ []simp
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

h': MeasRender F Doc.nl c i m

MeasureSet.set [m] (_ : ¬[m] = []) = MeasureSet.set [m] (_ : ¬[m] = []) ∧   ∃ m_better, m_better ∈ [m] ∧ dominates F m_better m = true
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

∃ ms h,
  MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesimp [dominates_refl: ∀ {α : Type} {m : Meas} (F : Factory α), dominates F m m = true
dominates_refl]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

c, i: ℕ

ml: MeasureSet

D: List Doc

d_choiceless: Doc

m: Meas

h_print: Resolve F Doc.nl c i ml

h_widen: Widen Doc.nl D

h_mem: d_choiceless ∈ D

h_render: MeasRender F d_choiceless c i m

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

∃ ms h, ml = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase line_taint h_bad: c > F.W ∨ i > F.W
h_bad h_render': MeasRender F Doc.nl c i m✝
h_render' => 
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_render: MeasRender F Doc.nl c i m
h_renderα✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

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

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

nl∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } = true
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truesimp at h_y: { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.y ≤ F.W
h_y h_x: { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i }.x ≤ F.W
h_xα✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

h_y: i ≤ F.W

h_x: c ≤ F.W ∧ i ≤ F.W

nl∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } = true 
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_render': MeasRender F Doc.nl c i m✝

h_y: i ≤ F.W

h_x: c ≤ F.W ∧ i ≤ F.W

h✝: c > F.W

nl.inl∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } = true
α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_render': MeasRender F Doc.nl c i m✝

h_y: i ≤ F.W

h_x: c ≤ F.W ∧ i ≤ F.W

h✝: i > F.W

nl.inr∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } = true 
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase inl h_bad: ?m.14955
h_bad => α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_render': MeasRender F Doc.nl c i m✝

h_y: i ≤ F.W

h_x: c ≤ F.W ∧ i ≤ F.W

h_bad: c > F.W

∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } = truelinarith
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

c, i: ℕ

m: Meas

h_y: m.y ≤ F.W

h_x: m.x ≤ F.W

h_render: MeasRender F Doc.nl c i m

m✝: Meas

h_bad: c > F.W ∨ i > F.W

h_render': MeasRender F Doc.nl c i m✝

∃ ms h, MeasureSet.tainted m✝ = MeasureSet.set ms h ∧ ∃ m_better, m_better ∈ ms ∧ dominates F m_better m = truecase inr h_bad: ?m.14956
h_bad => α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_render': MeasRender F Doc.nl c i m✝

h_y: i ≤ F.W

h_x: c ≤ F.W ∧ i ≤ F.W

h_bad: i > F.W

∃ ms h,
  MeasureSet.tainted m✝ = MeasureSet.set ms h ∧     ∃ m_better,
      m_better ∈ ms ∧         dominates F m_better { last := i, cost := Factory.nl F i, doc := Doc.nl, x := max c i, y := i } = truelinarith
Goals accomplished! 🐙