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

/-!
Various lemmas about `pareto`.
-/

lemma pareto_head: ∀ {α : Type} {F : Factory α} {m m' : Meas} {ms : List Meas},
  pareto F (m :: m' :: ms) → m.last > m'.last ∧ Factory.lt F m.cost m'.cost
pareto_head (h: pareto F (m :: m' :: ms)
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.4
F (m: ?m.14
m :: m': ?m.24
m' :: ms: ?m.34
ms)) : 
    m: ?m.14
m.last: {α : Type} → Meas → ℕ
last > m': ?m.24
m'.last: {α : Type} → Meas → ℕ
last ∧ F: ?m.4
F.lt: {α : Type} → Factory α → α → α → Prop
lt m: ?m.14
m.cost: {α : Type} → Meas → α
cost m': ?m.24
m'.cost: {α : Type} → Meas → α
cost := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

m.last > m'.last ∧ Factory.lt F m.cost m'.costconstructorα✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

leftm.last > m'.last
α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

rightFactory.lt F m.cost m'.cost 
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

m.last > m'.last ∧ Factory.lt F m.cost m'.costcase left => α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

m.last > m'.lastexact last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head h: pareto F (m :: m' :: ms)
h.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

m.last > m'.last ∧ Factory.lt F m.cost m'.costcase right => α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

Factory.lt F m.cost m'.costexact 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: pareto F (m :: m' :: ms)
h.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙

lemma pareto_rest: ∀ {α : Type} {F : Factory α} {ms : List Meas} {m : Meas}, pareto F (m :: ms) → pareto F ms
pareto_rest {ms: List Meas
ms : List: Type ?u.144 → Type ?u.144
List Meas: {α : Type} → Type
Meas} {m: Meas
m : Meas: {α : Type} → Type
Meas} 
    (h: pareto F (m :: ms)
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.141
F (m: Meas
m :: ms: List Meas
ms)) : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.141
F ms: List Meas
ms := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

pareto F msconstructorα✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

leftlast_decreasing ms
α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

rightcost_increasing F ms
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

pareto F mscase left => α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

last_decreasing msexact last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest h: pareto F (m :: ms)
h.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

pareto F mscase right => α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F (m :: ms)

cost_increasing F msexact cost_increasing_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas}, cost_increasing F (x :: xs) → cost_increasing F xs
cost_increasing_rest h: pareto F (m :: ms)
h.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙

lemma pareto_drop: ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.drop n ms)
pareto_drop (n: ℕ
n : ℕ: Type
ℕ) (h: pareto F ms
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.234
F ms: ?m.243
ms) : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.234
F (ms: ?m.243
ms.drop: {α : Type ?u.254} → ℕ → List α → List α
drop n: ℕ
n) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.drop n ms)induction ms: List Meas
ms generalizing n: ℕ
nα✝: Type

F: Factory α✝

n: ℕ

h: pareto F []

nilpareto F (List.drop n [])
α✝: Type

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: ∀ (n : ℕ), pareto F tail✝ → pareto F (List.drop n tail✝)

n: ℕ

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

conspareto F (List.drop n (head✝ :: tail✝))
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.drop n ms)case nil => α✝: Type

F: Factory α✝

n: ℕ

h: pareto F []

pareto F (List.drop n [])simpa
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.drop n ms)case cons hd: ?m.292
hd tl: List ?m.292
tl ih: ?m.293 tl
ih => 
    α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

n: ℕ

h: pareto F (hd :: tl)

pareto F (List.drop n (hd :: tl))dwi { α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

n: ℕ

h: pareto F (hd :: tl)

pareto F (List.drop n (hd :: tl))cases n: ℕ
nα✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

h: pareto F (hd :: tl)

zeropareto F (List.drop Nat.zero (hd :: tl))
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

h: pareto F (hd :: tl)

n✝: ℕ

succpareto F (List.drop (Nat.succ n✝) (hd :: tl)) }α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

h: pareto F (hd :: tl)

n✝: ℕ

succpareto F (List.drop (Nat.succ n✝) (hd :: tl)) 
    α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

n: ℕ

h: pareto F (hd :: tl)

pareto F (List.drop n (hd :: tl))case succ n: ℕ
n => α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: ∀ (n : ℕ), pareto F tl → pareto F (List.drop n tl)

h: pareto F (hd :: tl)

n: ℕ

pareto F (List.drop (Nat.succ n) (hd :: tl))exact ih: ?m.293 tl
ih n: ℕ
n (pareto_rest: ∀ {α : Type} {F : Factory α} {ms : List Meas} {m : Meas}, pareto F (m :: ms) → pareto F ms
pareto_rest h: pareto F (hd :: tl)
h)
Goals accomplished! 🐙

