import Pretty.Defs.Basic
import Pretty.Supports.Basic
import Pretty.Supports.FactoryMath
import Pretty.Supports.Domination

/-!
Various lemmas about list of measures when 
they are decreasing in last length and increasing in cost.
-/

lemma last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head (h: last_decreasing (x :: y :: xs)
h : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (x: ?m.7
x :: y: ?m.17
y :: xs: ?m.27
xs)) :
    x: ?m.7
x.last: {α : Type} → Meas → ℕ
last > y: ?m.17
y.last: {α : Type} → Meas → ℕ
last := by
Goals accomplished! 🐙
  α✝: Type

x, y: Meas

xs: List Meas

h: last_decreasing (x :: y :: xs)

x.last > y.lastexact h: last_decreasing (x :: y :: xs)
h 0: ?m.64
0 (α✝: Type

x, y: Meas

xs: List Meas

h: last_decreasing (x :: y :: xs)

x.last > y.lastby
Goals accomplished! 🐙 α✝: Type

x, y: Meas

xs: List Meas

h: last_decreasing (x :: y :: xs)

0 < List.length (x :: y :: xs)simp
Goals accomplished! 🐙) (α✝: Type

x, y: Meas

xs: List Meas

h: last_decreasing (x :: y :: xs)

x.last > y.lastby
Goals accomplished! 🐙 α✝: Type

x, y: Meas

xs: List Meas

h: last_decreasing (x :: y :: xs)

0 + 1 < List.length (x :: y :: xs)simp
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest (h: last_decreasing (x :: xs)
h : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (x: ?m.371
x :: xs: ?m.379
xs)) :
    last_decreasing: {α : Type} → List Meas → Prop
last_decreasing xs: ?m.379
xs := by
Goals accomplished! 🐙
  α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

last_decreasing xsintro i: ℕ
i _: i < List.length xs
_ _: i + 1 < List.length xs
_α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

(List.get xs { val := i, isLt := hi✝ }).last > (List.get xs { val := i + 1, isLt := hj✝ }).last 
  α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

last_decreasing xsexact h: last_decreasing (x :: xs)
h (i: ℕ
i + 1: ?m.415
1) (α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

(List.get xs { val := i, isLt := hi✝ }).last > (List.get xs { val := i + 1, isLt := hj✝ }).lastby
Goals accomplished! 🐙 α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs){α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs) α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs)simp_arithα✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 ≤ List.length xs;α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 ≤ List.length xs α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs)linarith
Goals accomplished! 🐙 }
Goals accomplished! 🐙) 
    (α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

(List.get xs { val := i, isLt := hi✝ }).last > (List.get xs { val := i + 1, isLt := hj✝ }).lastby
Goals accomplished! 🐙 α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs){α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs) α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs)simp_arithα✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 2 ≤ List.length xs;α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 2 ≤ List.length xs α✝: Type

x: Meas

xs: List Meas

h: last_decreasing (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs)linarith
Goals accomplished! 🐙 }
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma last_decreasing_empty: ∀ {α : Type}, last_decreasing []
last_decreasing_empty : @last_decreasing: {α : Type} → List Meas → Prop
last_decreasing α: ?m.5411
α []: List ?m.5415
[] := by
Goals accomplished! 🐙 
  α: Type

last_decreasing []intro _: ℕ
_ _: i✝ < List.length []
_ _: i✝ + 1 < List.length []
_α: Type

i✝: ℕ

hi✝: i✝ < List.length []

hj✝: i✝ + 1 < List.length []

(List.get [] { val := i✝, isLt := hi✝ }).last > (List.get [] { val := i✝ + 1, isLt := hj✝ }).last 
  α: Type

last_decreasing []contradiction
Goals accomplished! 🐙

lemma last_decreasing_one: ∀ {α : Type} {x : Meas}, last_decreasing [x]
last_decreasing_one : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing [x: ?m.5527
x] := by
Goals accomplished! 🐙 
  α✝: Type

x: Meas

last_decreasing [x]intro _: ℕ
_ _: i✝ < List.length [x]
_ _: i✝ + 1 < List.length [x]
_α✝: Type

x: Meas

i✝: ℕ

hi✝: i✝ < List.length [x]

hj✝: i✝ + 1 < List.length [x]

(List.get [x] { val := i✝, isLt := hi✝ }).last > (List.get [x] { val := i✝ + 1, isLt := hj✝ }).last 
  α✝: Type

x: Meas

last_decreasing [x]contradiction
Goals accomplished! 🐙

lemma last_decreasing_cons: ∀ {α : Type} (x y : Meas) (xs : List Meas), x.last > y.last → last_decreasing (y :: xs) → last_decreasing (x :: y :: xs)
last_decreasing_cons {α: Type
α : Type: Type 1
Type} (x: Meas
x y: Meas
y : @Meas: {α : Type} → Type
Meas α: Type
α) (xs: List Meas
xs : List: Type ?u.5999 → Type ?u.5999
List Meas: {α : Type} → Type
Meas)
    (h_last: x.last > y.last
h_last : x: Meas
x.last: {α : Type} → Meas → ℕ
last > y: Meas
y.last: {α : Type} → Meas → ℕ
last)
    (h: last_decreasing (y :: xs)
h : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (y: Meas
y :: xs: List Meas
xs)) : 
    last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (x: Meas
x :: y: Meas
y :: xs: List Meas
xs) := by
Goals accomplished! 🐙
  α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

last_decreasing (x :: y :: xs)intro i: ℕ
i _: i < List.length (x :: y :: xs)
_ _: i + 1 < List.length (x :: y :: xs)
_α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: i < List.length (x :: y :: xs)

hj✝: i + 1 < List.length (x :: y :: xs)

(List.get (x :: y :: xs) { val := i, isLt := hi✝ }).last > (List.get (x :: y :: xs) { val := i + 1, isLt := hj✝ }).last 
  α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

last_decreasing (x :: y :: xs)cases i: ℕ
iα: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

hi✝: Nat.zero < List.length (x :: y :: xs)

hj✝: Nat.zero + 1 < List.length (x :: y :: xs)

zero(List.get (x :: y :: xs) { val := Nat.zero, isLt := hi✝ }).last >   (List.get (x :: y :: xs) { val := Nat.zero + 1, isLt := hj✝ }).last
α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

n✝: ℕ

hi✝: Nat.succ n✝ < List.length (x :: y :: xs)

hj✝: Nat.succ n✝ + 1 < List.length (x :: y :: xs)

succ(List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := hi✝ }).last >   (List.get (x :: y :: xs) { val := Nat.succ n✝ + 1, isLt := hj✝ }).last 
  α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

last_decreasing (x :: y :: xs)case zero => α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

hi✝: Nat.zero < List.length (x :: y :: xs)

hj✝: Nat.zero + 1 < List.length (x :: y :: xs)

(List.get (x :: y :: xs) { val := Nat.zero, isLt := hi✝ }).last >   (List.get (x :: y :: xs) { val := Nat.zero + 1, isLt := hj✝ }).lastsimp [h_last: x.last > y.last
h_last]
Goals accomplished! 🐙
  α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

last_decreasing (x :: y :: xs)case succ i: ℕ
i _ _ => 
    α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

(List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).last >   (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).lastexact h: last_decreasing (y :: xs)
h i: ℕ
i (α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

(List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).last >   (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).lastby
Goals accomplished! 🐙 α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs){α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)
      α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)simp_arith at *α: Type

x, y: Meas

xs: List Meas

h: last_decreasing (y :: xs)

i: ℕ

h_last: y.last + 1 ≤ x.last

hi✝: i ≤ List.length xs

hj✝: i + 1 ≤ List.length xs

i ≤ List.length xs
      α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)assumption
Goals accomplished! 🐙
    }
Goals accomplished! 🐙) (α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

(List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).last >   (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).lastby
Goals accomplished! 🐙 α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs){α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)
      α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)simp_arith at *α: Type

x, y: Meas

xs: List Meas

h: last_decreasing (y :: xs)

i: ℕ

h_last: y.last + 1 ≤ x.last

hi✝: i ≤ List.length xs

hj✝: i + 1 ≤ List.length xs

i + 1 ≤ List.length xs
      α: Type

x, y: Meas

xs: List Meas

h_last: x.last > y.last

h: last_decreasing (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)assumption
Goals accomplished! 🐙
    }
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma last_decreasing_strong: ∀ {α : Type} {ms : List Meas},
  last_decreasing ms →
    ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
      i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).last
last_decreasing_strong (h: last_decreasing ms
h : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing ms: ?m.9152
ms) : 
  ∀ (i: ℕ
i j: ℕ
j : ℕ: Type
ℕ) (h_i: i < List.length ms
h_i : i: ℕ
i < ms: ?m.9152
ms.length: {α : Type ?u.9166} → List α → ℕ
length) (h_j: j < List.length ms
h_j : j: ℕ
j < ms: ?m.9152
ms.length: {α : Type ?u.9178} → List α → ℕ
length),
    i: ℕ
