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

/-!
## Lemmas for the informal proof of time complexity of $Π_e$
-/

/--
A measure set from resolving will have size 
at most $W_\mathcal{F} + 1$ (Lemma 5.9) 
-/
lemma Resolve_bound: ∀ {α : Type} {ms : List Meas} {F : Factory α} {d : Doc} {c i : ℕ} {h_not_empty : ms ≠ []},
  Resolve F d c i (MeasureSet.set ms h_not_empty) → List.length ms ≤ F.W + 1
Resolve_bound
    {h_not_empty: ms ≠ []
h_not_empty : ms: ?m.5
ms ≠ []: unknown metavariable '?_uniq.39'
[]}
    (h: Resolve F d c i (MeasureSet.set ms h_not_empty)
h : Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: ?m.18
F d: ?m.33
d c: ?m.47
c i: ?m.61
i (MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: ?m.5
ms h_not_empty: ms ≠ []
h_not_empty)) : 
    ms: ?m.5
ms.length: {α : Type ?u.86} → List α → ℕ
length ≤ F: ?m.18
F.W: {α : Type} → Factory α → ℕ
W + 1: ?m.96
1 := by
Goals accomplished! 🐙 
  α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: ms ≠ []

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

List.length ms ≤ F.W + 1have h_last: ?m.182
h_last := (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 (MeasureSet.set ms h_not_empty)
h).left: ∀ {a b : Prop}, a ∧ b → a
leftα✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: ms ≠ []

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

h_last: last_decreasing ms

List.length ms ≤ F.W + 1
  α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: ms ≠ []

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

List.length ms ≤ F.W + 1cases ms: List Meas
msα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: [] ≠ []

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

h_last: last_decreasing []

nilList.length [] ≤ F.W + 1
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

head✝: Meas

tail✝: List Meas

h_not_empty: head✝ :: tail✝ ≠ []

h: Resolve F d c i (MeasureSet.set (head✝ :: tail✝) h_not_empty)

h_last: last_decreasing (head✝ :: tail✝)

consList.length (head✝ :: tail✝) ≤ F.W + 1
  α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: ms ≠ []

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

List.length ms ≤ F.W + 1case nil => α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: [] ≠ []

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

h_last: last_decreasing []

List.length [] ≤ F.W + 1simp
Goals accomplished! 🐙
  α✝: Type

ms: List Meas

F: Factory α✝

d: Doc

c, i: ℕ

h_not_empty: ms ≠ []

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

List.length ms ≤ F.W + 1case cons hd: ?m.228
hd tl: List ?m.228
tl =>
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1have h_bound: (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1), isLt := ?m.766 }).last ≥   List.length (hd :: tl) - 1
h_bound : ((hd: ?m.228
hd :: tl: List ?m.228
tl).get: {α : Type ?u.620} → (as : List α) → Fin (List.length as) → α
get ⟨(hd: ?m.228
hd :: tl: List ?m.228
tl).length: {α : Type ?u.638} → List α → ℕ
length - 1: ?m.643
1 - ((hd: ?m.228
hd :: tl: List ?m.228
tl).length: {α : Type ?u.658} → List α → ℕ
length - 1: ?m.663
1), α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1by
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1) < List.length (hd :: tl)simp
Goals accomplished! 🐙⟩).last: {α : Type} → Meas → ℕ
last ≥ (hd: ?m.228
hd :: tl: List ?m.228
tl).length: {α : Type ?u.774} → List α → ℕ
length - 1: ?m.779
1 := α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1by
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

(List.get (hd :: tl)
      { val := List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1),
        isLt :=
          (_ :
            Nat.succ (List.length tl) - Nat.succ 0 - (Nat.succ (List.length tl) - Nat.succ 0) <               Nat.succ (List.length tl)) }).last ≥   List.length (hd :: tl) - 1{α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

(List.get (hd :: tl)
      { val := List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1),
        isLt :=
          (_ :
            Nat.succ (List.length tl) - Nat.succ 0 - (Nat.succ (List.length tl) - Nat.succ 0) <               Nat.succ (List.length tl)) }).last ≥   List.length (hd :: tl) - 1
      α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