lemma pareto_rest': ∀ {α : Type} {F : Factory α} {m m' : Meas} {ms : List Meas}, pareto F (m :: m' :: ms) → pareto F (m :: ms)
pareto_rest' (h: pareto F (m :: m' :: ms)
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.647
F (m: ?m.657
m :: m': ?m.667
m' :: ms: ?m.677
ms)) : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.647
F (m: ?m.657
m :: ms: ?m.677
ms) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

pareto F (m :: ms)simp [pareto: {α : Type} → Factory α → List Meas → Prop
pareto, cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing, last_decreasing: {α : Type} → List Meas → Prop
last_decreasing] at *α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

(∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
    (List.get ms { val := i, isLt := (_ : i < List.length ms) }).last <       (List.get (m :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
    Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
      (List.get ms { val := i, isLt := (_ : i < List.length ms) }).cost
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

pareto F (m :: ms)constructorα✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

left∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  (List.get ms { val := i, isLt := (_ : i < List.length ms) }).last < (List.get (m :: ms) { val := i, isLt := hi }).last
α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

right∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
    (List.get ms { val := i, isLt := (_ : i < List.length ms) }).cost
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

pareto F (m :: ms)case left => 
    α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  (List.get ms { val := i, isLt := (_ : i < List.length ms) }).last < (List.get (m :: ms) { val := i, isLt := hi }).lastintros i: ℕ
i hi: i < List.length (m :: ms)
hi hj: i + 1 < List.length (m :: ms)
hjα✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

i: ℕ

hi: i < List.length (m :: ms)

hj: i + 1 < List.length (m :: ms)

(List.get ms { val := i, isLt := (_ : i < List.length ms) }).last < (List.get (m :: ms) { val := i, isLt := hi }).last 
    α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  (List.get ms { val := i, isLt := (_ : i < List.length ms) }).last < (List.get (m :: ms) { val := i, isLt := hi }).lastcases ms: List Meas
msα✝: Type

F: Factory α✝

m, m': Meas

i: ℕ

h: (∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).last <       (List.get [m, m'] { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    Factory.lt F (List.get [m, m'] { val := i, isLt := hi }).cost
      (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).cost

hi: i < List.length [m]

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

nil(List.get [] { val := i, isLt := (_ : i < List.length []) }).last < (List.get [m] { val := i, isLt := hi }).last
α✝: Type

F: Factory α✝

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

cons(List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).last 
    α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  (List.get ms { val := i, isLt := (_ : i < List.length ms) }).last < (List.get (m :: ms) { val := i, isLt := hi }).lastcase nil => α✝: Type

F: Factory α✝

m, m': Meas

i: ℕ

h: (∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).last <       (List.get [m, m'] { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    Factory.lt F (List.get [m, m'] { val := i, isLt := hi }).cost
      (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).cost

hi: i < List.length [m]

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

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

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  (List.get ms { val := i, isLt := (_ : i < List.length ms) }).last < (List.get (m :: ms) { val := i, isLt := hi }).lastcase cons hd: Type
hd _ _ => 
      hd: Type

F: Factory hd

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).lastcases i: ℕ
ihd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

zero(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).last
hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

n✝: ℕ

hi: Nat.succ n✝ < List.length (m :: head✝ :: tail✝)

hj: Nat.succ n✝ + 1 < List.length (m :: head✝ :: tail✝)

succ(List.get (head✝ :: tail✝) { val := Nat.succ n✝, isLt := (_ : Nat.succ n✝ < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ n✝, isLt := hi }).last
      hd: Type

F: Factory hd

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).lastcase zero => 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lasthave h₁: ?m.11463
h₁ := h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost
h.left: ∀ {a b : Prop}, a ∧ b → a
left 0: ?m.11473
0 (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lastby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

0 < List.length (m :: m' :: head✝ :: tail✝)simp
Goals accomplished! 🐙) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lastby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

0 + 1 < List.length (m :: m' :: head✝ :: tail✝)simp
Goals accomplished! 🐙)hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).last
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lasthave h₂: ?m.11677
h₂ := h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost
h.left: ∀ {a b : Prop}, a ∧ b → a
left 1: ?m.11681
1 (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lastby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

1 < List.length (m :: m' :: head✝ :: tail✝)simp
Goals accomplished! 🐙) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lastby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

1 + 1 < List.length (m :: m' :: head✝ :: tail✝){hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

1 + 1 < List.length (m :: m' :: head✝ :: tail✝) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

1 + 1 < List.length (m :: m' :: head✝ :: tail✝)simp [Nat.succ_lt_succ: ∀ {n m : ℕ}, n < m → Nat.succ n < Nat.succ m
Nat.succ_lt_succ]
Goals accomplished! 🐙 }
Goals accomplished! 🐙)hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).last

h₂: (List.get (m' :: head✝ :: tail✝) { val := 1, isLt := (_ : 1 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝)
      { val := 1, isLt := (_ : 1 < Nat.succ (Nat.succ (List.length tail✝ + 1))) }).last

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).last
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lastsimp at h₁: ?m.11463
h₁ h₂: ?m.11677
h₂ ⊢hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: m'.last < m.last

h₂: head✝.last < m'.last

head✝.last < m.last 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).lastlinarith
Goals accomplished! 🐙
      hd: Type

F: Factory hd

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).lastcase succ i: ℕ
i => 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lastsimp at hi: Nat.succ i < List.length (m :: head✝ :: tail✝)
hi hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)
hjhd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).last 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lastrw [hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lastNat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_one,hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hi: i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hj: i + 1 + 1 < Nat.succ (Nat.succ (List.length tail✝))

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).last hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lastNat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_onehd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hi: i + 1 < List.length tail✝ + 1 + 1

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hj: i + 1 + 1 < List.length tail✝ + 1 + 1

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).last]hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hi: i + 1 < List.length tail✝ + 1 + 1

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hj: i + 1 + 1 < List.length tail✝ + 1 + 1

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).last at hi: i + 1 < Nat.succ (Nat.succ (List.length tail✝))
hi hj: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))
hjhd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hi: i + 1 < List.length tail✝ + 1 + 1

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hj: i + 1 + 1 < List.length tail✝ + 1 + 1

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).last
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lastsimp at hi: i + 1 < List.length tail✝ + 1 + 1
hi hj: i + 1 + 1 < List.length tail✝ + 1 + 1
hjhd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).last 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lasthave h': ?m.17013
h' := h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost
h.left: ∀ {a b : Prop}, a ∧ b → a
left (i: ℕ
i + 2: ?m.17028
2) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).lastby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝){hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝)simphd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)));hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝))) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝)rw [hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)))Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_onehd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length tail✝ + 2 + 1]hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length tail✝ + 2 + 1;hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length tail✝ + 2 + 1 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝)simpa
Goals accomplished! 🐙 }
Goals accomplished! 🐙) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).lastby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝){hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝)simphd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)));hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝))) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝)rw [hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)))Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_onehd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length tail✝ + 2 + 1]hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length tail✝ + 2 + 1;hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length tail✝ + 2 + 1 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝)simpa
Goals accomplished! 🐙 }
Goals accomplished! 🐙)hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