i < j: ℕ
j →
    (ms: ?m.9152
ms.get: {α : Type ?u.9192} → (as : List α) → Fin (List.length as) → α
get ⟨i: ℕ
i, by
Goals accomplished! 🐙 ms: List Meas

h: last_decreasing ms

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

i < List.length msassumption
Goals accomplished! 🐙⟩).last: {α : Type} → Meas → ℕ
last > (ms: ?m.9152
ms.get: {α : Type ?u.9206} → (as : List α) → Fin (List.length as) → α
get ⟨j: ℕ
j, by
Goals accomplished! 🐙 ms: List Meas

h: last_decreasing ms

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

j < List.length msassumption
Goals accomplished! 🐙⟩).last: {α : Type} → Meas → ℕ
last := by
Goals accomplished! 🐙
  α✝: Type

ms: List Meas

h: last_decreasing ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).lastintro i: ℕ
i j: ℕ
j hi: i < List.length ms
hi hj: j < List.length ms
hj h_lt: i < j
h_ltα✝: Type

ms: List Meas

h: last_decreasing ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_lt: i < j

(List.get ms { val := i, isLt := hi }).last > (List.get ms { val := j, isLt := hj }).last
  α✝: Type

ms: List Meas

h: last_decreasing ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).lastinduction ms: List Meas
ms generalizing i: ℕ
i j: ℕ
jα✝: Type

h: last_decreasing []

i, j: ℕ

hi: i < List.length []

hj: j < List.length []

h_lt: i < j

nil(List.get [] { val := i, isLt := hi }).last > (List.get [] { val := j, isLt := hj }).last
α✝: Type

head✝: Meas

tail✝: List Meas

tail_ih✝: last_decreasing tail✝ →
  ∀ (i j : ℕ) (hi : i < List.length tail✝) (hj : j < List.length tail✝),
    i < j → (List.get tail✝ { val := i, isLt := hi }).last > (List.get tail✝ { val := j, isLt := hj }).last

h: last_decreasing (head✝ :: tail✝)

i, j: ℕ

hi: i < List.length (head✝ :: tail✝)

hj: j < List.length (head✝ :: tail✝)

h_lt: i < j

cons(List.get (head✝ :: tail✝) { val := i, isLt := hi }).last > (List.get (head✝ :: tail✝) { val := j, isLt := hj }).last
  α✝: Type

ms: List Meas

h: last_decreasing ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).lastcase nil => 
    α✝: Type

h: last_decreasing []

i, j: ℕ

hi: i < List.length []

hj: j < List.length []

h_lt: i < j

(List.get [] { val := i, isLt := hi }).last > (List.get [] { val := j, isLt := hj }).lastsimp at hi: i < List.length []
hi
Goals accomplished! 🐙 
  α✝: Type

ms: List Meas

h: last_decreasing ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).lastcase cons hd: ?m.9286
hd tl: List ?m.9286
tl ih: ?m.9287 tl
ih => 
    α✝: Type

hd: Meas

tl: List Meas

ih: last_decreasing tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

h: last_decreasing (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

(List.get (hd :: tl) { val := i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastspecialize ih: ?m.9287 tl
ih (last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest h: last_decreasing (hd :: tl)
h)α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

(List.get (hd :: tl) { val := i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).last
    α✝: Type

hd: Meas

tl: List Meas

ih: last_decreasing tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

h: last_decreasing (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

(List.get (hd :: tl) { val := i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcases i: ℕ
iα✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

zero(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).last
α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

n✝: ℕ

hi: Nat.succ n✝ < List.length (hd :: tl)

h_lt: Nat.succ n✝ < j

succ(List.get (hd :: tl) { val := Nat.succ n✝, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).last 
    α✝: Type

hd: Meas

tl: List Meas

ih: last_decreasing tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

h: last_decreasing (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

(List.get (hd :: tl) { val := i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcase zero => 
      α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcases j: ℕ
jα✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi, hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < Nat.zero

zero(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last > (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).last
α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

n✝: ℕ

hj: Nat.succ n✝ < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ n✝

succ(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ n✝, isLt := hj }).last
      α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcase zero => α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi, hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < Nat.zero

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last > (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).lastsimp at h_lt: Nat.zero < Nat.zero
h_lt
Goals accomplished! 🐙
      α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcase succ j: ℕ
j => 
        α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ j

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastcases tl: List ?m.9286
tlα✝: Type

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

h: last_decreasing [hd]

ih: ∀ (i j : ℕ) (hi : i < List.length []) (hj : j < List.length []),
  i < j → (List.get [] { val := i, isLt := hi }).last > (List.get [] { val := j, isLt := hj }).last

hi: Nat.zero < List.length [hd]

hj: Nat.succ j < List.length [hd]

nil(List.get [hd] { val := Nat.zero, isLt := hi }).last > (List.get [hd] { val := Nat.succ j, isLt := hj }).last
α✝: Type

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: ∀ (i j : ℕ) (hi : i < List.length (head✝ :: tail✝)) (hj : j < List.length (head✝ :: tail✝)),
  i < j →
    (List.get (head✝ :: tail✝) { val := i, isLt := hi }).last >       (List.get (head✝ :: tail✝) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: head✝ :: tail✝)

hj: Nat.succ j < List.length (hd :: head✝ :: tail✝)

cons(List.get (hd :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: head✝ :: tail✝) { val := Nat.succ j, isLt := hj }).last 
        α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ j

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastcase nil => α✝: Type

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

h: last_decreasing [hd]

ih: ∀ (i j : ℕ) (hi : i < List.length []) (hj : j < List.length []),
  i < j → (List.get [] { val := i, isLt := hi }).last > (List.get [] { val := j, isLt := hj }).last

hi: Nat.zero < List.length [hd]

hj: Nat.succ j < List.length [hd]

(List.get [hd] { val := Nat.zero, isLt := hi }).last > (List.get [hd] { val := Nat.succ j, isLt := hj }).lastsimp at hj: Nat.succ j < List.length [hd]
hj
Goals accomplished! 🐙
        α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ j

(List.get (hd :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastcase cons hd2: ?m.9636
hd2 tl: List ?m.9636
tl => 
          α✝: Type

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

hj: Nat.succ j < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ j, isLt := hj }).lastcases j: ℕ
jα✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

h_lt: Nat.zero < Nat.succ Nat.zero

hj: Nat.succ Nat.zero < List.length (hd :: hd2 :: tl)

zero(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ Nat.zero, isLt := hj }).last
α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

n✝: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ n✝)

hj: Nat.succ (Nat.succ n✝) < List.length (hd :: hd2 :: tl)

succ(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ n✝), isLt := hj }).last 
          α✝: Type

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

hj: Nat.succ j < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ j, isLt := hj }).lastcase zero => 
            α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

h_lt: Nat.zero < Nat.succ Nat.zero

hj: Nat.succ Nat.zero < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ Nat.zero, isLt := hj }).lastsimp [last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head h: last_decreasing (hd :: hd2 :: tl)
h]
Goals accomplished! 🐙
          α✝: Type

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

hj: Nat.succ j < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ j, isLt := hj }).lastcase succ j: ℕ
j => 
            α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lasthave := last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head h: last_decreasing (hd :: hd2 :: tl)
hα✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

this: hd.last > hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).last
            α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastsimp at hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)
hjα✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).last
            α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastspecialize ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last
ih 0: ?m.10204
0 (j: ℕ
j + 1: ?m.10218
1) (α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastby
Goals accomplished! 🐙 α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

0 < List.length (hd2 :: tl)simp
Goals accomplished! 🐙) (α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastby
Goals accomplished! 🐙 α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

j + 1 < List.length (hd2 :: tl){α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

j + 1 < List.length (hd2 :: tl)
              α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

j + 1 < List.length (hd2 :: tl)simpα✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

j + 1 < Nat.succ (List.length tl)
              α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

j + 1 < List.length (hd2 :: tl)linarith
Goals accomplished! 🐙
            }
Goals accomplished! 🐙) (α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastby
Goals accomplished! 🐙 α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

0 < j + 1simp
Goals accomplished! 🐙)α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

ih: (List.get (hd2 :: tl) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tl)) }).last >   (List.get (hd2 :: tl) { val := j + 1, isLt := (_ : j + 1 < List.length (hd2 :: tl)) }).last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).last
            α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastsimp at ih: (List.get (hd2 :: tl) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tl)) }).last >   (List.get (hd2 :: tl) { val := j + 1, isLt := (_ : j + 1 < List.length (hd2 :: tl)) }).last
ihα✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