(List.get (hd :: tl)
      { val := List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1),
        isLt :=
          (_ :
            Nat.succ (List.length tl) - Nat.succ 0 - (Nat.succ (List.length tl) - Nat.succ 0) <               Nat.succ (List.length tl)) }).last ≥   List.length (hd :: tl) - 1dwi { α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

(List.get (hd :: tl)
      { val := List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1),
        isLt :=
          (_ :
            Nat.succ (List.length tl) - Nat.succ 0 - (Nat.succ (List.length tl) - Nat.succ 0) <               Nat.succ (List.length tl)) }).last ≥   List.length (hd :: tl) - 1apply last_decreasing_bound: ∀ {α : Type} {ms : List Meas},
  last_decreasing ms →
    ∀ (i : ℕ) (hi : List.length ms - 1 - i < List.length ms),
      i < List.length ms → (List.get ms { val := List.length ms - 1 - i, isLt := hi }).last ≥ i
last_decreasing_boundα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

hlast_decreasing (hd :: tl)
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

h_boundList.length (hd :: tl) - 1 < List.length (hd :: tl) }
Goals accomplished! 🐙
    }
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1simp at h_bound: (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1), isLt := ?m.766 }).last ≥   List.length (hd :: tl) - 1
h_boundα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

List.length (hd :: tl) ≤ F.W + 1
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1have h_last: ?m.5447
h_last := @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 _: Type
_ _: List Meas
_ _: Factory ?m.5448
_ _: Doc
_ _: ℕ
_ _: ℕ
_ hd: ?m.228
hd (α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

List.length (hd :: tl) ≤ F.W + 1by
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

hd :: tl ≠ []simp
Goals accomplished! 🐙) h: Resolve F d c i (MeasureSet.set (hd :: tl) h_not_empty)
h (α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

List.length (hd :: tl) ≤ F.W + 1by
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

hd ∈ hd :: tlsimp
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last✝: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

h_last: hd.last ≤ F.W

List.length (hd :: tl) ≤ F.W + 1
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1simp_arithα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last✝: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

h_last: hd.last ≤ F.W

List.length tl ≤ F.W 
    α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last: last_decreasing (hd :: tl)

List.length (hd :: tl) ≤ F.W + 1dwi { α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last✝: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

h_last: hd.last ≤ F.W

List.length tl ≤ F.Wapply le_trans: ∀ {α : Type ?u.8052} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_transα✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last✝: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

h_last: hd.last ≤ F.W

aList.length tl ≤ ?b
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last✝: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

h_last: hd.last ≤ F.W

a?b ≤ F.W
α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

hd: Meas

tl: List Meas

h_not_empty: hd :: tl ≠ []

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

h_last✝: last_decreasing (hd :: tl)

h_bound: List.length tl ≤ hd.last

h_last: hd.last ≤ F.W

bℕ }
Goals accomplished! 🐙

/--
If resolving happens at a printing context that 
exceeds $W_\mathcal{F}$, the result will always 
be tainted (Lemma 5.10)
-/
lemma Resolve_exceeding_tainted: ∀ {α : Type} {F : Factory α} {d : Doc} {c i : ℕ} {ms : MeasureSet},
  Resolve F d c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m
Resolve_exceeding_tainted
  (h: Resolve F d c i ms
h : Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: ?m.9999
F d: ?m.10006
d c: ?m.10012
c i: ?m.10018
i ms: ?m.10024
ms) 
  (h_bad: c > F.W ∨ i > F.W
h_bad : c: ?m.10012
c > F: ?m.9999
F.W: {α : Type} → Factory α → ℕ
W ∨ i: ?m.10018
i > F: ?m.9999
F.W: {α : Type} → Factory α → ℕ
W) : ∃ m: ?m.10050
m, ms: ?m.10024
ms = MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: ?m.10050
m := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted minduction d: Doc
d generalizing c: ℕ
c i: ℕ
i ms: MeasureSet
msα✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

ms: MeasureSet

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

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

text∃ m, ms = MeasureSet.tainted m
α✝: Type

F: Factory α✝

c, i: ℕ

ms: MeasureSet

h: Resolve F Doc.nl c i ms

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

nl∃ m, ms = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

concat∃ m, ms = MeasureSet.tainted m
α✝: Type

F: Factory α✝

n✝: ℕ

d✝: Doc

d_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

nest∃ m, ms = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d✝: Doc

d_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

align∃ m, ms = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

d₁_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

choice∃ m, ms = MeasureSet.tainted m
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted mcase text => 
    α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcases h: Resolve F (Doc.text s✝) c i ms
hα✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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

m✝: Meas

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

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

text_taint∃ m, MeasureSet.tainted m✝ = MeasureSet.tainted m
α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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

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_set∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m 
    α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase text_taint m: Meas
m _ _ => α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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

m: Meas

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

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

∃ m_1, MeasureSet.tainted m = MeasureSet.tainted m_1exists m: Meas
m
Goals accomplished! 🐙 
    α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase text_set h_c: c + String.length s✝ ≤ F.W
h_c h_i: i ≤ F.W
h_i _ => 
      α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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

m✝: Meas

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

h_i: i ≤ F.W

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

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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✝: c > F.W

inl∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m
α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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✝: i > F.W

inr∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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

m✝: Meas

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

h_i: i ≤ F.W

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

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcase inl h_bad: ?m.11062
h_bad => 
        α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: c > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mhave : c: ℕ
c ≤ F: Factory α✝
F.W: {α : Type} → Factory α → ℕ
W := α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: c > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: c > F.W

c ≤ F.Wlinarith
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: c > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mreplace h_bad: ?m.12958
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.11062
h_badα✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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: c ≤ F.W

h_bad: ¬c ≤ F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: c > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcontradiction
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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

m✝: Meas

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

h_i: i ≤ F.W

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

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcase inr h_bad: ?m.11063
h_bad => 
        α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: i > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mreplace h_bad: ?m.13528
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.11063
h_badα✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: ¬i ≤ F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

s✝: String

c, i: ℕ

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_bad: i > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcontradiction
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted mcase nl => 
    α✝: Type

F: Factory α✝

c, i: ℕ

ms: MeasureSet

h: Resolve F Doc.nl c i ms

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

∃ m, ms = MeasureSet.tainted mcases h: Resolve F Doc.nl c i ms
hα✝: Type

F: Factory α✝

c, i: ℕ

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

m✝: Meas

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

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

line_taint∃ m, MeasureSet.tainted m✝ = MeasureSet.tainted m
α✝: Type

F: Factory α✝

c, i: ℕ

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

m✝: Meas

h_c✝: c ≤ F.W

h_i✝: i ≤ F.W

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

line_set∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m 
    α✝: Type

F: Factory α✝

c, i: ℕ

ms: MeasureSet

h: Resolve F Doc.nl c i ms

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

∃ m, ms = MeasureSet.tainted mcase line_taint m: Meas
m _ _ => α✝: Type

F: Factory α✝

c, i: ℕ

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

m: Meas

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

h✝: MeasRender F Doc.nl c i m

∃ m_1, MeasureSet.tainted m = MeasureSet.tainted m_1exists m: Meas
m
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

c, i: ℕ

ms: MeasureSet

h: Resolve F Doc.nl c i ms

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

∃ m, ms = MeasureSet.tainted mcase line_set h_c: c ≤ F.W
h_c h_i: i ≤ F.W
h_i _ => 
      α✝: Type

F: Factory α✝

c, i: ℕ

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

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h✝: c > F.W

inl∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m
α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h✝: i > F.W

inr∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

c, i: ℕ

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

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcase inl h_bad: ?m.14742
h_bad => 
        α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h_bad: c > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mreplace h_bad: ?m.14787
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.14742
h_badα✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h_bad: ¬c ≤ F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h_bad: c > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcontradiction
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

c, i: ℕ

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

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcase inr h_bad: ?m.14743
h_bad => 
        α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h_bad: i > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mreplace h_bad: ?m.15223
h_bad := Nat.not_le_of_lt: ∀ {n m : ℕ}, m < n → ¬n ≤ m
Nat.not_le_of_lt h_bad: ?m.14743
h_badα✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h_bad: ¬i ≤ F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

c, i: ℕ

m✝: Meas

h_c: c ≤ F.W

h_i: i ≤ F.W

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

h_bad: i > F.W

∃ m, MeasureSet.set [m✝] (_ : ¬[m✝] = []) = MeasureSet.tainted mcontradiction
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted mcase nest n: ℕ
n _ ih: ?m.10127 d✝
ih => 
    α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcases h: Resolve F (Doc.nest n d✝) c i ms
hα✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

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

nest∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted m
    α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase nest h: Resolve F d✝ c (i + n) ms✝
h => 
      α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

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

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mcases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h✝: c > F.W

inl∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted m
α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h✝: i > F.W

inr∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

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

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mcase inl h_bad: ?m.16100
h_bad => 
        α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mlet ⟨m: Meas
m, _⟩ := ih: ?m.10127 d✝
ih h: Resolve F d✝ c (i + n) ms✝
h (α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

c > F.W ∨ i + n > F.W{α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

c > F.W ∨ i + n > F.W
          α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

c > F.W ∨ i + n > F.Wleftα✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

hc > F.W
          α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

c > F.W ∨ i + n > F.Wlinarith
Goals accomplished! 🐙
        }
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

m: Meas

h✝: ms✝ = MeasureSet.tainted m

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mexists m: Meas
m.adjust_nest: {α : Type} → ℕ → Meas → Meas
adjust_nest n: ℕ
nα✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

m: Meas

h✝: ms✝ = MeasureSet.tainted m

MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted (Meas.adjust_nest n m)
        α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted msimp [*, MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift, Meas.adjust_nest: {α : Type} → ℕ → Meas → Meas
Meas.adjust_nest]
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

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

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mcase inr h_bad: ?m.16101
h_bad => 
        α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mlet ⟨m: Meas
m, _⟩ := ih: ?m.10127 d✝
ih h: Resolve F d✝ c (i + n) ms✝
h (α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

c > F.W ∨ i + n > F.W{α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

c > F.W ∨ i + n > F.W
          α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

c > F.W ∨ i + n > F.Wrightα✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

hi + n > F.W
          α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

c > F.W ∨ i + n > F.Wlinarith
Goals accomplished! 🐙
        }
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

m: Meas

h✝: ms✝ = MeasureSet.tainted m

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted mexists m: Meas
m.adjust_nest: {α : Type} → ℕ → Meas → Meas
adjust_nest n: ℕ
nα✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

m: Meas

h✝: ms✝ = MeasureSet.tainted m

MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted (Meas.adjust_nest n m)
        α✝: Type

F: Factory α✝

n: ℕ

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

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

h_bad: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_nest n) ms✝ = MeasureSet.tainted msimp [*, MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift, Meas.adjust_nest: {α : Type} → ℕ → Meas → Meas
Meas.adjust_nest]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted mcase align ih: ?m.10127 d✝
ih => 
    α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcases h: Resolve F (Doc.align d✝) c i ms
hα✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

h✝: Resolve F d✝ c c ms✝

h_bad✝: i > F.W

align_taint∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms✝) = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

h✝: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

align∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted m
    α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase align h: Resolve F d✝ c c ms✝
h _ => 
      α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mcases h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h✝: c > F.W

inl∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h✝: i > F.W

inr∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mcase inl h_bad: ?m.26770
h_bad => 
        α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mlet ⟨m: Meas
m, _⟩ := ih: ?m.10127 d✝
ih h: Resolve F d✝ c c ms✝
h (α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

c > F.W ∨ c > F.W{α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

c > F.W ∨ c > F.W
          α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

c > F.W ∨ c > F.Wleftα✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

hc > F.W
          α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

c > F.W ∨ c > F.Wlinarith
Goals accomplished! 🐙
        }
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

m: Meas

h✝: ms✝ = MeasureSet.tainted m

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted m
        α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mexists m: Meas
m.adjust_align: {α : Type} → ℕ → Meas → Meas
adjust_align i: ℕ
iα✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

m: Meas

h✝: ms✝ = MeasureSet.tainted m

MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted (Meas.adjust_align i m)
        α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h_bad: c > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted msimp [*, MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift, Meas.adjust_align: {α : Type} → ℕ → Meas → Meas
Meas.adjust_align]
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mcase inr => α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms✝: MeasureSet

h: Resolve F d✝ c c ms✝

h_ok✝: i ≤ F.W

h✝: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) ms✝ = MeasureSet.tainted mlinarith
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase align_taint ms: MeasureSet
ms h: Resolve F d✝ c c ms
h _ => 
      α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms: MeasureSet

h: Resolve F d✝ c c ms

h_bad✝: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms) = MeasureSet.tainted mcases ms: MeasureSet
msα✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