hi✝: Nat.succ i < Nat.succ (Nat.succ (List.length tail✝))

hj✝: Nat.succ i + 1 < Nat.succ (Nat.succ (List.length tail✝))

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

h': (List.get (m' :: head✝ :: tail✝) { val := i + 2, isLt := (_ : i + 2 < List.length (m' :: head✝ :: tail✝)) }).last <   (List.get (m :: m' :: head✝ :: tail✝)
      { val := i + 2, isLt := (_ : i + 2 < List.length (m :: m' :: head✝ :: tail✝)) }).last

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).last
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

(List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).last <   (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).lastsimpa
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: pareto F (m :: m' :: ms)

pareto F (m :: ms)case right =>
    α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
    (List.get ms { val := i, isLt := (_ : i < List.length ms) }).costintros i: ℕ
i hi: i < List.length (m :: ms)
hi hj: i + 1 < List.length (m :: ms)
hjα✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

i: ℕ

hi: i < List.length (m :: ms)

hj: i + 1 < List.length (m :: ms)

Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
  (List.get ms { val := i, isLt := (_ : i < List.length ms) }).cost 
    α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
    (List.get ms { val := i, isLt := (_ : i < List.length ms) }).costcases ms: List Meas
msα✝: Type

F: Factory α✝

m, m': Meas

i: ℕ

h: (∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).last <       (List.get [m, m'] { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    Factory.lt F (List.get [m, m'] { val := i, isLt := hi }).cost
      (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).cost

hi: i < List.length [m]

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

nilFactory.lt F (List.get [m] { val := i, isLt := hi }).cost
  (List.get [] { val := i, isLt := (_ : i < List.length []) }).cost
α✝: Type

F: Factory α✝

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

consFactory.lt F (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).cost 
    α✝: Type

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
    (List.get ms { val := i, isLt := (_ : i < List.length ms) }).costcase nil => α✝: Type

F: Factory α✝

m, m': Meas

i: ℕ

h: (∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).last <       (List.get [m, m'] { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length [m, m']) (hj : i + 1 < List.length [m, m']),
    Factory.lt F (List.get [m, m'] { val := i, isLt := hi }).cost
      (List.get [m'] { val := i, isLt := (_ : i < List.length [m']) }).cost

hi: i < List.length [m]

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

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

F: Factory α✝

m, m': Meas

ms: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).last <       (List.get (m :: m' :: ms) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: ms)) (hj : i + 1 < List.length (m :: m' :: ms)),
    Factory.lt F (List.get (m :: m' :: ms) { val := i, isLt := hi }).cost
      (List.get (m' :: ms) { val := i, isLt := (_ : i < List.length (m' :: ms)) }).cost

∀ (i : ℕ) (hi : i < List.length (m :: ms)) (hj : i + 1 < List.length (m :: ms)),
  Factory.lt F (List.get (m :: ms) { val := i, isLt := hi }).cost
    (List.get ms { val := i, isLt := (_ : i < List.length ms) }).costcase cons hd: Type
hd _ _ => 
      hd: Type

F: Factory hd

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).costcases i: ℕ
ihd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

zeroFactory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).cost
hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

n✝: ℕ

hi: Nat.succ n✝ < List.length (m :: head✝ :: tail✝)

hj: Nat.succ n✝ + 1 < List.length (m :: head✝ :: tail✝)

succFactory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ n✝, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ n✝, isLt := (_ : Nat.succ n✝ < List.length (head✝ :: tail✝)) }).cost
      hd: Type

F: Factory hd

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).costcase zero => 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costhave h₁: ?m.19502
h₁ := h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost
h.right: ∀ {a b : Prop}, a ∧ b → b
right 0: ?m.19512
0 (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

0 < List.length (m :: m' :: head✝ :: tail✝)simp
Goals accomplished! 🐙) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

0 + 1 < List.length (m :: m' :: head✝ :: tail✝)simp_arith
Goals accomplished! 🐙)hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).cost

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).cost
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costhave h₂: ?m.19987
h₂ := h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost
h.right: ∀ {a b : Prop}, a ∧ b → b
right 1: ?m.19999
1 (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).cost

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).cost