ih: (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last < hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).last
            α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j → (List.get (hd2 :: tl) { val := i, isLt := hi }).last > (List.get (hd2 :: tl) { val := j, isLt := hj }).last

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastdwi { α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

ih: (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last < hd2.last

(List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last >   (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).lastapply lt_trans: ∀ {α : Type ?u.13521} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
lt_transα✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

ih: (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last < hd2.last

a(List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).last < ?b
α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

ih: (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last < hd2.last

a?b < (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).last
α✝: Type

hd, hd2: Meas

tl: List Meas

h: last_decreasing (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: hd.last > hd2.last

ih: (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last < hd2.last

bℕ }
Goals accomplished! 🐙
    α✝: Type

hd: Meas

tl: List Meas

ih: last_decreasing tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

h: last_decreasing (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

(List.get (hd :: tl) { val := i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcase succ i: ℕ
i => 
      α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

h_lt: Nat.succ i < j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcases j: ℕ
jα✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.zero

zero(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).last
α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

n✝: ℕ

hj: Nat.succ n✝ < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ n✝

succ(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ n✝, isLt := hj }).last 
      α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

h_lt: Nat.succ i < j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcase zero => α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.zero

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).lastsimp at h_lt: Nat.succ i < Nat.zero
h_lt
Goals accomplished! 🐙 
      α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

h_lt: Nat.succ i < j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last > (List.get (hd :: tl) { val := j, isLt := hj }).lastcase succ j: ℕ
j => 
        α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastsimp at hi: Nat.succ i < List.length (hd :: tl)
hi hj: Nat.succ j < List.length (hd :: tl)
hjα✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).last
        α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastspecialize ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last
ih i: ℕ
i j: ℕ
j (α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastby
Goals accomplished! 🐙 α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

i < List.length tllinarith
Goals accomplished! 🐙) (α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastby
Goals accomplished! 🐙 α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

j < List.length tllinarith
Goals accomplished! 🐙) (α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastby
Goals accomplished! 🐙 α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

i < jlinarith
Goals accomplished! 🐙)α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

ih: (List.get tl { val := i, isLt := (_ : i < List.length tl) }).last >   (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).last
        α✝: Type

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → (List.get tl { val := i, isLt := hi }).last > (List.get tl { val := j, isLt := hj }).last

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ j

(List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).lastsimp [ih: (List.get tl { val := i, isLt := (_ : i < List.length tl) }).last >   (List.get tl { val := j, isLt := (_ : j < List.length tl) }).last
ih]
Goals accomplished! 🐙

lemma cost_increasing_head: ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas},
  cost_increasing F (x :: y :: xs) → Factory.lt F x.cost y.cost
cost_increasing_head (h: cost_increasing F (x :: y :: xs)
h : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.21738
F (x: ?m.21748
x :: y: ?m.21758
y :: xs: ?m.21768
xs)) :
    F: ?m.21738
F.lt: {α : Type} → Factory α → α → α → Prop
lt x: ?m.21748
x.cost: {α : Type} → Meas → α
cost y: ?m.21758
y.cost: {α : Type} → Meas → α
cost := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing F (x :: y :: xs)

Factory.lt F x.cost y.costexact h: cost_increasing F (x :: y :: xs)
h 0: ?m.21807
0 (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing F (x :: y :: xs)

Factory.lt F x.cost y.costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing F (x :: y :: xs)

0 < List.length (x :: y :: xs)simp
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing F (x :: y :: xs)

Factory.lt F x.cost y.costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing F (x :: y :: xs)

0 + 1 < List.length (x :: y :: xs)simp
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma cost_increasing_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas}, cost_increasing F (x :: xs) → cost_increasing F xs
cost_increasing_rest (h: cost_increasing F (x :: xs)
h : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.22115
F (x: ?m.22125
x :: xs: ?m.22133
xs)) :
    cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.22115
F xs: ?m.22133
xs := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

cost_increasing F xsintro i: ℕ
i _: i < List.length xs
_ _: i + 1 < List.length xs
_α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

Factory.lt F (List.get xs { val := i, isLt := hi✝ }).cost (List.get xs { val := i + 1, isLt := hj✝ }).cost 
  α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

cost_increasing F xsexact h: cost_increasing F (x :: xs)
h (i: ℕ
i + 1: ?m.22170
1) (α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

Factory.lt F (List.get xs { val := i, isLt := hi✝ }).cost (List.get xs { val := i + 1, isLt := hj✝ }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs){α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs) α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs)simp_arithα✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 ≤ List.length xs;α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 ≤ List.length xs α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs)linarith
Goals accomplished! 🐙 }
Goals accomplished! 🐙) 
    (α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

Factory.lt F (List.get xs { val := i, isLt := hi✝ }).cost (List.get xs { val := i + 1, isLt := hj✝ }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs){α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs) α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs)simp_arithα✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 2 ≤ List.length xs;α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 2 ≤ List.length xs α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs)linarith
Goals accomplished! 🐙 }
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma cost_increasing_empty: ∀ {α : Type} {F : Factory α}, cost_increasing F []
cost_increasing_empty : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.27168
F []: List ?m.27175
[] := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

cost_increasing F []intro _: ℕ
_ _: i✝ < List.length []
_ _: i✝ + 1 < List.length []
_α✝: Type

F: Factory α✝

i✝: ℕ

hi✝: i✝ < List.length []

hj✝: i✝ + 1 < List.length []

Factory.lt F (List.get [] { val := i✝, isLt := hi✝ }).cost (List.get [] { val := i✝ + 1, isLt := hj✝ }).cost 
  α✝: Type

F: Factory α✝

cost_increasing F []contradiction
Goals accomplished! 🐙

lemma cost_increasing_one: ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing F [x]
cost_increasing_one : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.27288
F [x: ?m.27298
x] := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

x: Meas

cost_increasing F [x]intro _: ℕ
_ _: i✝ < List.length [x]
_ _: i✝ + 1 < List.length [x]
_α✝: Type

F: Factory α✝

x: Meas

i✝: ℕ

hi✝: i✝ < List.length [x]

hj✝: i✝ + 1 < List.length [x]

Factory.lt F (List.get [x] { val := i✝, isLt := hi✝ }).cost (List.get [x] { val := i✝ + 1, isLt := hj✝ }).cost 
  α✝: Type

F: Factory α✝

x: Meas

cost_increasing F [x]contradiction
Goals accomplished! 🐙

lemma cost_increasing_cons: ∀ {α : Type} {F : Factory α} (x y : Meas) (xs : List Meas),
  Factory.lt F x.cost y.cost → cost_increasing F (y :: xs) → cost_increasing F (x :: y :: xs)
cost_increasing_cons (x: Meas
x y: Meas
y : Meas: {α : Type} → Type
Meas) (xs: List Meas
xs : List: Type ?u.27790 → Type ?u.27790
List Meas: {α : Type} → Type
Meas)
    (h_cost: ?m.27794
h_cost : F: ?m.27781
FF.lt x.cost y.cost: Sort ?u.27776
.lt: {α : Type} → Factory α → α → α → Prop
ltF.lt x.cost y.cost: Sort ?u.27776
 x: Meas
xF.lt x.cost y.cost: Sort ?u.27776
.cost: {α : Type} → Meas → α
costF.lt x.cost y.cost: Sort ?u.27776
 y: Meas
yF.lt x.cost y.cost: Sort ?u.27776
.cost: {α : Type} → Meas → α
cost)
    (h: cost_increasing F (y :: xs)
h : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.27781
F (y: Meas
y :: xs: List Meas
xs)) : 
    cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.27781
F (x: Meas
x :: y: Meas
y :: xs: List Meas
xs) := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

cost_increasing F (x :: y :: xs)intro i: ℕ
i _: i < List.length (x :: y :: xs)
_ _: i + 1 < List.length (x :: y :: xs)
_α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: i < List.length (x :: y :: xs)

hj✝: i + 1 < List.length (x :: y :: xs)

Factory.lt F (List.get (x :: y :: xs) { val := i, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := i + 1, isLt := hj✝ }).cost 
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

cost_increasing F (x :: y :: xs)cases i: ℕ
iα✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

hi✝: Nat.zero < List.length (x :: y :: xs)

hj✝: Nat.zero + 1 < List.length (x :: y :: xs)

zeroFactory.lt F (List.get (x :: y :: xs) { val := Nat.zero, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := Nat.zero + 1, isLt := hj✝ }).cost
α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

n✝: ℕ

hi✝: Nat.succ n✝ < List.length (x :: y :: xs)

hj✝: Nat.succ n✝ + 1 < List.length (x :: y :: xs)

succFactory.lt F (List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := Nat.succ n✝ + 1, isLt := hj✝ }).cost 
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

cost_increasing F (x :: y :: xs)case zero => α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

hi✝: Nat.zero < List.length (x :: y :: xs)

hj✝: Nat.zero + 1 < List.length (x :: y :: xs)

Factory.lt F (List.get (x :: y :: xs) { val := Nat.zero, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := Nat.zero + 1, isLt := hj✝ }).costsimp [h_cost: Factory.lt F x.cost y.cost
h_cost]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

cost_increasing F (x :: y :: xs)case succ i: ℕ
i _ _ => 
    α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

Factory.lt F (List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).costexact h: cost_increasing F (y :: xs)
h i: ℕ
i (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

Factory.lt F (List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs){α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)simp_arith at *α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: i ≤ List.length xs

hj✝: i + 1 ≤ List.length xs

i ≤ List.length xs
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)assumption
Goals accomplished! 🐙
    }
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

Factory.lt F (List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs){α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)simp_arith at *α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: i ≤ List.length xs

hj✝: i + 1 ≤ List.length xs

i + 1 ≤ List.length xs
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.lt F x.cost y.cost

h: cost_increasing F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)assumption
Goals accomplished! 🐙
    }
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma cost_increasing_strong: ∀ {α : Type} {F : Factory α} {ms : List Meas},
  cost_increasing F ms →
    ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
      i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost
