import Pretty.Supports.Pareto

/-!
## Equivalence of Pareto frontier definitions
-/

/--
The traditional definition of Pareto frontier based on non-domination
-/
def pareto_nondom: {α : Type} → Factory α → List Meas → Prop
pareto_nondom (F: Factory α
F : Factory: Type → Type
Factory α: ?m.3
α) (ms: List Meas
ms : List: Type ?u.8 → Type ?u.8
List (@Meas: {α : Type} → Type
Meas α: ?m.3
α)) : Prop: Type
Prop := 
  ∀ (i: ℕ
i j: ℕ
j : ℕ: Type
ℕ) (h_i: i < List.length ms
h_i : i: ℕ
i < ms: List Meas
ms.length: {α : Type ?u.21} → List α → ℕ
length) (h_j: j < List.length ms
h_j : j: ℕ
j < ms: List Meas
ms.length: {α : Type ?u.34} → List α → ℕ
length), 
    i: ℕ
i ≠ j: ℕ
j → 
    (¬ dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F (ms: List Meas
ms.get: {α : Type ?u.48} → (as : List α) → Fin (List.length as) → α
get ⟨i: ℕ
i, by
Goals accomplished! 🐙 α: Type

F: Factory α

ms: List Meas

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

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

F: Factory α

ms: List Meas

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

j < List.length msassumption
Goals accomplished! 🐙⟩) ∧  
       ¬ dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F (ms: List Meas
ms.get: {α : Type ?u.150} → (as : List α) → Fin (List.length as) → α
get ⟨j: ℕ
j, by
Goals accomplished! 🐙 α: Type

F: Factory α

ms: List Meas

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

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

F: Factory α

ms: List Meas

i, j: ℕ

h_i: i < List.length ms

h_j: j < List.length ms

i < List.length msassumption
Goals accomplished! 🐙⟩))

/--
Our formalized definition of Pareto frontier is equivalent to the one in the paper based on non-domination.
-/
theorem pareto_nondom_iff_pareto: ∀ {α : Type} {F : Factory α} {ms : List Meas}, pareto F ms ↔ pareto_nondom F ms ∧ last_decreasing ms
pareto_nondom_iff_pareto : 
    pareto: {α : Type} → Factory α → List Meas → Prop
pareto F: ?m.262
F ms: ?m.269
ms ↔ (pareto_nondom: {α : Type} → Factory α → List Meas → Prop
pareto_nondom F: ?m.262
F ms: ?m.269
ms ∧ last_decreasing: {α : Type} → List Meas → Prop
last_decreasing ms: ?m.269
ms) := by
Goals accomplished! 🐙 
  α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms ↔ pareto_nondom F ms ∧ last_decreasing msapply Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.introα✝: Type

F: Factory α✝

ms: List Meas

mppareto F ms → pareto_nondom F ms ∧ last_decreasing ms
α✝: Type

F: Factory α✝

ms: List Meas

mprpareto_nondom F ms ∧ last_decreasing ms → pareto F ms
  α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms ↔ pareto_nondom F ms ∧ last_decreasing mscase mp => 
    α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms → pareto_nondom F ms ∧ last_decreasing msintro h: ?a
hα✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F ms ∧ last_decreasing ms
    α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms → pareto_nondom F ms ∧ last_decreasing msapply And.intro: ∀ {a b : Prop}, a → b → a ∧ b
And.introα✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

leftpareto_nondom F ms
α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

rightlast_decreasing ms 
    α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms → pareto_nondom F ms ∧ last_decreasing mscase left => 
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mssimp [pareto_nondom: {α : Type} → Factory α → List Meas → Prop
pareto_nondom]α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  ¬i = j →
    dominates F (List.get ms { val := i, isLt := h_i }) (List.get ms { val := j, isLt := h_j }) = false ∧       dominates F (List.get ms { val := j, isLt := h_j }) (List.get ms { val := i, isLt := h_i }) = false
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F msintro i: ℕ
i j: ℕ
j hi: i < List.length ms
hi hj: j < List.length ms
hj h_neq: ¬i = j
h_neqα✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

dominates F (List.get ms { val := i, isLt := hi }) (List.get ms { val := j, isLt := hj }) = false ∧   dominates F (List.get ms { val := j, isLt := hj }) (List.get ms { val := i, isLt := hi }) = false 
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mssimp only [pareto: {α : Type} → Factory α → List Meas → Prop
pareto] at h: ?a
hα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

dominates F (List.get ms { val := i, isLt := hi }) (List.get ms { val := j, isLt := hj }) = false ∧   dominates F (List.get ms { val := j, isLt := hj }) (List.get ms { val := i, isLt := hi }) = false
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F msreplace h_last: ?m.4463
h_last := last_decreasing_strong: ∀ {α : Type} {ms : List Meas},
  last_decreasing ms →
    ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
      i < j → (List.get ms { val := i, isLt := h_i }).last > (List.get ms { val := j, isLt := h_j }).last
last_decreasing_strong h: last_decreasing ms ∧ cost_increasing F ms
h.left: ∀ {a b : Prop}, a ∧ b → a
leftα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