h_bad✝: i > F.W

m✝: Meas

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

tainted∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.tainted m✝)) = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

h_bad✝: i > F.W

ms✝: List Meas

h✝: ms✝ ≠ []

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

set∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms✝ h✝)) = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms: MeasureSet

h: Resolve F d✝ c c ms

h_bad✝: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms) = MeasureSet.tainted mcase tainted m: Meas
m => α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

h_bad✝: i > F.W

m: Meas

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

∃ m_1, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.tainted m)) = MeasureSet.tainted m_1exists m: Meas
m.adjust_align: {α : Type} → ℕ → Meas → Meas
adjust_align i: ℕ
i
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms: MeasureSet

h: Resolve F d✝ c c ms

h_bad✝: i > F.W

∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms) = MeasureSet.tainted mcase set ms: List Meas
ms _ => α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

h_bad✝: i > F.W

ms: List Meas

h✝: ms ≠ []

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

∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms h✝)) = MeasureSet.tainted mexists (ms: List Meas
ms.head: {α : Type ?u.37938} → (as : List α) → as ≠ [] → α
head (α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

h_bad✝: i > F.W

ms: List Meas

h✝: ms ≠ []

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

∃ m, MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint (MeasureSet.set ms h✝)) = MeasureSet.tainted mby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

d✝: Doc

ih: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

h_bad✝: i > F.W

ms: List Meas

h✝: ms ≠ []

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

ms ≠ []assumption
Goals accomplished! 🐙)).adjust_align: {α : Type} → ℕ → Meas → Meas
adjust_align i: ℕ
i
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted mcase choice ih₁: ?m.10127 d₁✝
ih₁ ih₂: ?m.10127 d₂✝
ih₂ => 
    α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcases h: Resolve F (Doc.choice d₁✝ d₂✝) c i ms