cost_increasing_strong (h: cost_increasing F ms
h : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.30327
F ms: ?m.30334
ms) : 
  ∀ (i: ℕ
i j: ℕ
j : ℕ: Type
ℕ) (h_i: i < List.length ms
h_i : i: ℕ
i < ms: ?m.30334
ms.length: {α : Type ?u.30348} → List α → ℕ
length) (h_j: j < List.length ms
h_j : j: ℕ
j < ms: ?m.30334
ms.length: {α : Type ?u.30360} → List α → ℕ
length),
    i: ℕ
i < j: ℕ
j →
    F: ?m.30327
F.lt: {α : Type} → Factory α → α → α → Prop
lt (ms: ?m.30334
ms.get: {α : Type ?u.30379} → (as : List α) → Fin (List.length as) → α
get ⟨i: ℕ
i, by
Goals accomplished! 🐙 F: Factory ?m.30404

ms: List Meas

h: cost_increasing F ms

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

i < List.length msassumption
Goals accomplished! 🐙⟩).cost: {α : Type} → Meas → α
cost (ms: ?m.30334
ms.get: {α : Type ?u.30393} → (as : List α) → Fin (List.length as) → α
get ⟨j: ℕ
j, by
Goals accomplished! 🐙 F: Factory ?m.30404

ms: List Meas

h: cost_increasing F ms

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

j < List.length msassumption
Goals accomplished! 🐙⟩).cost: {α : Type} → Meas → α
cost := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing F ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).costintro i: ℕ
i j: ℕ
j hi: i < List.length ms
hi hj: j < List.length ms
hj h_lt: i < j
h_ltα✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_lt: i < j

Factory.lt F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost
  α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing F ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).costinduction ms: List Meas
ms generalizing i: ℕ
i j: ℕ
jα✝: Type

F: Factory α✝

h: cost_increasing F []

i, j: ℕ

hi: i < List.length []

hj: j < List.length []

h_lt: i < j

nilFactory.lt F (List.get [] { val := i, isLt := hi }).cost (List.get [] { val := j, isLt := hj }).cost
α✝: Type

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: cost_increasing F tail✝ →
  ∀ (i j : ℕ) (hi : i < List.length tail✝) (hj : j < List.length tail✝),
    i < j → Factory.lt F (List.get tail✝ { val := i, isLt := hi }).cost (List.get tail✝ { val := j, isLt := hj }).cost

h: cost_increasing F (head✝ :: tail✝)

i, j: ℕ

hi: i < List.length (head✝ :: tail✝)

hj: j < List.length (head✝ :: tail✝)

h_lt: i < j

consFactory.lt F (List.get (head✝ :: tail✝) { val := i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := j, isLt := hj }).cost
  α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing F ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).costcase nil => 
    α✝: Type

F: Factory α✝

h: cost_increasing F []

i, j: ℕ

hi: i < List.length []

hj: j < List.length []

h_lt: i < j

Factory.lt F (List.get [] { val := i, isLt := hi }).cost (List.get [] { val := j, isLt := hj }).costsimp at hi: i < List.length []
hi
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing F ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).costcase cons hd: ?m.30473
hd tl: List ?m.30473
tl ih: ?m.30474 tl
ih => 
    α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: cost_increasing F tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

h: cost_increasing F (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

Factory.lt F (List.get (hd :: tl) { val := i, isLt := hi }).cost (List.get (hd :: tl) { val := j, isLt := hj }).costspecialize ih: ?m.30474 tl
ih (cost_increasing_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas}, cost_increasing F (x :: xs) → cost_increasing F xs
cost_increasing_rest h: cost_increasing F (hd :: tl)
h)α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

Factory.lt F (List.get (hd :: tl) { val := i, isLt := hi }).cost (List.get (hd :: tl) { val := j, isLt := hj }).cost
    α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: cost_increasing F tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

h: cost_increasing F (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

Factory.lt F (List.get (hd :: tl) { val := i, isLt := hi }).cost (List.get (hd :: tl) { val := j, isLt := hj }).costcases i: ℕ
iα✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

zeroFactory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).cost
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

n✝: ℕ

hi: Nat.succ n✝ < List.length (hd :: tl)

h_lt: Nat.succ n✝ < j

succFactory.lt F (List.get (hd :: tl) { val := Nat.succ n✝, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).cost 
    α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: cost_increasing F tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

h: cost_increasing F (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

Factory.lt F (List.get (hd :: tl) { val := i, isLt := hi }).cost (List.get (hd :: tl) { val := j, isLt := hj }).costcase zero => 
      α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).costcases j: ℕ
jα✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi, hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < Nat.zero

zeroFactory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).cost
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

n✝: ℕ

hj: Nat.succ n✝ < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ n✝

succFactory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ n✝, isLt := hj }).cost
      α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).costcase zero => α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi, hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < Nat.zero

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).costsimp at h_lt: Nat.zero < Nat.zero
h_lt
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

h_lt: Nat.zero < j

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).costcase succ j: ℕ
j => 
        α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costcases tl: List ?m.30473
tlα✝: Type

F: Factory α✝

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

h: cost_increasing F [hd]

ih: ∀ (i j : ℕ) (hi : i < List.length []) (hj : j < List.length []),
  i < j → Factory.lt F (List.get [] { val := i, isLt := hi }).cost (List.get [] { val := j, isLt := hj }).cost

hi: Nat.zero < List.length [hd]

hj: Nat.succ j < List.length [hd]

nilFactory.lt F (List.get [hd] { val := Nat.zero, isLt := hi }).cost (List.get [hd] { val := Nat.succ j, isLt := hj }).cost
α✝: Type

F: Factory α✝

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: ∀ (i j : ℕ) (hi : i < List.length (head✝ :: tail✝)) (hj : j < List.length (head✝ :: tail✝)),
  i < j →
    Factory.lt F (List.get (head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (head✝ :: tail✝) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: head✝ :: tail✝)

hj: Nat.succ j < List.length (hd :: head✝ :: tail✝)

consFactory.lt F (List.get (hd :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: head✝ :: tail✝) { val := Nat.succ j, isLt := hj }).cost 
        α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costcase nil => α✝: Type

F: Factory α✝

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

h: cost_increasing F [hd]

ih: ∀ (i j : ℕ) (hi : i < List.length []) (hj : j < List.length []),
  i < j → Factory.lt F (List.get [] { val := i, isLt := hi }).cost (List.get [] { val := j, isLt := hj }).cost

hi: Nat.zero < List.length [hd]

hj: Nat.succ j < List.length [hd]

Factory.lt F (List.get [hd] { val := Nat.zero, isLt := hi }).cost (List.get [hd] { val := Nat.succ j, isLt := hj }).costsimp at hj: Nat.succ j < List.length [hd]
hj
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.zero < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costcase cons hd2: ?m.30825
hd2 tl: List ?m.30825
tl => 
          α✝: Type

F: Factory α✝

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

hj: Nat.succ j < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ j, isLt := hj }).costcases j: ℕ
jα✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

h_lt: Nat.zero < Nat.succ Nat.zero

hj: Nat.succ Nat.zero < List.length (hd :: hd2 :: tl)

zeroFactory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ Nat.zero, isLt := hj }).cost
α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

n✝: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ n✝)

hj: Nat.succ (Nat.succ n✝) < List.length (hd :: hd2 :: tl)

succFactory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ n✝), isLt := hj }).cost 
          α✝: Type

F: Factory α✝

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

hj: Nat.succ j < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ j, isLt := hj }).costcase zero => 
            α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

h_lt: Nat.zero < Nat.succ Nat.zero

hj: Nat.succ Nat.zero < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ Nat.zero, isLt := hj }).costsimp [cost_increasing_head: ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas},
  cost_increasing F (x :: y :: xs) → Factory.lt F x.cost y.cost
cost_increasing_head h: cost_increasing F (hd :: hd2 :: tl)
h]
Goals accomplished! 🐙
          α✝: Type

F: Factory α✝

hd: Meas

j: ℕ

h_lt: Nat.zero < Nat.succ j

hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

hj: Nat.succ j < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ j, isLt := hj }).costcase succ j: ℕ
j => 
            α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costhave := cost_increasing_head: ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas},
  cost_increasing F (x :: y :: xs) → Factory.lt F x.cost y.cost
cost_increasing_head h: cost_increasing F (hd :: hd2 :: tl)
hα✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

this: Factory.lt F hd.cost hd2.cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).cost
            α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costsimp at hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)
hjα✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).cost
            α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costspecialize ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost
ih 0: ?m.31281
0 (j: ℕ
j + 1: ?m.31295
1) (α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

0 < List.length (hd2 :: tl)simp
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

j + 1 < List.length (hd2 :: tl){α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

j + 1 < List.length (hd2 :: tl)
              α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

j + 1 < List.length (hd2 :: tl)simpα✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

j + 1 < Nat.succ (List.length tl)
              α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

j + 1 < List.length (hd2 :: tl)linarith
Goals accomplished! 🐙
            }
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

0 < j + 1simp
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

ih: Factory.lt F (List.get (hd2 :: tl) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tl)) }).cost
  (List.get (hd2 :: tl) { val := j + 1, isLt := (_ : j + 1 < List.length (hd2 :: tl)) }).cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).cost
            α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costsimp at ih: Factory.lt F (List.get (hd2 :: tl) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tl)) }).cost
  (List.get (hd2 :: tl) { val := j + 1, isLt := (_ : j + 1 < List.length (hd2 :: tl)) }).cost