dominates F (List.get ms { val := i, isLt := hi }) (List.get ms { val := j, isLt := hj }) = false ∧   dominates F (List.get ms { val := j, isLt := hj }) (List.get ms { val := i, isLt := hi }) = false 
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F msreplace h_cost: ?m.4517
h_cost := cost_increasing_strong: ∀ {α : Type} {F : Factory α} {ms : List Meas},
  cost_increasing F ms →
    ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
      i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost
cost_increasing_strong h: last_decreasing ms ∧ cost_increasing F ms
h.right: ∀ {a b : Prop}, a ∧ b → b
rightα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

dominates F (List.get ms { val := i, isLt := hi }) (List.get ms { val := j, isLt := hj }) = false ∧   dominates F (List.get ms { val := j, isLt := hj }) (List.get ms { val := i, isLt := hi }) = false
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mssimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false) 
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mshave h_tri: ?m.5356
h_tri := Nat.lt_trichotomy: ∀ (a b : ℕ), a < b ∨ a = b ∨ b < a
Nat.lt_trichotomy i: ℕ
i j: ℕ
jα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j ∨ i = j ∨ j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false) 
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mscases h_tri: ?m.5356
h_triα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h✝: i < j

inl((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)
α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h✝: i = j ∨ j < i

inr((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false) 
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mscase inl h_tri: ?m.5377
h_tri => 
        α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)specialize h_cost: ?m.4517
h_cost i: ℕ
i j: ℕ
j hi: i < List.length ms
hi hj: j < List.length ms
hj h_tri: ?m.5377
h_triα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

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

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)
        α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)simp [h_last: ?m.4463
h_last i: ℕ
i j: ℕ
j hi: i < List.length ms
hi hj: j < List.length ms
hj h_tri: ?m.5377
h_tri]α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

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

(List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨   Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false
        α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)rightα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

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

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)rw [α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

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

hFactory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false← F: Factory α✝
F.not_le_iff_lt: ∀ {α : Type} {F : Factory α} {c₁ c₂ : α}, ¬Factory.le F c₁ c₂ = true ↔ Factory.lt F c₂ c₁
not_le_iff_ltα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

h_cost: ¬Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = true

hFactory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false]α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

h_cost: ¬Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = true

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

h_cost: ¬Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = true

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)simp at h_cost: ¬Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = true
h_costα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: i < j

h_cost: Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i < j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)assumption
Goals accomplished! 🐙
      α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

pareto_nondom F mscase inr h_tri: ?m.5378
h_tri => 
        α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i = j ∨ j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)cases h_tri: ?m.5378
h_triα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h✝: i = j

inl((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)
α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h✝: j < i

inr((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)
        α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i = j ∨ j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)case inl h_tri: ?m.5724
h_tri => 
          α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i = j

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)simp [h_neq: ¬i = j
h_neq] at h_tri: ?m.5724
h_tri
Goals accomplished! 🐙
        α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: i = j ∨ j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)case inr h_tri: ?m.5725
h_tri => 
          α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)specialize h_cost: ?m.4517
h_cost j: ℕ
j i: ℕ
i hj: j < List.length ms
hj hi: i < List.length ms
hi h_tri: ?m.5725
h_triα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

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

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)
          α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)simp [h_last: ?m.4463
h_last j: ℕ
j i: ℕ
i hj: j < List.length ms
hj hi: i < List.length ms
hi h_tri: ?m.5725
h_tri]α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

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

(List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨   Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false
          α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)rightα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

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

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)rw [α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

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

hFactory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false← F: Factory α✝
F.not_le_iff_lt: ∀ {α : Type} {F : Factory α} {c₁ c₂ : α}, ¬Factory.le F c₁ c₂ = true ↔ Factory.lt F c₂ c₁
not_le_iff_ltα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

h_cost: ¬Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = true

hFactory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false]α✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

h_cost: ¬Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = true

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

h_cost: ¬Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = true

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)simp at h_cost: ¬Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = true
h_costα✝: Type

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_tri: j < i

h_cost: Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false

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

F: Factory α✝

ms: List Meas

h: last_decreasing ms ∧ cost_increasing F ms

i, j: ℕ

hi: i < List.length ms

hj: j < List.length ms

h_neq: ¬i = j

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

h_cost: ∀ (i j : ℕ) (h_i : i < List.length ms) (h_j : j < List.length ms),
  i < j → Factory.lt F (List.get ms { val := i, isLt := h_i }).cost (List.get ms { val := j, isLt := h_j }).cost

h_tri: j < i