1 < List.length (m :: m' :: head✝ :: tail✝)simp
Goals accomplished! 🐙) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).cost

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).cost

1 + 1 < List.length (m :: m' :: head✝ :: tail✝)simp_arith
Goals accomplished! 🐙)hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < Nat.succ (List.length tail✝ + 2)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 0, isLt := (_ : 0 < List.length (m' :: head✝ :: tail✝)) }).cost

h₂: Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝)
      { val := 1, isLt := (_ : 1 < Nat.succ (Nat.succ (List.length tail✝ + 1))) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := 1, isLt := (_ : 1 < List.length (m' :: head✝ :: tail✝)) }).cost

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).cost
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costsimp at h₁: ?m.19502
h₁ h₂: ?m.19987
h₂ ⊢hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

Factory.lt F m.cost head✝.cost 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.zero, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.zero, isLt := (_ : Nat.zero < List.length (head✝ :: tail✝)) }).costapply Factory.lt_trans: ∀ {α : Type} {F : Factory α} {c₁ c₂ c₃ : α}, Factory.lt F c₁ c₂ → Factory.lt F c₂ c₃ → Factory.lt F c₁ c₃
Factory.lt_transhd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

h₁Factory.lt F m.cost ?c₂
hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

h₂Factory.lt F ?c₂ head✝.cost
hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

c₂hd hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

Factory.lt F m.cost head✝.cost<;>hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

h₁Factory.lt F m.cost ?c₂
hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

h₂Factory.lt F ?c₂ head✝.cost
hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

c₂hd hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: Nat.zero + 1 < List.length (m :: head✝ :: tail✝)

h₁: Factory.lt F m.cost m'.cost

h₂: Factory.lt F m'.cost head✝.cost

Factory.lt F m.cost head✝.costassumption
Goals accomplished! 🐙
      hd: Type

F: Factory hd

m, m': Meas

i: ℕ

head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

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

hj: i + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (head✝ :: tail✝)) }).costcase succ i: ℕ
i => 
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).costsimp [Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_one, Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_one] at hi: Nat.succ i < List.length (m :: head✝ :: tail✝)
hi hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)
hjhd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).cost
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).costhave h': ?m.22071
h' := h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost
h.right: ∀ {a b : Prop}, a ∧ b → b
right (i: ℕ
i + 2: ?m.22084
2) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).costby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝){hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝)simphd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)));hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝))) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝)rw [hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)))Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_onehd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length tail✝ + 2 + 1]hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length tail✝ + 2 + 1;hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length tail✝ + 2 + 1 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 < List.length (m :: m' :: head✝ :: tail✝)simpa
Goals accomplished! 🐙 }
Goals accomplished! 🐙) (hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).costby
Goals accomplished! 🐙 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝){hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝)simphd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)));hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝))) hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝)rw [hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < Nat.succ (Nat.succ (Nat.succ (List.length tail✝)))Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_onehd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length tail✝ + 2 + 1]hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length tail✝ + 2 + 1;hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length tail✝ + 2 + 1 hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