ihα✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

ih: Factory.lt F hd2.cost (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).cost
            α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length (hd2 :: tl)) (hj : j < List.length (hd2 :: tl)),
  i < j →
    Factory.lt F (List.get (hd2 :: tl) { val := i, isLt := hi }).cost
      (List.get (hd2 :: tl) { val := j, isLt := hj }).cost

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < List.length (hd :: hd2 :: tl)

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costdwi { α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

ih: Factory.lt F hd2.cost (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost

Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost
  (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).costapply F: Factory α✝
F.lt_trans: ∀ {α : Type} {F : Factory α} {c₁ c₂ c₃ : α}, Factory.lt F c₁ c₂ → Factory.lt F c₂ c₃ → Factory.lt F c₁ c₃
lt_transα✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

ih: Factory.lt F hd2.cost (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost

h₁Factory.lt F (List.get (hd :: hd2 :: tl) { val := Nat.zero, isLt := hi }).cost ?m.34280
α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

ih: Factory.lt F hd2.cost (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost

h₂Factory.lt F ?m.34280 (List.get (hd :: hd2 :: tl) { val := Nat.succ (Nat.succ j), isLt := hj }).cost
α✝: Type

F: Factory α✝

hd, hd2: Meas

tl: List Meas

h: cost_increasing F (hd :: hd2 :: tl)

hi: Nat.zero < List.length (hd :: hd2 :: tl)

j: ℕ

h_lt: Nat.zero < Nat.succ (Nat.succ j)

hj: Nat.succ (Nat.succ j) < Nat.succ (Nat.succ (List.length tl))

this: Factory.lt F hd.cost hd2.cost

ih: Factory.lt F hd2.cost (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost

α✝ }
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: cost_increasing F tl →
  ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
    i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

h: cost_increasing F (hd :: tl)

i, j: ℕ

hi: i < List.length (hd :: tl)

hj: j < List.length (hd :: tl)

h_lt: i < j

Factory.lt F (List.get (hd :: tl) { val := i, isLt := hi }).cost (List.get (hd :: tl) { val := j, isLt := hj }).costcase succ i: ℕ
i => 
      α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

h_lt: Nat.succ i < j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).costcases j: ℕ
jα✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.zero

zeroFactory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).cost
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

n✝: ℕ

hj: Nat.succ n✝ < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ n✝

succFactory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ n✝, isLt := hj }).cost 
      α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

h_lt: Nat.succ i < j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).costcase zero => α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

hj: Nat.zero < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.zero

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.zero, isLt := hj }).costsimp at h_lt: Nat.succ i < Nat.zero
h_lt
Goals accomplished! 🐙 
      α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

j: ℕ

hj: j < List.length (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

h_lt: Nat.succ i < j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := j, isLt := hj }).costcase succ j: ℕ
j => 
        α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costsimp at hi: Nat.succ i < List.length (hd :: tl)
hi hj: Nat.succ j < List.length (hd :: tl)
hjα✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).cost
        α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costspecialize ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost
ih i: ℕ
i j: ℕ
j (α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

i < List.length tllinarith
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

j < List.length tllinarith
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

i < jlinarith
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

i: ℕ

hi: Nat.succ i < Nat.succ (List.length tl)

j: ℕ

hj: Nat.succ j < Nat.succ (List.length tl)

h_lt: Nat.succ i < Nat.succ j

ih: Factory.lt F (List.get tl { val := i, isLt := (_ : i < List.length tl) }).cost
  (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).cost
        α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: ∀ (i j : ℕ) (hi : i < List.length tl) (hj : j < List.length tl),
  i < j → Factory.lt F (List.get tl { val := i, isLt := hi }).cost (List.get tl { val := j, isLt := hj }).cost

i: ℕ

hi: Nat.succ i < List.length (hd :: tl)

j: ℕ

hj: Nat.succ j < List.length (hd :: tl)

h_lt: Nat.succ i < Nat.succ j

Factory.lt F (List.get (hd :: tl) { val := Nat.succ i, isLt := hi }).cost
  (List.get (hd :: tl) { val := Nat.succ j, isLt := hj }).costsimp [ih: Factory.lt F (List.get tl { val := i, isLt := (_ : i < List.length tl) }).cost
  (List.get tl { val := j, isLt := (_ : j < List.length tl) }).cost
ih]
Goals accomplished! 🐙

lemma cost_increasing_non_strict_head: ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: y :: xs) → Factory.le F x.cost y.cost = true
cost_increasing_non_strict_head (h: cost_increasing_non_strict F (x :: y :: xs)
h : cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.42130
F (x: ?m.42140
x :: y: ?m.42150
y :: xs: ?m.42160
xs)) :
    F: ?m.42130
F.le: {α : Type} → Factory α → α → α → Bool
le x: ?m.42140
x.cost: {α : Type} → Meas → α
cost y: ?m.42150
y.cost: {α : Type} → Meas → α
cost := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: y :: xs)

Factory.le F x.cost y.cost = trueexact h: cost_increasing_non_strict F (x :: y :: xs)
h 0: ?m.42203
0 (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: y :: xs)

Factory.le F x.cost y.cost = trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: y :: xs)

0 < List.length (x :: y :: xs)simp
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: y :: xs)

Factory.le F x.cost y.cost = trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: y :: xs)

0 + 1 < List.length (x :: y :: xs)simp
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma cost_increasing_non_strict_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs
cost_increasing_non_strict_rest (h: cost_increasing_non_strict F (x :: xs)
h : cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.42513
F (x: ?m.42523
x :: xs: ?m.42531
xs)) :
    cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.42513
F xs: ?m.42531
xs := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

cost_increasing_non_strict F xsintro i: ℕ
i _: i < List.length xs
_ _: i + 1 < List.length xs
_α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

Factory.le F (List.get xs { val := i, isLt := hi✝ }).cost (List.get xs { val := i + 1, isLt := hj✝ }).cost = true 
  α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

cost_increasing_non_strict F xsexact h: cost_increasing_non_strict F (x :: xs)
h (i: ℕ
i + 1: ?m.42568
1) (α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

Factory.le F (List.get xs { val := i, isLt := hi✝ }).cost (List.get xs { val := i + 1, isLt := hj✝ }).cost = trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs){α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs) α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs)simp_arithα✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 ≤ List.length xs;α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 ≤ List.length xs α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 < List.length (x :: xs)linarith
Goals accomplished! 🐙 }
Goals accomplished! 🐙) 
    (α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

Factory.le F (List.get xs { val := i, isLt := hi✝ }).cost (List.get xs { val := i + 1, isLt := hj✝ }).cost = trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs){α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs) α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs)simp_arithα✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 2 ≤ List.length xs;α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 2 ≤ List.length xs α✝: Type

F: Factory α✝

x: Meas

xs: List Meas

h: cost_increasing_non_strict F (x :: xs)

i: ℕ

hi✝: i < List.length xs

hj✝: i + 1 < List.length xs

i + 1 + 1 < List.length (x :: xs)linarith
Goals accomplished! 🐙 }
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma cost_increasing_non_strict_empty: ∀ {α : Type} {F : Factory α}, cost_increasing_non_strict F []
cost_increasing_non_strict_empty : cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.47567
F []: List ?m.47574
[] := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

cost_increasing_non_strict F []intro _: ℕ
_ _: i✝ < List.length []
_ _: i✝ + 1 < List.length []
_α✝: Type

F: Factory α✝

i✝: ℕ

hi✝: i✝ < List.length []

hj✝: i✝ + 1 < List.length []

Factory.le F (List.get [] { val := i✝, isLt := hi✝ }).cost (List.get [] { val := i✝ + 1, isLt := hj✝ }).cost = true 
  α✝: Type

F: Factory α✝

cost_increasing_non_strict F []contradiction
Goals accomplished! 🐙

lemma cost_increasing_non_strict_one: ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing_non_strict F [x]
cost_increasing_non_strict_one : cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.47687
F [x: ?m.47697
x] := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

x: Meas

cost_increasing_non_strict F [x]intro _: ℕ
_ _: i✝ < List.length [x]
_ _: i✝ + 1 < List.length [x]
_α✝: Type

F: Factory α✝

x: Meas

i✝: ℕ

hi✝: i✝ < List.length [x]

hj✝: i✝ + 1 < List.length [x]

Factory.le F (List.get [x] { val := i✝, isLt := hi✝ }).cost (List.get [x] { val := i✝ + 1, isLt := hj✝ }).cost = true 
  α✝: Type

F: Factory α✝

x: Meas

cost_increasing_non_strict F [x]contradiction
Goals accomplished! 🐙

lemma cost_increasing_non_strict_cons: ∀ {α : Type} {F : Factory α} (x y : Meas) (xs : List Meas),
  Factory.le F x.cost y.cost = true →
    cost_increasing_non_strict F (y :: xs) → cost_increasing_non_strict F (x :: y :: xs)