hα✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left✝: Resolve F d₁✝ c i ms✝

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

choice∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted m 
    α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase choice h_left: Resolve F d₁✝ c i ms✝
h_left h_right: Resolve F d₂✝ c i ms'✝
h_right => 
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted mlet ⟨m: Meas
m, h: ms✝ = MeasureSet.tainted m
h⟩ := ih₁: ?m.10127 d₁✝
ih₁ h_left: Resolve F d₁✝ c i ms✝
h_left h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

m: Meas

h: ms✝ = MeasureSet.tainted m

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted m
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted mlet ⟨m': Meas
m', h': ms'✝ = MeasureSet.tainted m'
h'⟩ := ih₂: ?m.10127 d₂✝
ih₂ h_right: Resolve F d₂✝ c i ms'✝
h_right h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

m: Meas

h: ms✝ = MeasureSet.tainted m

m': Meas

h': ms'✝ = MeasureSet.tainted m'

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted m
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted mexists m: Meas
mα✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

m: Meas

h: ms✝ = MeasureSet.tainted m

m': Meas

h': ms'✝ = MeasureSet.tainted m'

MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted msubst h: ms✝ = MeasureSet.tainted m
h h': ms'✝ = MeasureSet.tainted m'
h'α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

m, m': Meas

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

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