i + 2 + 1 < List.length (m :: m' :: head✝ :: tail✝)simpa
Goals accomplished! 🐙 }
Goals accomplished! 🐙)hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj✝: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

hi: i < List.length tail✝ + 1

hj: i < List.length tail✝

h': Factory.lt F
  (List.get (m :: m' :: head✝ :: tail✝)
      { val := i + 2, isLt := (_ : i + 2 < List.length (m :: m' :: head✝ :: tail✝)) }).cost
  (List.get (m' :: head✝ :: tail✝) { val := i + 2, isLt := (_ : i + 2 < List.length (m' :: head✝ :: tail✝)) }).cost

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi✝ }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).cost
        hd: Type

F: Factory hd

m, m', head✝: Meas

tail✝: List Meas

h: (∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).last <       (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).last) ∧   ∀ (i : ℕ) (hi : i < List.length (m :: m' :: head✝ :: tail✝)) (hj : i + 1 < List.length (m :: m' :: head✝ :: tail✝)),
    Factory.lt F (List.get (m :: m' :: head✝ :: tail✝) { val := i, isLt := hi }).cost
      (List.get (m' :: head✝ :: tail✝) { val := i, isLt := (_ : i < List.length (m' :: head✝ :: tail✝)) }).cost

i: ℕ

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

hj: Nat.succ i + 1 < List.length (m :: head✝ :: tail✝)

Factory.lt F (List.get (m :: head✝ :: tail✝) { val := Nat.succ i, isLt := hi }).cost
  (List.get (head✝ :: tail✝) { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (head✝ :: tail✝)) }).costsimpa
Goals accomplished! 🐙 

lemma pareto_one: ∀ {α : Type} {F : Factory α} (m : Meas), pareto F [m]
pareto_one (m: Meas
m : Meas: {α : Type} → Type
Meas) : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24127
F [m: Meas
m] := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

m: Meas

pareto F [m]simp [pareto: {α : Type} → Factory α → List Meas → Prop
pareto, cost_increasing_one: ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing F [x]
cost_increasing_one, last_decreasing_one: ∀ {α : Type} {x : Meas}, last_decreasing [x]
last_decreasing_one]
Goals accomplished! 🐙

lemma pareto_cons: ∀ {α : Type} {F : Factory α} (ms : List Meas) (x y : Meas),
  x.last > y.last → Factory.lt F x.cost y.cost → pareto F (y :: ms) → pareto F (x :: y :: ms)
pareto_cons (ms: List Meas
ms : List: Type ?u.24263 → Type ?u.24263
List Meas: {α : Type} → Type
Meas) (x: Meas
x y: Meas
y : 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_cost: sorryAx (Sort ?u.24255) true
h_cost : F: ?m.24260
FF.lt x.cost y.cost: Sort ?u.24255
.lt: {α : Type} → Factory α → α → α → Prop
ltF.lt x.cost y.cost: Sort ?u.24255
 x: Meas
xF.lt x.cost y.cost: Sort ?u.24255
.cost: {α : Type} → Meas → α
costF.lt x.cost y.cost: Sort ?u.24255
 y: Meas
yF.lt x.cost y.cost: Sort ?u.24255
.cost: {α : Type} → Meas → α
cost)
    (h: pareto F (y :: ms)
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24260
F (y: Meas
y :: ms: List Meas
ms)) : 
    pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24260
F (x: Meas
x :: y: Meas
y :: ms: List Meas
ms) := by
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: pareto F (y :: ms)

pareto F (x :: y :: ms)simp only [pareto: {α : Type} → Factory α → List Meas → Prop
pareto] at *α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

last_decreasing (x :: y :: ms) ∧ cost_increasing F (x :: y :: ms)
  α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: pareto F (y :: ms)

pareto F (x :: y :: ms)constructorα✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

leftlast_decreasing (x :: y :: ms)
α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

rightcost_increasing F (x :: y :: ms)
  α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: pareto F (y :: ms)

pareto F (x :: y :: ms)case left => 
    α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

last_decreasing (x :: y :: ms)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 α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

h_lastx.last > y.last
α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

hlast_decreasing (y :: ms) 
    α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

last_decreasing (x :: y :: ms)case h_last => α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

x.last > y.lastsimp [h_last: x.last > y.last
h_last]
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

last_decreasing (x :: y :: ms)case h => α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

last_decreasing (y :: ms)simp [h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)
h]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: pareto F (y :: ms)

pareto F (x :: y :: ms)case right =>
    α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

cost_increasing F (x :: y :: ms)apply 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α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

h_costFactory.lt F x.cost y.cost
α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