cost_increasing_non_strict_cons (x: Meas
x y: Meas
y : Meas: {α : Type} → Type
Meas) (xs: List Meas
xs : List: Type ?u.48172 → Type ?u.48172
List Meas: {α : Type} → Type
Meas)
    (h_cost: ?m.48193
h_cost : F: ?m.48180
FF.le x.cost y.cost: Sort ?u.48175
.le: {α : Type} → Factory α → α → α → Bool
leF.le x.cost y.cost: Sort ?u.48175
 x: Meas
xF.le x.cost y.cost: Sort ?u.48175
.cost: {α : Type} → Meas → α
costF.le x.cost y.cost: Sort ?u.48175
 y: Meas
yF.le x.cost y.cost: Sort ?u.48175
.cost: {α : Type} → Meas → α
cost)
    (h: cost_increasing_non_strict F (y :: xs)
h : cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.48180
F (y: Meas
y :: xs: List Meas
xs)) : 
    cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.48180
F (x: Meas
x :: y: Meas
y :: xs: List Meas
xs) := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

cost_increasing_non_strict F (x :: y :: xs)intro i: ℕ
i _: i < List.length (x :: y :: xs)
_ _: i + 1 < List.length (x :: y :: xs)
_α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: i < List.length (x :: y :: xs)

hj✝: i + 1 < List.length (x :: y :: xs)

Factory.le F (List.get (x :: y :: xs) { val := i, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := i + 1, isLt := hj✝ }).cost =   true 
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

cost_increasing_non_strict F (x :: y :: xs)cases i: ℕ
iα✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

hi✝: Nat.zero < List.length (x :: y :: xs)

hj✝: Nat.zero + 1 < List.length (x :: y :: xs)

zeroFactory.le F (List.get (x :: y :: xs) { val := Nat.zero, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := Nat.zero + 1, isLt := hj✝ }).cost =   true
α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

n✝: ℕ

hi✝: Nat.succ n✝ < List.length (x :: y :: xs)

hj✝: Nat.succ n✝ + 1 < List.length (x :: y :: xs)

succFactory.le F (List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := Nat.succ n✝ + 1, isLt := hj✝ }).cost =   true 
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

cost_increasing_non_strict F (x :: y :: xs)case zero => α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

hi✝: Nat.zero < List.length (x :: y :: xs)

hj✝: Nat.zero + 1 < List.length (x :: y :: xs)

Factory.le F (List.get (x :: y :: xs) { val := Nat.zero, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := Nat.zero + 1, isLt := hj✝ }).cost =   truesimp [h_cost: Factory.le F x.cost y.cost = true
h_cost]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

cost_increasing_non_strict F (x :: y :: xs)case succ i: ℕ
i _ _ => 
    α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

Factory.le F (List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).cost =   trueexact h: cost_increasing_non_strict F (y :: xs)
h i: ℕ
i (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

Factory.le F (List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).cost =   trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs){α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)simp_arith at *α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: i ≤ List.length xs

hj✝: i + 1 ≤ List.length xs

i ≤ List.length xs
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i < List.length (y :: xs)assumption
Goals accomplished! 🐙
    }
Goals accomplished! 🐙) (α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

Factory.le F (List.get (x :: y :: xs) { val := Nat.succ i, isLt := hi✝ }).cost
    (List.get (x :: y :: xs) { val := Nat.succ i + 1, isLt := hj✝ }).cost =   trueby
Goals accomplished! 🐙 α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs){α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)simp_arith at *α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: i ≤ List.length xs

hj✝: i + 1 ≤ List.length xs

i + 1 ≤ List.length xs
      α✝: Type

F: Factory α✝

x, y: Meas

xs: List Meas

h_cost: Factory.le F x.cost y.cost = true

h: cost_increasing_non_strict F (y :: xs)

i: ℕ

hi✝: Nat.succ i < List.length (x :: y :: xs)

hj✝: Nat.succ i + 1 < List.length (x :: y :: xs)

i + 1 < List.length (y :: xs)assumption
Goals accomplished! 🐙
    }
Goals accomplished! 🐙)
Goals accomplished! 🐙

lemma last_decreasing_concat: ∀ {α : Type} {ms : List Meas} (F : Factory α) (m : Meas),
  last_decreasing ms → last_decreasing (List.map (fun m' => Meas.concat F m m') ms)
last_decreasing_concat (F: Factory α
F : Factory: Type → Type
Factory α: ?m.50891
α) (m: Meas
m : Meas: {α : Type} → Type
Meas) (h: last_decreasing ms
h : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing ms: ?m.50901
ms) : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (ms: ?m.50901
ms.map: {α : Type ?u.50916} → {β : Type ?u.50915} → (α → β) → List α → List β
map (fun m': ?m.50924
m' => Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: Factory α
F m: Meas
m m': ?m.50924
m')) := by
Goals accomplished! 🐙 
  α: Type

ms: List Meas

F: Factory α

m: Meas

h: last_decreasing ms

last_decreasing (List.map (fun m' => Meas.concat F m m') ms)induction ms: List Meas
msα: Type

F: Factory α

m: Meas

h: last_decreasing []

nillast_decreasing (List.map (fun m' => Meas.concat F m m') [])
α: Type

F: Factory α

m, head✝: Meas

tail✝: List Meas

tail_ih✝: last_decreasing tail✝ → last_decreasing (List.map (fun m' => Meas.concat F m m') tail✝)

h: last_decreasing (head✝ :: tail✝)

conslast_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝)) 
  α: Type

ms: List Meas

F: Factory α

m: Meas

h: last_decreasing ms

last_decreasing (List.map (fun m' => Meas.concat F m m') ms)case nil => α: Type

F: Factory α

m: Meas

h: last_decreasing []

last_decreasing (List.map (fun m' => Meas.concat F m m') [])apply last_decreasing_empty: ∀ {α : Type}, last_decreasing []
last_decreasing_empty
Goals accomplished! 🐙
  α: Type

ms: List Meas

F: Factory α

m: Meas

h: last_decreasing ms

last_decreasing (List.map (fun m' => Meas.concat F m m') ms)case cons hd: ?m.50964
hd tl: List ?m.50964
tl ih: ?m.50965 tl
ih => 
    α: Type

F: Factory α

m, hd: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (List.map (fun m' => Meas.concat F m m') tl)

h: last_decreasing (hd :: tl)

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: tl))specialize ih: ?m.50965 tl
ih (last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest h: last_decreasing (hd :: tl)
h)α: Type

F: Factory α

m, hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') tl)

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: tl))
    α: Type

F: Factory α

m, hd: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (List.map (fun m' => Meas.concat F m m') tl)

h: last_decreasing (hd :: tl)

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: tl))cases tl: List ?m.50964
tlα: Type

F: Factory α

m, hd: Meas

h: last_decreasing [hd]

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') [])

nillast_decreasing (List.map (fun m' => Meas.concat F m m') [hd])
α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

conslast_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝)) 
    α: Type

F: Factory α

m, hd: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (List.map (fun m' => Meas.concat F m m') tl)

h: last_decreasing (hd :: tl)

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: tl))case nil => α: Type

F: Factory α

m, hd: Meas

h: last_decreasing [hd]

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') [])

last_decreasing (List.map (fun m' => Meas.concat F m m') [hd])simp [last_decreasing_one: ∀ {α : Type} {x : Meas}, last_decreasing [x]
last_decreasing_one]
Goals accomplished! 🐙
    α: Type

F: Factory α

m, hd: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (List.map (fun m' => Meas.concat F m m') tl)

h: last_decreasing (hd :: tl)

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: tl))case cons => 
      α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝))apply last_decreasing_cons: ∀ {α : Type} (x y : Meas) (xs : List Meas), x.last > y.last → last_decreasing (y :: xs) → last_decreasing (x :: y :: xs)
last_decreasing_consα: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h_last((fun m' => Meas.concat F m m') hd).last > ((fun m' => Meas.concat F m m') head✝).last
α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

hlast_decreasing ((fun m' => Meas.concat F m m') head✝ :: List.map (fun m' => Meas.concat F m m') tail✝)
      α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝))case h_last => 
        α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

((fun m' => Meas.concat F m m') hd).last > ((fun m' => Meas.concat F m m') head✝).lastreplace h: ?m.51180
h := last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head h: last_decreasing (hd :: head✝ :: tail✝)
hα: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: hd.last > head✝.last

((fun m' => Meas.concat F m m') hd).last > ((fun m' => Meas.concat F m m') head✝).last 
        α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

((fun m' => Meas.concat F m m') hd).last > ((fun m' => Meas.concat F m m') head✝).lastsimp [h: ?m.51180
h]
Goals accomplished! 🐙
      α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

last_decreasing (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝))case h => α: Type

F: Factory α

m, hd, head✝: Meas

tail✝: List Meas

h: last_decreasing (hd :: head✝ :: tail✝)