MeasureSet.union F (MeasureSet.tainted m) (MeasureSet.tainted m') = MeasureSet.tainted m
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

ih₂: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

ms✝, ms'✝: MeasureSet

h_left: Resolve F d₁✝ c i ms✝

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

∃ m, MeasureSet.union F ms✝ ms'✝ = MeasureSet.tainted msimp [*, MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

d: Doc

c, i: ℕ

ms: MeasureSet

h: Resolve F d c i ms

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

∃ m, ms = MeasureSet.tainted mcase concat ih₁: ?m.10127 d₁✝
ih₁ _ => 
    α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcases h: Resolve F (Doc.concat d₁✝ d₂✝) c i ms
hα✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

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✝)

concat_taint∃ m, MeasureSet.tainted (Meas.concat F m✝ m'✝) = MeasureSet.tainted m
α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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∃ m, ms = MeasureSet.tainted m 
    α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase concat_taint m₁: Meas
m₁ _ m₂: Meas
m₂ _ _ _ => 
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

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

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₁)

∃ m, MeasureSet.tainted (Meas.concat F m₁ m₂) = MeasureSet.tainted mexists (Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: Factory α✝
F m₁: Meas
m₁ m₂: Meas
m₂)
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcase concat_set h_left: Resolve F d₁✝ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left _ => 
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mlet ⟨_, _⟩ := ih₁: ?m.10127 d₁✝
ih₁ h_left: Resolve F d₁✝ c i (MeasureSet.set ms✝ h_non_empty✝)
h_left h_bad: c > F.W ∨ i > F.W
h_badα✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

w✝: Meas

h✝: MeasureSet.set ms✝ h_non_empty✝ = MeasureSet.tainted w✝

∃ m, ms = MeasureSet.tainted m 
      α✝: Type

F: Factory α✝

d₁✝, d₂✝: Doc

ih₁: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₁✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

d₂_ih✝: ∀ {c i : ℕ} {ms : MeasureSet}, Resolve F d₂✝ c i ms → c > F.W ∨ i > F.W → ∃ m, ms = MeasureSet.tainted m

c, i: ℕ

ms: MeasureSet

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

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

∃ m, ms = MeasureSet.tainted mcontradiction
Goals accomplished! 🐙