hcost_increasing F (y :: ms) 
    α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

cost_increasing F (x :: y :: ms)case h_cost => α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

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

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

cost_increasing F (x :: y :: ms)case h => α✝: Type

F: Factory α✝

ms: List Meas

x, y: Meas

h_last: x.last > y.last

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

h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)

cost_increasing F (y :: ms)simp [h: last_decreasing (y :: ms) ∧ cost_increasing F (y :: ms)
h]
Goals accomplished! 🐙

lemma pareto_concat: ∀ {α : Type} {F : Factory α} {ms : List Meas} (m : Meas),
  pareto F ms → pareto F (dedup F (List.map (fun m' => Meas.concat F m m') ms))
pareto_concat (m: Meas
m : Meas: {α : Type} → Type
Meas) (h: pareto F ms
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24626
F ms: ?m.24636
ms) : 
    pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24626
F (dedup: {α : Type} → Factory α → List Meas → List Meas
dedup F: ?m.24626
F (ms: ?m.24636
ms.map: {α : Type ?u.24652} → {β : Type ?u.24651} → (α → β) → List α → List β
map (fun m': ?m.24660
m' => Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: ?m.24626
F m: Meas
m m': ?m.24660
m'))) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F ms

pareto F (dedup F (List.map (fun m' => Meas.concat F m m') ms))simp only [pareto: {α : Type} → Factory α → List Meas → Prop
pareto] at *α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

last_decreasing (dedup F (List.map (fun m' => Meas.concat F m m') ms)) ∧   cost_increasing F (dedup F (List.map (fun m' => Meas.concat F m m') ms)) 
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

last_decreasing (dedup F (List.map (fun m' => Meas.concat F m m') ms))apply dedup_last_decreasing: ∀ {α : Type} {ms : List Meas} {F : Factory α}, last_decreasing ms → last_decreasing (dedup F ms)
dedup_last_decreasingα✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

last_decreasing (dedup F (List.map (fun m' => Meas.concat F m m') ms))apply 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α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

h.hlast_decreasing ms
    α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

last_decreasing (dedup F (List.map (fun m' => Meas.concat F m m') ms))apply h: last_decreasing ms ∧ cost_increasing F ms
h.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: pareto F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

cost_increasing F (dedup F (List.map (fun m' => Meas.concat F m m') ms))apply dedup_cost_increasing: ∀ {α : Type} {F : Factory α} {ms : List Meas}, cost_increasing_non_strict F ms → cost_increasing F (dedup F ms)
dedup_cost_increasingα✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

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

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

cost_increasing F (dedup F (List.map (fun m' => Meas.concat F m m') ms))apply 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α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

h.hcost_increasing F ms
    α✝: Type

F: Factory α✝

ms: List Meas

m: Meas

h: last_decreasing ms ∧ cost_increasing F ms

cost_increasing F (dedup F (List.map (fun m' => Meas.concat F m m') ms))apply h: last_decreasing ms ∧ cost_increasing F ms
h.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙

lemma pareto_map_lift_align: ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.map (Meas.adjust_align n) ms)
pareto_map_lift_align (n: ℕ
n : ℕ: Type
ℕ) (h: pareto F ms
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24879
F ms: ?m.24888
ms) : 
    pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.24879
F (ms: ?m.24888
ms.map: {α : Type ?u.24900} → {β : Type ?u.24899} → (α → β) → List α → List β
map (Meas.adjust_align: {α : Type} → ℕ → Meas → Meas
Meas.adjust_align n: ℕ
n)) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

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

F: Factory α✝

n: ℕ

h: pareto F []

nilpareto F (List.map (Meas.adjust_align n) [])
α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tail✝: List Meas

tail_ih✝: pareto F tail✝ → pareto F (List.map (Meas.adjust_align n) tail✝)

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

conspareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.map (Meas.adjust_align n) ms)case nil => α✝: Type

F: Factory α✝

n: ℕ

h: pareto F []

pareto F (List.map (Meas.adjust_align n) [])simpa
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.map (Meas.adjust_align n) ms)case cons tl: List ?m.24948
tl ih: ?m.24949 tl
ih => 
    α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tl: List Meas

ih: pareto F tl → pareto F (List.map (Meas.adjust_align n) tl)

h: pareto F (head✝ :: tl)

pareto F (List.map (Meas.adjust_align n) (head✝ :: tl))cases tl: List ?m.24948
tlα✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

ih: pareto F [] → pareto F (List.map (Meas.adjust_align n) [])

h: pareto F [head✝]

nilpareto F (List.map (Meas.adjust_align n) [head✝])
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

conspareto F (List.map (Meas.adjust_align n) (head✝¹ :: head✝ :: tail✝))
    α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tl: List Meas

ih: pareto F tl → pareto F (List.map (Meas.adjust_align n) tl)