ih: last_decreasing (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

last_decreasing ((fun m' => Meas.concat F m m') head✝ :: List.map (fun m' => Meas.concat F m m') tail✝)assumption
Goals accomplished! 🐙 

lemma cost_increasing_non_strict_concat: ∀ {α : Type} {F : Factory α} {ms : List Meas} (m : Meas),
  cost_increasing F ms → cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') ms)
cost_increasing_non_strict_concat (m: Meas
m : Meas: {α : Type} → Type
Meas) (h: cost_increasing F ms
h : cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing F: ?m.51395
F ms: ?m.51405
ms) : cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict F: ?m.51395
F (ms: ?m.51405
ms.map: {α : Type ?u.51418} → {β : Type ?u.51417} → (α → β) → List α → List β
map (fun m': ?m.51426
m' => Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: ?m.51395
F m: Meas
m m': ?m.51426
m')) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: cost_increasing F ms

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') ms)induction ms: List Meas
msα✝: Type

F: Factory α✝

m: Meas

h: cost_increasing F []

nilcost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') [])
α✝: Type

F: Factory α✝

m, head✝: Meas

tail✝: List Meas

tail_ih✝: cost_increasing F tail✝ → cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') tail✝)

h: cost_increasing F (head✝ :: tail✝)

conscost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝)) 
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: cost_increasing F ms

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') ms)case nil => α✝: Type

F: Factory α✝

m: Meas

h: cost_increasing F []

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') [])apply cost_increasing_non_strict_empty: ∀ {α : Type} {F : Factory α}, cost_increasing_non_strict F []
cost_increasing_non_strict_empty
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: cost_increasing F ms

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') ms)case cons hd: ?m.51468
hd tl: List ?m.51468
tl ih: ?m.51469 tl
ih => 
    α✝: Type

F: Factory α✝

m, hd: Meas

tl: List Meas

ih: cost_increasing F tl → cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') tl)

h: cost_increasing F (hd :: tl)

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: tl))specialize ih: ?m.51469 tl
ih (cost_increasing_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas}, cost_increasing F (x :: xs) → cost_increasing F xs
cost_increasing_rest h: cost_increasing F (hd :: tl)
h)α✝: Type

F: Factory α✝

m, hd: Meas

tl: List Meas

h: cost_increasing F (hd :: tl)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') tl)

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: tl))
    α✝: Type

F: Factory α✝

m, hd: Meas

tl: List Meas

ih: cost_increasing F tl → cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') tl)

h: cost_increasing F (hd :: tl)

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: tl))cases tl: List ?m.51468
tlα✝: Type

F: Factory α✝

m, hd: Meas

h: cost_increasing F [hd]

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') [])

nilcost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') [hd])
α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

conscost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝)) 
    α✝: Type

F: Factory α✝

m, hd: Meas

tl: List Meas

ih: cost_increasing F tl → cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') tl)

h: cost_increasing F (hd :: tl)

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: tl))case nil => α✝: Type

F: Factory α✝

m, hd: Meas

h: cost_increasing F [hd]

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') [])

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') [hd])simp [cost_increasing_non_strict_one: ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing_non_strict F [x]
cost_increasing_non_strict_one]
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

m, hd: Meas

tl: List Meas

ih: cost_increasing F tl → cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') tl)

h: cost_increasing F (hd :: tl)

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: tl))case cons => 
      α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝))apply cost_increasing_non_strict_cons: ∀ {α : Type} {F : Factory α} (x y : Meas) (xs : List Meas),
  Factory.le F x.cost y.cost = true →
    cost_increasing_non_strict F (y :: xs) → cost_increasing_non_strict F (x :: y :: xs)
cost_increasing_non_strict_consα✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h_costFactory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = true
α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

hcost_increasing_non_strict F ((fun m' => Meas.concat F m m') head✝ :: List.map (fun m' => Meas.concat F m m') tail✝)
      α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝))case h_cost => 
        α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

Factory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = truereplace h: ?m.51702
h := cost_increasing_head: ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas},
  cost_increasing F (x :: y :: xs) → Factory.lt F x.cost y.cost
cost_increasing_head h: cost_increasing F (hd :: head✝ :: tail✝)
hα✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

Factory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = true 
        α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

Factory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = truesimp [h: ?m.51702
h]α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

Factory.le F (Factory.concat F m.cost hd.cost) (Factory.concat F m.cost head✝.cost) = true
        α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

Factory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = trueapply F: Factory α✝
F.concat_monotonic: ∀ {α : Type} (self : Factory α) {cost₁ cost₂ cost₃ cost₄ : α},
  Factory.le self cost₁ cost₂ = true →
    Factory.le self cost₃ cost₄ = true →
      Factory.le self (Factory.concat self cost₁ cost₃) (Factory.concat self cost₂ cost₄) = true
concat_monotonicα✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

aFactory.le F m.cost m.cost = true
α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

aFactory.le F hd.cost head✝.cost = true 
        α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

Factory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = true. α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

aFactory.le F m.cost m.cost = true
α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

aFactory.le F hd.cost head✝.cost = trueapply F: Factory α✝
F.le_refl: ∀ {α : Type} {F : Factory α} (c : α), Factory.le F c c = true
le_refl
Goals accomplished! 🐙 
        α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

Factory.le F ((fun m' => Meas.concat F m m') hd).cost ((fun m' => Meas.concat F m m') head✝).cost = true. α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

aFactory.le F hd.cost head✝.cost = trueapply Factory.le_of_lt: ∀ {α : Type} {F : Factory α} {c c' : α}, Factory.lt F c c' → Factory.le F c c' = true
Factory.le_of_ltα✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

a.h₁Factory.lt F hd.cost head✝.cost
          α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

h: Factory.lt F hd.cost head✝.cost

aFactory.le F hd.cost head✝.cost = trueassumption
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (hd :: head✝ :: tail✝))case h => α✝: Type

F: Factory α✝

m, hd, head✝: Meas

tail✝: List Meas

h: cost_increasing F (hd :: head✝ :: tail✝)

ih: cost_increasing_non_strict F (List.map (fun m' => Meas.concat F m m') (head✝ :: tail✝))

cost_increasing_non_strict F ((fun m' => Meas.concat F m m') head✝ :: List.map (fun m' => Meas.concat F m m') tail✝)assumption
Goals accomplished! 🐙 

lemma 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 (h: last_decreasing ms
h : last_decreasing: {α : Type} → List Meas → Prop
last_decreasing ms: ?m.51925
ms) (i: ℕ
i : ℕ: Type
ℕ) (hi: List.length ms - 1 - i < List.length ms
hi : ms: ?m.51925
ms.length: {α : Type ?u.51942} → List α → ℕ
length - 1: ?m.51947
1 - i: ℕ
i < ms: ?m.51925
ms.length: {α : Type ?u.51962} → List α → ℕ
length) (h_bound: i < List.length ms
h_bound : i: ℕ
i < ms: ?m.51925
ms.length: {α : Type ?u.52048} → List α → ℕ
length) : (ms: ?m.51925
ms.get: {α : Type ?u.52057} → (as : List α) → Fin (List.length as) → α
get ⟨ms: ?m.51925
ms.length: {α : Type ?u.52073} → List α → ℕ
length - 1: ?m.52078
1 - i: ℕ
i, hi: List.length ms - 1 - i < List.length ms
hi⟩).last: {α : Type} → Meas → ℕ
last ≥ i: ℕ
i := by
Goals accomplished! 🐙 
  α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

hi: List.length ms - 1 - i < List.length ms

h_bound: i < List.length ms

(List.get ms { val := List.length ms - 1 - i, isLt := hi }).last ≥ iinduction i: ℕ
iα✝: Type

ms: List Meas

h: last_decreasing ms

hi: List.length ms - 1 - Nat.zero < List.length ms

h_bound: Nat.zero < List.length ms

zero(List.get ms { val := List.length ms - 1 - Nat.zero, isLt := hi }).last ≥ Nat.zero
α✝: Type

ms: List Meas

h: last_decreasing ms

n✝: ℕ

n_ih✝: ∀ (hi : List.length ms - 1 - n✝ < List.length ms),
  n✝ < List.length ms → (List.get ms { val := List.length ms - 1 - n✝, isLt := hi }).last ≥ n✝

hi: List.length ms - 1 - Nat.succ n✝ < List.length ms

h_bound: Nat.succ n✝ < List.length ms

succ(List.get ms { val := List.length ms - 1 - Nat.succ n✝, isLt := hi }).last ≥ Nat.succ n✝
  α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

hi: List.length ms - 1 - i < List.length ms

h_bound: i < List.length ms

(List.get ms { val := List.length ms - 1 - i, isLt := hi }).last ≥ icase zero => α✝: Type

ms: List Meas

h: last_decreasing ms

hi: List.length ms - 1 - Nat.zero < List.length ms

h_bound: Nat.zero < List.length ms

(List.get ms { val := List.length ms - 1 - Nat.zero, isLt := hi }).last ≥ Nat.zerosimp
Goals accomplished! 🐙
  α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

hi: List.length ms - 1 - i < List.length ms

h_bound: i < List.length ms

(List.get ms { val := List.length ms - 1 - i, isLt := hi }).last ≥ icase succ i: ℕ
i ih: ?m.52187 i
ih => 
    α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