((List.get ms { val := j, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last ∨     Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := j, isLt := hj }).cost = false) ∧   ((List.get ms { val := i, isLt := hi }).last < (List.get ms { val := j, isLt := hj }).last ∨     Factory.le F (List.get ms { val := j, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)assumption
Goals accomplished! 🐙
    α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms → pareto_nondom F ms ∧ last_decreasing mscase right => α✝: Type

F: Factory α✝

ms: List Meas

h: pareto F ms

last_decreasing mssimp [h: ?a
h.left: ∀ {a b : Prop}, a ∧ b → a
left]
Goals accomplished! 🐙
  α✝: Type

F: Factory α✝

ms: List Meas

pareto F ms ↔ pareto_nondom F ms ∧ last_decreasing mscase mpr => 
    α✝: Type

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msrintro ⟨h_pareto, h_last⟩: ?b
⟨h_pareto: pareto_nondom F ms
h_pareto⟨h_pareto, h_last⟩: ?b
, h_last: last_decreasing ms
h_last⟨h_pareto, h_last⟩: ?b
⟩α✝: Type

F: Factory α✝

ms: List Meas

h_pareto: pareto_nondom F ms

h_last: last_decreasing ms

intropareto F ms
    α✝: Type

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F mssimp [pareto: {α : Type} → Factory α → List Meas → Prop
pareto, h_last: last_decreasing ms
h_last, cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing]α✝: Type

F: Factory α✝

ms: List Meas

h_pareto: pareto_nondom F ms

h_last: last_decreasing ms

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msintro i: ℕ
i hi: i < List.length ms
hi hj: i + 1 < List.length ms
hjα✝: Type

F: Factory α✝

ms: List Meas

h_pareto: pareto_nondom F ms

h_last: last_decreasing ms

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msspecialize h_last: last_decreasing ms
h_last i: ℕ
i hi: i < List.length ms
hi hj: i + 1 < List.length ms
hjα✝: Type

F: Factory α✝

ms: List Meas

h_pareto: pareto_nondom F ms

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msspecialize h_pareto: pareto_nondom F ms
h_pareto i: ℕ
i (i: ℕ
i + 1: ?m.7391
1) hi: i < List.length ms
hi hj: i + 1 < List.length ms
hj (α✝: Type

F: Factory α✝

ms: List Meas

h_pareto: pareto_nondom F ms

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

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

F: Factory α✝

ms: List Meas

h_pareto: pareto_nondom F ms

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

i ≠ i + 1simp
Goals accomplished! 🐙)α✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

h_pareto: ¬dominates F (List.get ms { val := i, isLt := hi }) (List.get ms { val := i + 1, isLt := hj }) = true ∧   ¬dominates F (List.get ms { val := i + 1, isLt := hj }) (List.get ms { val := i, isLt := hi }) = true

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F mssimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates] at h_pareto: ¬dominates F (List.get ms { val := i, isLt := hi }) (List.get ms { val := i + 1, isLt := hj }) = true ∧   ¬dominates F (List.get ms { val := i + 1, isLt := hj }) (List.get ms { val := i, isLt := hi }) = true
h_paretoα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

h_pareto: ((List.get ms { val := i, isLt := hi }).last ≤ (List.get ms { val := i + 1, isLt := hj }).last →
    Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := i + 1, isLt := hj }).cost = false) ∧   ((List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last →
    Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msreplace h_pareto: ?m.9243
h_pareto := h_pareto: ((List.get ms { val := i, isLt := hi }).last ≤ (List.get ms { val := i + 1, isLt := hj }).last →
    Factory.le F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := i + 1, isLt := hj }).cost = false) ∧   ((List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last →
    Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false)
h_pareto.right: ∀ {a b : Prop}, a ∧ b → b
rightα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last

h_pareto: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last →
  Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F mssimp at h_last: (List.get ms { val := i, isLt := hi }).last > (List.get ms { val := i + 1, isLt := hj }).last
h_lastα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_pareto: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last →
  Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

h_last: (List.get ms { val := i + 1, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msreplace h_last: ?m.9408
h_last := Nat.le_of_lt: ∀ {n m : ℕ}, n < m → n ≤ m
Nat.le_of_lt h_last: (List.get ms { val := i + 1, isLt := hj }).last < (List.get ms { val := i, isLt := hi }).last
h_lastα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_pareto: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last →
  Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

h_last: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msspecialize h_pareto: ?m.9243
h_pareto h_last: ?m.9408
h_lastα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last

h_pareto: Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

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

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msrw [α✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last

h_pareto: Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

introFactory.lt F (List.get ms { val := i, isLt := hi }).cost (List.get ms { val := i + 1, isLt := hj }).cost← F: Factory α✝
F.not_le_iff_lt: ∀ {α : Type} {F : Factory α} {c₁ c₂ : α}, ¬Factory.le F c₁ c₂ = true ↔ Factory.lt F c₂ c₁
not_le_iff_ltα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last

h_pareto: Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

intro¬Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = true]α✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last

h_pareto: Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

intro¬Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = true
    α✝: Type

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F mssimpα✝: Type

F: Factory α✝

ms: List Meas

i: ℕ

hi: i < List.length ms

hj: i + 1 < List.length ms

h_last: (List.get ms { val := i + 1, isLt := hj }).last ≤ (List.get ms { val := i, isLt := hi }).last

h_pareto: Factory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false

introFactory.le F (List.get ms { val := i + 1, isLt := hj }).cost (List.get ms { val := i, isLt := hi }).cost = false
    α✝: Type

F: Factory α✝

ms: List Meas

pareto_nondom F ms ∧ last_decreasing ms → pareto F msassumption
Goals accomplished! 🐙