h: pareto F (head✝ :: tl)

pareto F (List.map (Meas.adjust_align n) (head✝ :: tl))case nil => α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

ih: pareto F [] → pareto F (List.map (Meas.adjust_align n) [])

h: pareto F [head✝]

pareto F (List.map (Meas.adjust_align n) [head✝])apply pareto_one: ∀ {α : Type} {F : Factory α} (m : Meas), pareto F [m]
pareto_one
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tl: List Meas

ih: pareto F tl → pareto F (List.map (Meas.adjust_align n) tl)

h: pareto F (head✝ :: tl)

pareto F (List.map (Meas.adjust_align n) (head✝ :: tl))case cons => 
      α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_align n) (head✝¹ :: head✝ :: tail✝))dwi { α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_align n) (head✝¹ :: head✝ :: tail✝))apply pareto_cons: ∀ {α : Type} {F : Factory α} (ms : List Meas) (x y : Meas),
  x.last > y.last → Factory.lt F x.cost y.cost → pareto F (y :: ms) → pareto F (x :: y :: ms)
pareto_consα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_last(Meas.adjust_align n head✝¹).last > (Meas.adjust_align n head✝).last
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_costFactory.lt F (Meas.adjust_align n head✝¹).cost (Meas.adjust_align n head✝).cost
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

hpareto F (Meas.adjust_align n head✝ :: List.map (Meas.adjust_align n) tail✝) }α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_last(Meas.adjust_align n head✝¹).last > (Meas.adjust_align n head✝).last
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_costFactory.lt F (Meas.adjust_align n head✝¹).cost (Meas.adjust_align n head✝).cost
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

hpareto F (Meas.adjust_align n head✝ :: List.map (Meas.adjust_align n) tail✝) 
      α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_align n) (head✝¹ :: head✝ :: tail✝))case h => 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (Meas.adjust_align n head✝ :: List.map (Meas.adjust_align n) tail✝)apply ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))
ihα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (head✝ :: tail✝)
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (Meas.adjust_align n head✝ :: List.map (Meas.adjust_align n) tail✝)apply pareto_rest: ∀ {α : Type} {F : Factory α} {ms : List Meas} {m : Meas}, pareto F (m :: ms) → pareto F ms
pareto_restα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

hpareto F (?m :: head✝ :: tail✝)
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

mMeas 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (Meas.adjust_align n head✝ :: List.map (Meas.adjust_align n) tail✝)assumption
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_align n) (head✝¹ :: head✝ :: tail✝))case h_last | h_cost => 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

Factory.lt F (Meas.adjust_align n head✝¹).cost (Meas.adjust_align n head✝).costreplace h: ?m.25418
h := pareto_head: ∀ {α : Type} {F : Factory α} {m m' : Meas} {ms : List Meas},
  pareto F (m :: m' :: ms) → m.last > m'.last ∧ Factory.lt F m.cost m'.cost
pareto_head h: pareto F (head✝¹ :: head✝ :: tail✝)
hα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: head✝¹.last > head✝.last ∧ Factory.lt F head✝¹.cost head✝.cost

(Meas.adjust_align n head✝¹).last > (Meas.adjust_align n head✝).last 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_align n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

(Meas.adjust_align n head✝¹).last > (Meas.adjust_align n head✝).lastsimp [Meas.adjust_align: {α : Type} → ℕ → Meas → Meas
Meas.adjust_align, h: ?m.25418
h]
Goals accomplished! 🐙

lemma pareto_map_lift_nest: ∀ {α : Type} {F : Factory α} {ms : List Meas} (n : ℕ), pareto F ms → pareto F (List.map (Meas.adjust_nest n) ms)
pareto_map_lift_nest (n: ℕ
n : ℕ: Type
ℕ) (h: pareto F ms
h : pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.27789
F ms: ?m.27798
ms) : 
    pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.27789
F (ms: ?m.27798
ms.map: {α : Type ?u.27810} → {β : Type ?u.27809} → (α → β) → List α → List β
map (Meas.adjust_nest: {α : Type} → ℕ → Meas → Meas
Meas.adjust_nest n: ℕ
n)) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

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

F: Factory α✝

n: ℕ

h: pareto F []

nilpareto F (List.map (Meas.adjust_nest n) [])
α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tail✝: List Meas

tail_ih✝: pareto F tail✝ → pareto F (List.map (Meas.adjust_nest n) tail✝)

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

conspareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.map (Meas.adjust_nest n) ms)case nil => α✝: Type

F: Factory α✝

n: ℕ

h: pareto F []

pareto F (List.map (Meas.adjust_nest n) [])simpa
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

n: ℕ

h: pareto F ms

pareto F (List.map (Meas.adjust_nest n) ms)case cons tl: List ?m.27858
tl ih: ?m.27859 tl
ih => 
    α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tl: List Meas

ih: pareto F tl → pareto F (List.map (Meas.adjust_nest n) tl)

h: pareto F (head✝ :: tl)

pareto F (List.map (Meas.adjust_nest n) (head✝ :: tl))cases tl: List ?m.27858
tlα✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

ih: pareto F [] → pareto F (List.map (Meas.adjust_nest n) [])

h: pareto F [head✝]

nilpareto F (List.map (Meas.adjust_nest n) [head✝])
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

conspareto F (List.map (Meas.adjust_nest n) (head✝¹ :: head✝ :: tail✝))
    α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tl: List Meas

ih: pareto F tl → pareto F (List.map (Meas.adjust_nest n) tl)

h: pareto F (head✝ :: tl)

pareto F (List.map (Meas.adjust_nest n) (head✝ :: tl))case nil => α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

ih: pareto F [] → pareto F (List.map (Meas.adjust_nest n) [])

h: pareto F [head✝]

pareto F (List.map (Meas.adjust_nest n) [head✝])apply pareto_one: ∀ {α : Type} {F : Factory α} (m : Meas), pareto F [m]
pareto_one
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

n: ℕ

head✝: Meas

tl: List Meas

ih: pareto F tl → pareto F (List.map (Meas.adjust_nest n) tl)

h: pareto F (head✝ :: tl)

pareto F (List.map (Meas.adjust_nest n) (head✝ :: tl))case cons => 
      α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_nest n) (head✝¹ :: head✝ :: tail✝))dwi { α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_nest n) (head✝¹ :: head✝ :: tail✝))apply pareto_cons: ∀ {α : Type} {F : Factory α} (ms : List Meas) (x y : Meas),
  x.last > y.last → Factory.lt F x.cost y.cost → pareto F (y :: ms) → pareto F (x :: y :: ms)