ih: ∀ (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

hi: List.length ms - 1 - Nat.succ i < List.length ms

h_bound: Nat.succ i < List.length ms

(List.get ms { val := List.length ms - 1 - Nat.succ i, isLt := hi }).last ≥ Nat.succ isimpα✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

ih: ∀ (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

hi: List.length ms - 1 - Nat.succ i < List.length ms

h_bound: Nat.succ i < List.length ms

Nat.succ i ≤ (List.get ms { val := List.length ms - 1 - Nat.succ i, isLt := hi }).last
    α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

ih: ∀ (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

hi: List.length ms - 1 - Nat.succ i < List.length ms

h_bound: Nat.succ i < List.length ms

(List.get ms { val := List.length ms - 1 - Nat.succ i, isLt := hi }).last ≥ Nat.succ icases ms: List Meas
msα✝: Type

i: ℕ

h: last_decreasing []

ih: ∀ (hi : List.length [] - 1 - i < List.length []),
  i < List.length [] → (List.get [] { val := List.length [] - 1 - i, isLt := hi }).last ≥ i

hi: List.length [] - 1 - Nat.succ i < List.length []

h_bound: Nat.succ i < List.length []

nilNat.succ i ≤ (List.get [] { val := List.length [] - 1 - Nat.succ i, isLt := hi }).last
α✝: Type

i: ℕ

head✝: Meas

tail✝: List Meas

h: last_decreasing (head✝ :: tail✝)

ih: ∀ (hi : List.length (head✝ :: tail✝) - 1 - i < List.length (head✝ :: tail✝)),
  i < List.length (head✝ :: tail✝) →
    (List.get (head✝ :: tail✝) { val := List.length (head✝ :: tail✝) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (head✝ :: tail✝) - 1 - Nat.succ i < List.length (head✝ :: tail✝)

h_bound: Nat.succ i < List.length (head✝ :: tail✝)

consNat.succ i ≤ (List.get (head✝ :: tail✝) { val := List.length (head✝ :: tail✝) - 1 - Nat.succ i, isLt := hi }).last 
    α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

ih: ∀ (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

hi: List.length ms - 1 - Nat.succ i < List.length ms

h_bound: Nat.succ i < List.length ms

(List.get ms { val := List.length ms - 1 - Nat.succ i, isLt := hi }).last ≥ Nat.succ icase nil => α✝: Type

i: ℕ

h: last_decreasing []

ih: ∀ (hi : List.length [] - 1 - i < List.length []),
  i < List.length [] → (List.get [] { val := List.length [] - 1 - i, isLt := hi }).last ≥ i

hi: List.length [] - 1 - Nat.succ i < List.length []

h_bound: Nat.succ i < List.length []

Nat.succ i ≤ (List.get [] { val := List.length [] - 1 - Nat.succ i, isLt := hi }).lastsimp at hi: List.length [] - 1 - Nat.succ i < List.length []
hi
Goals accomplished! 🐙 
    α✝: Type

ms: List Meas

h: last_decreasing ms

i: ℕ

ih: ∀ (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

hi: List.length ms - 1 - Nat.succ i < List.length ms

h_bound: Nat.succ i < List.length ms

(List.get ms { val := List.length ms - 1 - Nat.succ i, isLt := hi }).last ≥ Nat.succ icase cons hd: ?m.56383
hd tl: List ?m.56383
tl =>
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastsimp at h_bound: Nat.succ i < List.length (hd :: tl)
h_boundα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < Nat.succ (List.length tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastreplace h_bound: ?m.57105
h_bound := Nat.lt_of_succ_lt_succ: ∀ {n m : ℕ}, Nat.succ n < Nat.succ m → n < m
Nat.lt_of_succ_lt_succ h_bound: Nat.succ i < Nat.succ (List.length tl)
h_boundα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastspecialize ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i
ih (α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastby
Goals accomplished! 🐙 α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

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

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastby
Goals accomplished! 🐙 α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

i < List.length (hd :: tl){α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

i < List.length (hd :: tl)
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

i < List.length (hd :: tl)simp_arithα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

i ≤ List.length tl
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

i < List.length (hd :: tl)exact Nat.le_of_lt: ∀ {n m : ℕ}, n < m → n ≤ m
Nat.le_of_lt h_bound: i < List.length tl
h_bound
Goals accomplished! 🐙
      }
Goals accomplished! 🐙)α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

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

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

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

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last
      
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lasthave := last_decreasing_strong: ∀ {α : Type} {ms : List Meas},
  last_decreasing ms →
    ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
      i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).last
last_decreasing_strong h: last_decreasing (hd :: tl)
h _: ℕ
_ ((hd: ?m.56383
hd :: tl: List ?m.56383
tl).length: {α : Type ?u.62336} → List α → ℕ
length - 1: ?m.62341
1 - i: ℕ
i) hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)
hi (α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastby
Goals accomplished! 🐙 α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

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

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastby
Goals accomplished! 🐙 α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - i{α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - i
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - isimpα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length tl - Nat.succ i < List.length tl - i
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - igeneralize h_gen : tl: List Meas
tl.length: {α : Type ?u.67435} → List α → ℕ
length = nα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

n: ℕ

h_gen: List.length tl = n

n - Nat.succ i < n - i
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - isimp [h_gen: List.length tl = n
h_gen] at h_bound: i < List.length tl
h_boundα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

n: ℕ

h_gen: List.length tl = n

h_bound: i < n

n - Nat.succ i < n - i 
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - iclear * - h_bound: i < n
h_boundi, n: ℕ

h_bound: i < n

n - Nat.succ i < n - i 
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - icases n: ℕ
ni: ℕ

h_bound: i < Nat.zero

zeroNat.zero - Nat.succ i < Nat.zero - i
i, n✝: ℕ

h_bound: i < Nat.succ n✝

succNat.succ n✝ - Nat.succ i < Nat.succ n✝ - i
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - icase zero => i: ℕ

h_bound: i < Nat.zero

Nat.zero - Nat.succ i < Nat.zero - isimp at h_bound: i < Nat.zero
h_bound
Goals accomplished! 🐙
        α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl) - 1 - icase succ => 
          i, n✝: ℕ

h_bound: i < Nat.succ n✝

Nat.succ n✝ - Nat.succ i < Nat.succ n✝ - isimpi, n✝: ℕ

h_bound: i < Nat.succ n✝

n✝ - i < Nat.succ n✝ - i 
          i, n✝: ℕ

h_bound: i < Nat.succ n✝

Nat.succ n✝ - Nat.succ i < Nat.succ n✝ - isimp_arith at h_bound: i < Nat.succ n✝
h_boundi, n✝: ℕ

h_bound: i ≤ n✝

n✝ - i < Nat.succ n✝ - i 
          i, n✝: ℕ

h_bound: i < Nat.succ n✝

Nat.succ n✝ - Nat.succ i < Nat.succ n✝ - idwi { i, n✝: ℕ

h_bound: i ≤ n✝

n✝ - i < Nat.succ n✝ - iapply Nat.sub_lt_sub_right: ∀ {a b c : ℕ}, a < b → c ≤ a → a - c < b - c
Nat.sub_lt_sub_righti, n✝: ℕ

h_bound: i ≤ n✝

h0n✝ < Nat.succ n✝
i, n✝: ℕ

h_bound: i ≤ n✝

h1i ≤ n✝ }
Goals accomplished! 🐙
      }
Goals accomplished! 🐙)α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last >   (List.get (hd :: tl)
      { val := List.length (hd :: tl) - 1 - i,
        isLt := (_ : Nat.succ (List.length tl) - Nat.succ 0 - i < Nat.succ (List.length tl)) }).last

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastsimp at this: ?m.62319
thisα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).last
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lasthave : i: ℕ
i < ((hd: ?m.56383
hd :: tl: List ?m.56383
tl).get: {α : Type ?u.72805} → (as : List α) → Fin (List.length as) → α
get ⟨(hd: ?m.56383
hd :: tl: List ?m.56383
tl).length: {α : Type ?u.72823} → List α → ℕ
length - 1: ?m.72828
1 - Nat.succ: ℕ → ℕ
Nat.succ i: ℕ
i, hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)
hi⟩).last: {α : Type} → Meas → ℕ
last := α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastby
Goals accomplished! 🐙 α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

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

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

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

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

i < (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastsimpα✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

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

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: i < List.length tl

ih: i ≤ (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last

this: (List.get (hd :: tl) { val := List.length tl - i, isLt := (_ : List.length tl - i < List.length (hd :: tl)) }).last <   (List.get (hd :: tl)
      { val := List.length tl - Nat.succ i, isLt := (_ : List.length tl - Nat.succ i < List.length (hd :: tl)) }).last

i < (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastlinarith
Goals accomplished! 🐙
      }
Goals accomplished! 🐙
      α✝: Type

i: ℕ

hd: Meas

tl: List Meas

h: last_decreasing (hd :: tl)

ih: ∀ (hi : List.length (hd :: tl) - 1 - i < List.length (hd :: tl)),
  i < List.length (hd :: tl) → (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - i, isLt := hi }).last ≥ i

hi: List.length (hd :: tl) - 1 - Nat.succ i < List.length (hd :: tl)

h_bound: Nat.succ i < List.length (hd :: tl)

Nat.succ i ≤ (List.get (hd :: tl) { val := List.length (hd :: tl) - 1 - Nat.succ i, isLt := hi }).lastlinarith
Goals accomplished! 🐙