pareto_consα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_last(Meas.adjust_nest n head✝¹).last > (Meas.adjust_nest n head✝).last
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_costFactory.lt F (Meas.adjust_nest n head✝¹).cost (Meas.adjust_nest n head✝).cost
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

hpareto F (Meas.adjust_nest n head✝ :: List.map (Meas.adjust_nest n) tail✝) }α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_last(Meas.adjust_nest n head✝¹).last > (Meas.adjust_nest n head✝).last
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

h_costFactory.lt F (Meas.adjust_nest n head✝¹).cost (Meas.adjust_nest n head✝).cost
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

hpareto F (Meas.adjust_nest n head✝ :: List.map (Meas.adjust_nest n) tail✝) 
      α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_nest n) (head✝¹ :: head✝ :: tail✝))case h => 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (Meas.adjust_nest n head✝ :: List.map (Meas.adjust_nest n) tail✝)apply ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))
ihα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (head✝ :: tail✝)
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (Meas.adjust_nest n head✝ :: List.map (Meas.adjust_nest n) tail✝)apply pareto_rest: ∀ {α : Type} {F : Factory α} {ms : List Meas} {m : Meas}, pareto F (m :: ms) → pareto F ms
pareto_restα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

hpareto F (?m :: head✝ :: tail✝)
α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

mMeas 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (Meas.adjust_nest n head✝ :: List.map (Meas.adjust_nest n) tail✝)assumption
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

pareto F (List.map (Meas.adjust_nest n) (head✝¹ :: head✝ :: tail✝))case h_last | h_cost => 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

(Meas.adjust_nest n head✝¹).last > (Meas.adjust_nest n head✝).lastreplace h: ?m.28328
h := pareto_head: ∀ {α : Type} {F : Factory α} {m m' : Meas} {ms : List Meas},
  pareto F (m :: m' :: ms) → m.last > m'.last ∧ Factory.lt F m.cost m'.cost
pareto_head h: pareto F (head✝¹ :: head✝ :: tail✝)
hα✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: head✝¹.last > head✝.last ∧ Factory.lt F head✝¹.cost head✝.cost

Factory.lt F (Meas.adjust_nest n head✝¹).cost (Meas.adjust_nest n head✝).cost 
        α✝: Type

F: Factory α✝

n: ℕ

head✝¹, head✝: Meas

tail✝: List Meas

ih: pareto F (head✝ :: tail✝) → pareto F (List.map (Meas.adjust_nest n) (head✝ :: tail✝))

h: pareto F (head✝¹ :: head✝ :: tail✝)

Factory.lt F (Meas.adjust_nest n head✝¹).cost (Meas.adjust_nest n head✝).costsimp [Meas.adjust_nest: {α : Type} → ℕ → Meas → Meas
Meas.adjust_nest, h: ?m.28328
h]
Goals accomplished! 🐙