import Pretty.Supports.LastAndCost

/-! 
## Various lemmas related to the `dedup` operation
-/

lemma 
dedup_not_empty: ∀ {α : Type} {ms : List Meas} {F : Factory α}, ms ≠ [] → dedup F ms ≠ []
dedup_not_empty (
h: ms ≠ []
h : 
ms: ?m.5
ms ≠ 
[]: unknown metavariable '?_uniq.11'
[]) : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.20
F 
ms: ?m.5
ms ≠ 
[]: List ?m.39
[] := by
Goals accomplished! 🐙 
  
α✝: Type

ms: List Meas

F: Factory α✝

h: ms ≠ []

dedup F ms ≠ []induction 
ms: List Meas
ms
α✝: Type

F: Factory α✝

h: [] ≠ []

nil
dedup F [] ≠ []
α✝: Type

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: tail✝ ≠ [] → dedup F tail✝ ≠ []

h: head✝ :: tail✝ ≠ []

cons
dedup F (head✝ :: tail✝) ≠ [] 
  
α✝: Type

ms: List Meas

F: Factory α✝

h: ms ≠ []

dedup F ms ≠ []case nil => 
α✝: Type

F: Factory α✝

h: [] ≠ []

dedup F [] ≠ []contradiction
Goals accomplished! 🐙
  
α✝: Type

ms: List Meas

F: Factory α✝

h: ms ≠ []

dedup F ms ≠ []case cons 
hd: ?m.71
hd 
tl: List ?m.71
tl 
ih: ?m.72 tl
ih => 
    
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: tl ≠ [] → dedup F tl ≠ []

h: hd :: tl ≠ []

dedup F (hd :: tl) ≠ []cases 
tl: List ?m.71
tl
α✝: Type

F: Factory α✝

hd: Meas

ih: [] ≠ [] → dedup F [] ≠ []

h: [hd] ≠ []

nil
dedup F [hd] ≠ []
α✝: Type

F: Factory α✝

hd, head✝: Meas

tail✝: List Meas

ih: head✝ :: tail✝ ≠ [] → dedup F (head✝ :: tail✝) ≠ []

h: hd :: head✝ :: tail✝ ≠ []

cons
dedup F (hd :: head✝ :: tail✝) ≠ [] 
    
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: tl ≠ [] → dedup F tl ≠ []

h: hd :: tl ≠ []

dedup F (hd :: tl) ≠ []case nil => 
α✝: Type

F: Factory α✝

hd: Meas

ih: [] ≠ [] → dedup F [] ≠ []

h: [hd] ≠ []

dedup F [hd] ≠ []simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

hd: Meas

tl: List Meas

ih: tl ≠ [] → dedup F tl ≠ []

h: hd :: tl ≠ []

dedup F (hd :: tl) ≠ []case cons 
hd': ?m.109
hd' 
tl': List ?m.109
tl' => 
      
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

dedup F (hd :: hd' :: tl') ≠ []simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

¬(if Factory.le F hd'.cost hd.cost = true then dedup F (hd' :: tl') else hd :: dedup F (hd' :: tl')) = []
      
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

dedup F (hd :: hd' :: tl') ≠ []split_ifs
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

h✝: Factory.le F hd'.cost hd.cost = true

inl
¬dedup F (hd' :: tl') = []
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

h✝: ¬Factory.le F hd'.cost hd.cost = true

inr
¬False
      
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

dedup F (hd :: hd' :: tl') ≠ []case inl => 
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

h✝: Factory.le F hd'.cost hd.cost = true

¬dedup F (hd' :: tl') = []simp [
ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []
ih]
Goals accomplished! 🐙
      
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

dedup F (hd :: hd' :: tl') ≠ []case inr => 
α✝: Type

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: hd' :: tl' ≠ [] → dedup F (hd' :: tl') ≠ []

h: hd :: hd' :: tl' ≠ []

h✝: ¬Factory.le F hd'.cost hd.cost = true

¬Falsesimp
Goals accomplished! 🐙

lemma 
dedup_member: ∀ {α : Type} {m : Meas} {F : Factory α} {ms : List Meas}, m ∈ dedup F ms → m ∈ ms
dedup_member (
h: m ∈ dedup F ms
h : 
m: ?m.1678
m ∈ 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.1698
F 
ms: ?m.1720
ms) : 
m: ?m.1678
m ∈ 
ms: ?m.1720
ms := by
Goals accomplished! 🐙 
  
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

h: m ∈ dedup F ms

m ∈ msinduction 
ms: List Meas
ms
α✝: Type

m: Meas

F: Factory α✝

h: m ∈ dedup F []

nil
m ∈ []
α✝: Type

m: Meas

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: m ∈ dedup F tail✝ → m ∈ tail✝

h: m ∈ dedup F (head✝ :: tail✝)

cons
m ∈ head✝ :: tail✝ 
  
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

h: m ∈ dedup F ms

m ∈ mscase nil => 
α✝: Type

m: Meas

F: Factory α✝

h: m ∈ dedup F []

m ∈ []simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: m ∈ dedup F []
h
Goals accomplished! 🐙
  
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

h: m ∈ dedup F ms

m ∈ mscase cons 
hd: ?m.1809
hd 
tl: List ?m.1809
tl 
ih: ?m.1810 tl
ih => 
    
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

tl: List Meas

ih: m ∈ dedup F tl → m ∈ tl

h: m ∈ dedup F (hd :: tl)

m ∈ hd :: tlcases 
tl: List ?m.1809
tl
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

ih: m ∈ dedup F [] → m ∈ []

h: m ∈ dedup F [hd]

nil
m ∈ [hd]
α✝: Type

m: Meas

F: Factory α✝

hd, head✝: Meas

tail✝: List Meas

ih: m ∈ dedup F (head✝ :: tail✝) → m ∈ head✝ :: tail✝

h: m ∈ dedup F (hd :: head✝ :: tail✝)

cons
m ∈ hd :: head✝ :: tail✝
    
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

tl: List Meas

ih: m ∈ dedup F tl → m ∈ tl

h: m ∈ dedup F (hd :: tl)

m ∈ hd :: tlcase nil => 
      
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

ih: m ∈ dedup F [] → m ∈ []

h: m ∈ dedup F [hd]

m ∈ [hd]simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: m ∈ dedup F [hd]
h
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

ih: m ∈ dedup F [] → m ∈ []

h: m = hd

m ∈ [hd]
      
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

ih: m ∈ dedup F [] → m ∈ []

h: m ∈ dedup F [hd]

m ∈ [hd]simp [
h: m = hd
h]
Goals accomplished! 🐙
    
α✝: Type

m: Meas

F: Factory α✝

hd: Meas

tl: List Meas

ih: m ∈ dedup F tl → m ∈ tl

h: m ∈ dedup F (hd :: tl)

m ∈ hd :: tlcase cons 
hd': ?m.1989
hd' 
tl': List ?m.1989
tl' => 
      
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h: m ∈ dedup F (hd :: hd' :: tl')

m ∈ hd :: hd' :: tl'simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: m ∈ dedup F (hd :: hd' :: tl')
h
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h: m ∈ if Factory.le F hd'.cost hd.cost = true then dedup F (hd' :: tl') else hd :: dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl' 
      
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h: m ∈ dedup F (hd :: hd' :: tl')

m ∈ hd :: hd' :: tl'split_ifs at 
h: m ∈ if Factory.le F hd'.cost hd.cost = true then dedup F (hd' :: tl') else hd :: dedup F (hd' :: tl')
h
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

inl
m ∈ hd :: hd' :: tl'
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ hd :: dedup F (hd' :: tl')

inr
m ∈ hd :: hd' :: tl' 
      
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h: m ∈ dedup F (hd :: hd' :: tl')

m ∈ hd :: hd' :: tl'case inl => 
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'specialize 
ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'
ih 
h: m ∈ dedup F (hd' :: tl')
h
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m ∈ hd :: hd' :: tl' 
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'rw [
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m ∈ hd :: hd' :: tl'
List.mem_cons: ∀ {α : Type ?u.3165} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
List.mem_cons
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m = hd ∨ m ∈ hd' :: tl']
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m = hd ∨ m ∈ hd' :: tl'
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'right
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

h
m ∈ hd' :: tl'
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'assumption
Goals accomplished! 🐙
      
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h: m ∈ dedup F (hd :: hd' :: tl')

m ∈ hd :: hd' :: tl'case inr => 
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ hd :: dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'simp at 
h: m ∈ hd :: dedup F (hd' :: tl')
h
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m = hd ∨ m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl' 
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ hd :: dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'cases 
h: m = hd ∨ m ∈ dedup F (hd' :: tl')
h
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝¹: ¬Factory.le F hd'.cost hd.cost = true

h✝: m = hd

inl
m ∈ hd :: hd' :: tl'
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝¹: ¬Factory.le F hd'.cost hd.cost = true

h✝: m ∈ dedup F (hd' :: tl')

inr
m ∈ hd :: hd' :: tl' 
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ hd :: dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'case inl 
h: ?m.4973
h => 
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m = hd

m ∈ hd :: hd' :: tl'simp [
h: ?m.4973
h]
Goals accomplished! 🐙
        
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ hd :: dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'case inr 
h: ?m.4974
h => 
          
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'specialize 
ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'
ih 
h: ?m.4974
h
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m ∈ hd :: hd' :: tl' 
          
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'rw [
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m ∈ hd :: hd' :: tl'
List.mem_cons: ∀ {α : Type ?u.9119} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
List.mem_cons
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m = hd ∨ m ∈ hd' :: tl']
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

m = hd ∨ m ∈ hd' :: tl'
          
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'right
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

ih: m ∈ hd' :: tl'

h
m ∈ hd' :: tl' 
          
α✝: Type

m: Meas

F: Factory α✝

hd, hd': Meas

tl': List Meas

ih: m ∈ dedup F (hd' :: tl') → m ∈ hd' :: tl'

h✝: ¬Factory.le F hd'.cost hd.cost = true

h: m ∈ dedup F (hd' :: tl')

m ∈ hd :: hd' :: tl'assumption
Goals accomplished! 🐙  

lemma 
dedup_last_first: ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas},
  dedup F (m :: ms) = m' :: ms' → last_decreasing (m :: ms) → m.last ≥ m'.last
dedup_last_first (
h: dedup F (m :: ms) = m' :: ms'
h : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.9189
F (
m: ?m.9200
m :: 
ms: ?m.9209
ms) = 
m': ?m.9220
m' :: 
ms': ?m.9231
ms')
    (
h_last: last_decreasing (m :: ms)
h_last : 
last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (
m: ?m.9200
m :: 
ms: ?m.9209
ms)) : 
    
m: ?m.9200
m.
last: {α : Type} → Meas → ℕ
last ≥ 
m': ?m.9220
m'.
last: {α : Type} → Meas → ℕ
last := by
Goals accomplished! 🐙 
  
α✝: Type

F: Factory α✝

m: Meas

ms: List Meas

m': Meas

ms': List Meas

h: dedup F (m :: ms) = m' :: ms'

h_last: last_decreasing (m :: ms)

m.last ≥ m'.lastinduction 
ms: List Meas
ms generalizing 
m: Meas
m
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h: dedup F [m] = m' :: ms'

h_last: last_decreasing [m]

nil
m.last ≥ m'.last
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

head✝: Meas

tail✝: List Meas

tail_ih✝: ∀ {m : Meas}, dedup F (m :: tail✝) = m' :: ms' → last_decreasing (m :: tail✝) → m.last ≥ m'.last

m: Meas

h: dedup F (m :: head✝ :: tail✝) = m' :: ms'

h_last: last_decreasing (m :: head✝ :: tail✝)

cons
m.last ≥ m'.last
  
α✝: Type

F: Factory α✝

m: Meas

ms: List Meas

m': Meas

ms': List Meas

h: dedup F (m :: ms) = m' :: ms'

h_last: last_decreasing (m :: ms)

m.last ≥ m'.lastcase nil => 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h: dedup F [m] = m' :: ms'

h_last: last_decreasing [m]

m.last ≥ m'.lastsimp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: dedup F [m] = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h_last: last_decreasing [m]

h: m = m' ∧ [] = ms'

m.last ≥ m'.last 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h: dedup F [m] = m' :: ms'

h_last: last_decreasing [m]

m.last ≥ m'.lastsimp [
h: m = m' ∧ [] = ms'
h]
Goals accomplished! 🐙
  
α✝: Type

F: Factory α✝

m: Meas

ms: List Meas

m': Meas

ms': List Meas

h: dedup F (m :: ms) = m' :: ms'

h_last: last_decreasing (m :: ms)

m.last ≥ m'.lastcase cons 
hd: ?m.9326
hd 
tl: List ?m.9326
tl 
ih: ?m.9327 tl
ih => 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: last_decreasing (m :: hd :: tl)

m.last ≥ m'.lastsimp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: dedup F (m :: hd :: tl) = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h: (if Factory.le F hd.cost m.cost = true then dedup F (hd :: tl) else m :: dedup F (hd :: tl)) = m' :: ms'

h_last: last_decreasing (m :: hd :: tl)

m.last ≥ m'.last 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: last_decreasing (m :: hd :: tl)

m.last ≥ m'.lastsplit_ifs at 
h: (if Factory.le F hd.cost m.cost = true then dedup F (hd :: tl) else m :: dedup F (hd :: tl)) = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h✝: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

inl
m.last ≥ m'.last
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m :: dedup F (hd :: tl) = m' :: ms'

inr
m.last ≥ m'.last
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: last_decreasing (m :: hd :: tl)

m.last ≥ m'.lastcase inl 
h_if: Factory.le F hd.cost m.cost = true
h_if => 
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.last ≥ m'.lastspecialize 
ih: ?m.9327 tl
ih 
h: dedup F (hd :: tl) = m' :: ms'
h (
last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest 
h_last: last_decreasing (m :: hd :: tl)
h_last)
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.last ≥ m'.last

m.last ≥ m'.last
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.last ≥ m'.lastreplace 
h_last: ?m.10172
h_last := 
last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head 
h_last: last_decreasing (m :: hd :: tl)
h_last
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.last ≥ m'.last

h_last: m.last > hd.last

m.last ≥ m'.last
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.last ≥ m'.lastclear * - 
h_last: ?m.10172
h_last 
ih: hd.last ≥ m'.last
ih
α✝: Type

m', hd, m: Meas

ih: hd.last ≥ m'.last

h_last: m.last > hd.last

m.last ≥ m'.last
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.last ≥ m'.lastlinarith
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: last_decreasing (m :: hd :: tl)

m.last ≥ m'.lastcase inr => 
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m :: dedup F (hd :: tl) = m' :: ms'

m.last ≥ m'.lastsimp at 
h: m :: dedup F (hd :: tl) = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m = m' ∧ dedup F (hd :: tl) = ms'

m.last ≥ m'.last
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → last_decreasing (m :: tl) → m.last ≥ m'.last

m: Meas

h_last: last_decreasing (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m :: dedup F (hd :: tl) = m' :: ms'

m.last ≥ m'.lastsimp [
h: m = m' ∧ dedup F (hd :: tl) = ms'
h]
Goals accomplished! 🐙
      
lemma 
dedup_last_decreasing: ∀ {α : Type} {ms : List Meas} {F : Factory α}, last_decreasing ms → last_decreasing (dedup F ms)
dedup_last_decreasing (
h: last_decreasing ms
h : 
last_decreasing: {α : Type} → List Meas → Prop
last_decreasing 
ms: ?m.12118
ms) : 
last_decreasing: {α : Type} → List Meas → Prop
last_decreasing (
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.12130
F 
ms: ?m.12118
ms) := by
Goals accomplished! 🐙 
  
α✝: Type

ms: List Meas

F: Factory α✝

h: last_decreasing ms

last_decreasing (dedup F ms)induction 
ms: List Meas
ms
α✝: Type

F: Factory α✝

h: last_decreasing []

nil
last_decreasing (dedup F [])
α✝: Type

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: last_decreasing tail✝ → last_decreasing (dedup F tail✝)

h: last_decreasing (head✝ :: tail✝)

cons
last_decreasing (dedup F (head✝ :: tail✝)) 
  
α✝: Type

ms: List Meas

F: Factory α✝

h: last_decreasing ms

last_decreasing (dedup F ms)case nil => 
α✝: Type

F: Factory α✝

h: last_decreasing []

last_decreasing (dedup F [])simpa [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
Goals accomplished! 🐙
  
α✝: Type

ms: List Meas

F: Factory α✝

h: last_decreasing ms

last_decreasing (dedup F ms)case cons 
x: ?m.12172
x 
tl: List ?m.12172
tl 
ih: ?m.12173 tl
ih => 
    
α✝: Type

F: Factory α✝

x: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (dedup F tl)

h: last_decreasing (x :: tl)

last_decreasing (dedup F (x :: tl))cases 
tl: List ?m.12172
tl
α✝: Type

F: Factory α✝

x: Meas

ih: last_decreasing [] → last_decreasing (dedup F [])

h: last_decreasing [x]

nil
last_decreasing (dedup F [x])
α✝: Type

F: Factory α✝

x, head✝: Meas

tail✝: List Meas

ih: last_decreasing (head✝ :: tail✝) → last_decreasing (dedup F (head✝ :: tail✝))

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

cons
last_decreasing (dedup F (x :: head✝ :: tail✝)) 
    
α✝: Type

F: Factory α✝

x: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (dedup F tl)

h: last_decreasing (x :: tl)

last_decreasing (dedup F (x :: tl))case nil => 
α✝: Type

F: Factory α✝

x: Meas

ih: last_decreasing [] → last_decreasing (dedup F [])

h: last_decreasing [x]

last_decreasing (dedup F [x])simpa [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

x: Meas

tl: List Meas

ih: last_decreasing tl → last_decreasing (dedup F tl)

h: last_decreasing (x :: tl)

last_decreasing (dedup F (x :: tl))case cons 
x': ?m.12257
x' 
tl': List ?m.12257
tl' => 
      
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

last_decreasing (dedup F (x :: x' :: tl'))simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

last_decreasing (if Factory.le F x'.cost x.cost = true then dedup F (x' :: tl') else x :: dedup F (x' :: tl'))
      
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

last_decreasing (dedup F (x :: x' :: tl'))split_ifs
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

inl
last_decreasing (dedup F (x' :: tl'))
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

inr
last_decreasing (x :: dedup F (x' :: tl'))
      
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

last_decreasing (dedup F (x :: x' :: tl'))case inl => 
        
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

last_decreasing (dedup F (x' :: tl'))apply 
ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))
ih
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

last_decreasing (x' :: tl') 
        
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

last_decreasing (dedup F (x' :: tl'))apply 
last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

h
last_decreasing (?x :: x' :: tl')
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

x
Meas
        
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: Factory.le F x'.cost x.cost = true

last_decreasing (dedup F (x' :: tl'))assumption
Goals accomplished! 🐙
      
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

last_decreasing (dedup F (x :: x' :: tl'))case inr => 
        
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

last_decreasing (x :: dedup F (x' :: tl'))cases h_case : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: Factory α✝
F (
x': ?m.12257
x' :: 
tl': List ?m.12257
tl')
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

h_case: dedup F (x' :: tl') = []

nil
last_decreasing [x]
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (x' :: tl') = head✝ :: tail✝

cons
last_decreasing (x :: head✝ :: tail✝)
        
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

last_decreasing (x :: dedup F (x' :: tl'))case nil => 
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

h_case: dedup F (x' :: tl') = []

last_decreasing [x]apply 
last_decreasing_one: ∀ {α : Type} {x : Meas}, last_decreasing [x]
last_decreasing_one
Goals accomplished! 🐙 
        
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

last_decreasing (x :: dedup F (x' :: tl'))case cons => 
          
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)rw [
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)
h_case: dedup F (x' :: tl') = head✝ :: tail✝
h_case
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)]
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝) at 
ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))
ih
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)
          
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)apply 
last_decreasing_cons: ∀ {α : Type} (x y : Meas) (xs : List Meas), x.last > y.last → last_decreasing (y :: xs) → last_decreasing (x :: y :: xs)
last_decreasing_cons
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

h_last
x.last > head✝.last
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

h
last_decreasing (head✝ :: tail✝) 
          
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)case h_last => 
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x.last > head✝.lastreplace 
h_case: ?m.12985
h_case := 
dedup_last_first: ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas},
  dedup F (m :: ms) = m' :: ms' → last_decreasing (m :: ms) → m.last ≥ m'.last
dedup_last_first 
h_case: dedup F (x' :: tl') = head✝ :: tail✝
h_case (
last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest 
h: last_decreasing (x :: x' :: tl')
h)
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: x'.last ≥ head✝.last

x.last > head✝.last
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x.last > head✝.lastsimp at 
h_case: ?m.12985
h_case ⊢
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: head✝.last ≤ x'.last

head✝.last < x.last 
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x.last > head✝.lastreplace 
h: ?m.13524
h := 
last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head 
h: last_decreasing (x :: x' :: tl')
h
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: head✝.last ≤ x'.last

h: x.last > x'.last

head✝.last < x.last
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x.last > head✝.lastsimp at 
h: ?m.13524
h
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: head✝.last ≤ x'.last

h: x'.last < x.last

head✝.last < x.last
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x.last > head✝.lastclear * - 
h_case: head✝.last ≤ x'.last
h_case 
h: x'.last < x.last
h
α✝: Type

x, x', head✝: Meas

h_case: head✝.last ≤ x'.last

h: x'.last < x.last

head✝.last < x.last
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x.last > head✝.lastlinarith
Goals accomplished! 🐙
          
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (dedup F (x' :: tl'))

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x :: head✝ :: tail✝)case h => 
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (head✝ :: tail✝)apply 
ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)
ih
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (x' :: tl') 
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (head✝ :: tail✝)apply 
last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

h
last_decreasing (?x :: x' :: tl')
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

x
Meas  
            
α✝: Type

F: Factory α✝

x, x': Meas

tl': List Meas

h: last_decreasing (x :: x' :: tl')

h✝: ¬Factory.le F x'.cost x.cost = true

head✝: Meas

tail✝: List Meas

ih: last_decreasing (x' :: tl') → last_decreasing (head✝ :: tail✝)

h_case: dedup F (x' :: tl') = head✝ :: tail✝

last_decreasing (head✝ :: tail✝)assumption
Goals accomplished! 🐙

lemma 
dedup_cost_first: ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas},
  dedup F (m :: ms) = m' :: ms' → cost_increasing_non_strict F (m :: ms) → m.cost = m'.cost
dedup_cost_first (
h: dedup F (m :: ms) = m' :: ms'
h : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.15325
F (
m: ?m.15336
m :: 
ms: ?m.15345
ms) = 
m': ?m.15356
m' :: 
ms': ?m.15367
ms')
    (
h_last: cost_increasing_non_strict F (m :: ms)
h_last : 
cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict 
F: ?m.15325
F (
m: ?m.15336
m :: 
ms: ?m.15345
ms)) : 
    
m: ?m.15336
m.
cost: {α : Type} → Meas → α
cost = 
m': ?m.15356
m'.
cost: {α : Type} → Meas → α
cost := by
Goals accomplished! 🐙 
  
α✝: Type

F: Factory α✝

m: Meas

ms: List Meas

m': Meas

ms': List Meas

h: dedup F (m :: ms) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: ms)

m.cost = m'.costinduction 
ms: List Meas
ms generalizing 
m: Meas
m
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h: dedup F [m] = m' :: ms'

h_last: cost_increasing_non_strict F [m]

nil
m.cost = m'.cost
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

head✝: Meas

tail✝: List Meas

tail_ih✝: ∀ {m : Meas}, dedup F (m :: tail✝) = m' :: ms' → cost_increasing_non_strict F (m :: tail✝) → m.cost = m'.cost

m: Meas

h: dedup F (m :: head✝ :: tail✝) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: head✝ :: tail✝)

cons
m.cost = m'.cost
  
α✝: Type

F: Factory α✝

m: Meas

ms: List Meas

m': Meas

ms': List Meas

h: dedup F (m :: ms) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: ms)

m.cost = m'.costcase nil => 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h: dedup F [m] = m' :: ms'

h_last: cost_increasing_non_strict F [m]

m.cost = m'.costsimp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: dedup F [m] = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h_last: cost_increasing_non_strict F [m]

h: m = m' ∧ [] = ms'

m.cost = m'.cost 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

m: Meas

h: dedup F [m] = m' :: ms'

h_last: cost_increasing_non_strict F [m]

m.cost = m'.costsimp [
h: m = m' ∧ [] = ms'
h]
Goals accomplished! 🐙
  
α✝: Type

F: Factory α✝

m: Meas

ms: List Meas

m': Meas

ms': List Meas

h: dedup F (m :: ms) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: ms)

m.cost = m'.costcase cons 
hd: ?m.15451
hd 
tl: List ?m.15451
tl 
ih: ?m.15452 tl
ih =>
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: hd :: tl)

m.cost = m'.costsimp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: dedup F (m :: hd :: tl) = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h: (if Factory.le F hd.cost m.cost = true then dedup F (hd :: tl) else m :: dedup F (hd :: tl)) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: hd :: tl)

m.cost = m'.cost 
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: hd :: tl)

m.cost = m'.costsplit_ifs at 
h: m :: dedup F (hd :: tl) = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h✝: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

inl
m.cost = m'.cost
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m :: dedup F (hd :: tl) = m' :: ms'

inr
m.cost = m'.cost
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: hd :: tl)

m.cost = m'.costcase inl 
h_if: Factory.le F hd.cost m.cost = true
h_if => 
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.cost = m'.costspecialize 
ih: ?m.15452 tl
ih 
h: dedup F (hd :: tl) = m' :: ms'
h (
cost_increasing_non_strict_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs
cost_increasing_non_strict_rest 
h_last: cost_increasing_non_strict F (m :: hd :: tl)
h_last)
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

m.cost = m'.cost
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.cost = m'.costreplace 
h_last: ?m.16227
h_last := 
cost_increasing_non_strict_head: ∀ {α : Type} {F : Factory α} {x y : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: y :: xs) → Factory.le F x.cost y.cost = true
cost_increasing_non_strict_head 
h_last: cost_increasing_non_strict F (m :: hd :: tl)
h_last
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

h_last: Factory.le F m.cost hd.cost = true

m.cost = m'.cost
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.cost = m'.costhave := 
F: Factory α✝
F.
le_antisymm: ∀ {α : Type} (self : Factory α) {c₁ c₂ : α}, Factory.le self c₁ c₂ = true → Factory.le self c₂ c₁ = true → c₁ = c₂
le_antisymm 
h_last: ?m.16227
h_last 
h_if: Factory.le F hd.cost m.cost = true
h_if
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

h_last: Factory.le F m.cost hd.cost = true

this: m.cost = hd.cost

m.cost = m'.cost 
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

m.cost = m'.costrw [
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

h_last: Factory.le F m.cost hd.cost = true

this: m.cost = hd.cost

m.cost = m'.cost
this: ?m.16242
this,
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

h_last: Factory.le F m.cost hd.cost = true

this: m.cost = hd.cost

hd.cost = m'.cost 
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

h_last: Factory.le F m.cost hd.cost = true

this: m.cost = hd.cost

m.cost = m'.cost
ih: hd.cost = m'.cost
ih
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

m: Meas

h_if: Factory.le F hd.cost m.cost = true

h: dedup F (hd :: tl) = m' :: ms'

ih: hd.cost = m'.cost

h_last: Factory.le F m.cost hd.cost = true

this: m.cost = hd.cost

m'.cost = m'.cost]
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h: dedup F (m :: hd :: tl) = m' :: ms'

h_last: cost_increasing_non_strict F (m :: hd :: tl)

m.cost = m'.costcase inr => 
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m :: dedup F (hd :: tl) = m' :: ms'

m.cost = m'.costsimp at 
h: m :: dedup F (hd :: tl) = m' :: ms'
h
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m = m' ∧ dedup F (hd :: tl) = ms'

m.cost = m'.cost
      
α✝: Type

F: Factory α✝

m': Meas

ms': List Meas

hd: Meas

tl: List Meas

ih: ∀ {m : Meas}, dedup F (m :: tl) = m' :: ms' → cost_increasing_non_strict F (m :: tl) → m.cost = m'.cost

m: Meas

h_last: cost_increasing_non_strict F (m :: hd :: tl)

h✝: ¬Factory.le F hd.cost m.cost = true

h: m :: dedup F (hd :: tl) = m' :: ms'

m.cost = m'.costsimp [
h: m = m' ∧ dedup F (hd :: tl) = ms'
h]
Goals accomplished! 🐙
  
lemma 
dedup_cost_increasing: ∀ {α : Type} {F : Factory α} {ms : List Meas}, cost_increasing_non_strict F ms → cost_increasing F (dedup F ms)
dedup_cost_increasing (
h: cost_increasing_non_strict F ms
h : 
cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict 
F: ?m.16376
F 
ms: ?m.16383
ms) : 
cost_increasing: {α : Type} → Factory α → List Meas → Prop
cost_increasing 
F: ?m.16376
F (
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.16376
F 
ms: ?m.16383
ms) := by
Goals accomplished! 🐙 
  
α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing_non_strict F ms

cost_increasing F (dedup F ms)induction 
ms: List Meas
ms
α✝: Type

F: Factory α✝

h: cost_increasing_non_strict F []

nil
cost_increasing F (dedup F [])
α✝: Type

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: cost_increasing_non_strict F tail✝ → cost_increasing F (dedup F tail✝)

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

cons
cost_increasing F (dedup F (head✝ :: tail✝)) 
  
α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing_non_strict F ms

cost_increasing F (dedup F ms)case nil =>  
    
α✝: Type

F: Factory α✝

h: cost_increasing_non_strict F []

cost_increasing F (dedup F [])intro 
i: ℕ
i 
hi: i < List.length (dedup F [])
hi 
hj: i + 1 < List.length (dedup F [])
hj
α✝: Type

F: Factory α✝

h: cost_increasing_non_strict F []

i: ℕ

hi: i < List.length (dedup F [])

hj: i + 1 < List.length (dedup F [])

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

F: Factory α✝

h: cost_increasing_non_strict F []

cost_increasing F (dedup F [])simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
hi: i < List.length (dedup F [])
hi
Goals accomplished! 🐙 
  
α✝: Type

F: Factory α✝

ms: List Meas

h: cost_increasing_non_strict F ms

cost_increasing F (dedup F ms)case cons 
x: ?m.16426
x 
tl: List ?m.16426
tl 
ih: ?m.16427 tl
ih => 
    
α✝: Type

F: Factory α✝

x: Meas

tl: List Meas

ih: cost_increasing_non_strict F tl → cost_increasing F (dedup F tl)

h: cost_increasing_non_strict F (x :: tl)

cost_increasing F (dedup F (x :: tl))cases 
tl: List ?m.16426
tl
α✝: Type

F: Factory α✝

x: Meas

ih: cost_increasing_non_strict F [] → cost_increasing F (dedup F [])

h: cost_increasing_non_strict F [x]

nil
cost_increasing F (dedup F [x])
α✝: Type

F: Factory α✝

x, head✝: Meas

tail✝: List Meas

ih: cost_increasing_non_strict F (head✝ :: tail✝) → cost_increasing F (dedup F (head✝ :: tail✝))

h: cost_increasing_non_strict F (x :: head✝ :: tail✝)

cons
cost_increasing F (dedup F (x :: head✝ :: tail✝)) 
    
α✝: Type

F: Factory α✝

x: Meas

tl: List Meas

ih: cost_increasing_non_strict F tl → cost_increasing F (dedup F tl)

h: cost_increasing_non_strict F (x :: tl)

cost_increasing F (dedup F (x :: tl))case nil => 
      
α✝: Type

F: Factory α✝

x: Meas

ih: cost_increasing_non_strict F [] → cost_increasing F (dedup F [])

h: cost_increasing_non_strict F [x]

cost_increasing F (dedup F [x])simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
α✝: Type

F: Factory α✝

x: Meas

ih: cost_increasing_non_strict F [] → cost_increasing F (dedup F [])

h: cost_increasing_non_strict F [x]

cost_increasing F [x]
      
α✝: Type

F: Factory α✝

x: Meas

ih: cost_increasing_non_strict F [] → cost_increasing F (dedup F [])

h: cost_increasing_non_strict F [x]

cost_increasing F (dedup F [x])apply 
cost_increasing_one: ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing F [x]
cost_increasing_one
Goals accomplished! 🐙
    
α✝: Type

F: Factory α✝

x: Meas

tl: List Meas

ih: cost_increasing_non_strict F tl → cost_increasing F (dedup F tl)

h: cost_increasing_non_strict F (x :: tl)

cost_increasing F (dedup F (x :: tl))case cons 
y: ?m.16637
y 
tl: List ?m.16637
tl => 
      
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

cost_increasing F (dedup F (x :: y :: tl))simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

cost_increasing F (if Factory.le F y.cost x.cost = true then dedup F (y :: tl) else x :: dedup F (y :: tl))
      
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

cost_increasing F (dedup F (x :: y :: tl))split_ifs
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

inl
cost_increasing F (dedup F (y :: tl))
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: ¬Factory.le F y.cost x.cost = true

inr
cost_increasing F (x :: dedup F (y :: tl)) 
      
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

cost_increasing F (dedup F (x :: y :: tl))case inl => 
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

cost_increasing F (dedup F (y :: tl))apply 
ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))
ih
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

cost_increasing_non_strict F (y :: tl) 
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

cost_increasing F (dedup F (y :: tl))apply 
cost_increasing_non_strict_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs
cost_increasing_non_strict_rest
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

h
cost_increasing_non_strict F (?x :: y :: tl)
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

x
Meas 
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h✝: Factory.le F y.cost x.cost = true

cost_increasing F (dedup F (y :: tl))assumption
Goals accomplished! 🐙
      
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

cost_increasing F (dedup F (x :: y :: tl))case inr 
h_if: ¬Factory.le F y.cost x.cost = true
h_if => 
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h_if: ¬Factory.le F y.cost x.cost = true

cost_increasing F (x :: dedup F (y :: tl))replace 
h: ?m.17263
h := 
cost_increasing_non_strict_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs
cost_increasing_non_strict_rest 
h: cost_increasing_non_strict F (x :: y :: tl)
h
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h_if: ¬Factory.le F y.cost x.cost = true

h: cost_increasing_non_strict F (y :: tl)

cost_increasing F (x :: dedup F (y :: tl))
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h_if: ¬Factory.le F y.cost x.cost = true

cost_increasing F (x :: dedup F (y :: tl))specialize 
ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))
ih 
h: ?m.17263
h
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

h_if: ¬Factory.le F y.cost x.cost = true

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

cost_increasing F (x :: dedup F (y :: tl))
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h_if: ¬Factory.le F y.cost x.cost = true

cost_increasing F (x :: dedup F (y :: tl))rw [
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

h_if: ¬Factory.le F y.cost x.cost = true

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

cost_increasing F (x :: dedup F (y :: tl))
Factory.not_le_iff_lt: ∀ {α : Type} {F : Factory α} {c₁ c₂ : α}, ¬Factory.le F c₁ c₂ = true ↔ Factory.lt F c₂ c₁
Factory.not_le_iff_lt
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

cost_increasing F (x :: dedup F (y :: tl))]
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

cost_increasing F (x :: dedup F (y :: tl)) at 
h_if: ¬Factory.le F y.cost x.cost = true
h_if
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

cost_increasing F (x :: dedup F (y :: tl))
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h_if: ¬Factory.le F y.cost x.cost = true

cost_increasing F (x :: dedup F (y :: tl))cases h_case : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: Factory α✝
F (
y: ?m.16637
y :: 
tl: List ?m.16637
tl)
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

h_case: dedup F (y :: tl) = []

nil
cost_increasing F [x]
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

cons
cost_increasing F (x :: head✝ :: tail✝) 
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h_if: ¬Factory.le F y.cost x.cost = true

cost_increasing F (x :: dedup F (y :: tl))case nil => 
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

h_case: dedup F (y :: tl) = []

cost_increasing F [x]apply 
cost_increasing_one: ∀ {α : Type} {F : Factory α} {x : Meas}, cost_increasing F [x]
cost_increasing_one
Goals accomplished! 🐙
        
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

ih: cost_increasing_non_strict F (y :: tl) → cost_increasing F (dedup F (y :: tl))

h: cost_increasing_non_strict F (x :: y :: tl)

h_if: ¬Factory.le F y.cost x.cost = true

cost_increasing F (x :: dedup F (y :: tl))case cons => 
          
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

cost_increasing F (x :: head✝ :: tail✝)replace 
h: ?m.17406
h := 
dedup_cost_first: ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas},
  dedup F (m :: ms) = m' :: ms' → cost_increasing_non_strict F (m :: ms) → m.cost = m'.cost
dedup_cost_first 
h_case: dedup F (y :: tl) = head✝ :: tail✝
h_case 
h: cost_increasing_non_strict F (y :: tl)
h
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

cost_increasing F (x :: head✝ :: tail✝)
          
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

cost_increasing F (x :: head✝ :: tail✝)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 α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

h_cost
Factory.lt F x.cost head✝.cost
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

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

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

cost_increasing F (x :: head✝ :: tail✝)case h => 
            
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

cost_increasing F (head✝ :: tail✝)simp [
h_case: dedup F (y :: tl) = head✝ :: tail✝
h_case] at 
ih: cost_increasing F (dedup F (y :: tl))
ih
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

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

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

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

cost_increasing F (head✝ :: tail✝)assumption
Goals accomplished! 🐙
          
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

h: cost_increasing_non_strict F (y :: tl)

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

cost_increasing F (x :: head✝ :: tail✝)case h_cost => 
            
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

Factory.lt F x.cost head✝.costrw [
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

Factory.lt F x.cost head✝.cost←
h: ?m.17406
h
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

Factory.lt F x.cost y.cost]
α✝: Type

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

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

F: Factory α✝

x, y: Meas

tl: List Meas

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

ih: cost_increasing F (dedup F (y :: tl))

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: tl) = head✝ :: tail✝

h: y.cost = head✝.cost

Factory.lt F x.cost head✝.costapply 
h_if: Factory.lt F x.cost y.cost
h_if
Goals accomplished! 🐙 

lemma 
dedup_cons: ∀ {α : Type} {m : Meas} {F : Factory α} {ms : List Meas} (m' : Meas), m ∈ dedup F ms → m ∈ dedup F (m' :: ms)
dedup_cons (
m': Meas
m' : 
Meas: {α : Type} → Type
Meas) (
h: m ∈ dedup F ms
h : 
m: ?m.17535
m ∈ 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.17558
F 
ms: ?m.17583
ms) : 
m: ?m.17535
m ∈ 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.17558
F (
m': Meas
m' :: 
ms: ?m.17583
ms) := by
Goals accomplished! 🐙 
  
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

m': Meas

h: m ∈ dedup F ms

m ∈ dedup F (m' :: ms)cases 
ms: List Meas
ms
α✝: Type

m: Meas

F: Factory α✝

m': Meas

h: m ∈ dedup F []

nil
m ∈ dedup F [m']
α✝: Type

m: Meas

F: Factory α✝

m', head✝: Meas

tail✝: List Meas

h: m ∈ dedup F (head✝ :: tail✝)

cons
m ∈ dedup F (m' :: head✝ :: tail✝) 
  
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

m': Meas

h: m ∈ dedup F ms

m ∈ dedup F (m' :: ms)case nil => 
α✝: Type

m: Meas

F: Factory α✝

m': Meas

h: m ∈ dedup F []

m ∈ dedup F [m']simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup] at 
h: m ∈ dedup F []
h
Goals accomplished! 🐙
  
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

m': Meas

h: m ∈ dedup F ms

m ∈ dedup F (m' :: ms)case cons 
x: ?m.17680
x 
tl: List ?m.17680
tl => 
    
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

m ∈ dedup F (m' :: x :: tl)simp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

m ∈ if Factory.le F x.cost m'.cost = true then dedup F (x :: tl) else m' :: dedup F (x :: tl)
    
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

m ∈ dedup F (m' :: x :: tl)split_ifs
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

h✝: Factory.le F x.cost m'.cost = true

inl
m ∈ dedup F (x :: tl)
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

h✝: ¬Factory.le F x.cost m'.cost = true

inr
m ∈ m' :: dedup F (x :: tl)
    
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

m ∈ dedup F (m' :: x :: tl)case inl => 
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

h✝: Factory.le F x.cost m'.cost = true

m ∈ dedup F (x :: tl)assumption
Goals accomplished! 🐙
    
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

m ∈ dedup F (m' :: x :: tl)case inr => 
      
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

h✝: ¬Factory.le F x.cost m'.cost = true

m ∈ m' :: dedup F (x :: tl)apply 
List.Mem.tail: ∀ {α : Type ?u.18873} {a : α} (b : α) {as : List α}, List.Mem a as → List.Mem a (b :: as)
List.Mem.tail
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

h✝: ¬Factory.le F x.cost m'.cost = true

a
List.Mem m (dedup F (x :: tl)) 
      
α✝: Type

m: Meas

F: Factory α✝

m', x: Meas

tl: List Meas

h: m ∈ dedup F (x :: tl)

h✝: ¬Factory.le F x.cost m'.cost = true

m ∈ m' :: dedup F (x :: tl)assumption
Goals accomplished! 🐙

lemma 
dedup_dom: ∀ {α : Type} {m : Meas} {ms : List Meas} {F : Factory α},
  m ∈ ms →
    last_decreasing ms →
      cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true
dedup_dom (
h: m ∈ ms
h : 
m: ?m.18926
m ∈ 
ms: ?m.18945
ms) (
h_last: last_decreasing ms
h_last : 
last_decreasing: {α : Type} → List Meas → Prop
last_decreasing 
ms: ?m.18945
ms) (
h_cost: cost_increasing_non_strict F ms
h_cost : 
cost_increasing_non_strict: {α : Type} → Factory α → List Meas → Prop
cost_increasing_non_strict 
F: ?m.18988
F 
ms: ?m.18945
ms) : ∃ 
m_better: ?m.19037
m_better, 
m_better: ?m.19037
m_better ∈ 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: ?m.18988
F 
ms: ?m.18945
ms ∧ 
dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates 
F: ?m.18988
F 
m_better: ?m.19037
m_better 
m: ?m.18926
m := by
Goals accomplished! 🐙 
α✝: Type

m: Meas

ms: List Meas

F: Factory α✝

h: m ∈ ms

h_last: last_decreasing ms

h_cost: cost_increasing_non_strict F ms

∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true{
α✝: Type

m: Meas

ms: List Meas

F: Factory α✝

h: m ∈ ms

h_last: last_decreasing ms

h_cost: cost_increasing_non_strict F ms

∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true
  
α✝: Type

m: Meas

ms: List Meas

F: Factory α✝

h: m ∈ ms

h_last: last_decreasing ms

h_cost: cost_increasing_non_strict F ms

∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = trueinduction 
ms: List Meas
ms
α✝: Type

m: Meas

F: Factory α✝

h: m ∈ []

h_last: last_decreasing []

h_cost: cost_increasing_non_strict F []

nil
∃ m_better, m_better ∈ dedup F [] ∧ dominates F m_better m = true
α✝: Type

m: Meas

F: Factory α✝

head✝: Meas

tail✝: List Meas

tail_ih✝: m ∈ tail✝ →
  last_decreasing tail✝ →
    cost_increasing_non_strict F tail✝ → ∃ m_better, m_better ∈ dedup F tail✝ ∧ dominates F m_better m = true

h: m ∈ head✝ :: tail✝

h_last: last_decreasing (head✝ :: tail✝)

h_cost: cost_increasing_non_strict F (head✝ :: tail✝)

cons
∃ m_better, m_better ∈ dedup F (head✝ :: tail✝) ∧ dominates F m_better m = true
  
α✝: Type

m: Meas

ms: List Meas

F: Factory α✝

h: m ∈ ms

h_last: last_decreasing ms

h_cost: cost_increasing_non_strict F ms

∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = truecase nil => 
α✝: Type

m: Meas

F: Factory α✝

h: m ∈ []

h_last: last_decreasing []

h_cost: cost_increasing_non_strict F []

∃ m_better, m_better ∈ dedup F [] ∧ dominates F m_better m = truecontradiction
Goals accomplished! 🐙
  
α✝: Type

m: Meas

ms: List Meas

F: Factory α✝

h: m ∈ ms

h_last: last_decreasing ms

h_cost: cost_increasing_non_strict F ms

∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = truecase cons 
x: ?m.19176
x 
ms: List ?m.19176
ms 
ih: ?m.19177 ms
ih => 
    
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h: m ∈ x :: ms

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = truecases 
h: m ∈ x :: ms
h
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (m :: ms)

h_cost: cost_increasing_non_strict F (m :: ms)

head
∃ m_better, m_better ∈ dedup F (m :: ms) ∧ dominates F m_better m = true
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

a✝: List.Mem m ms

tail
∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = true 
    
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h: m ∈ x :: ms

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = truecase head => 
      
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (m :: ms)

h_cost: cost_increasing_non_strict F (m :: ms)

∃ m_better, m_better ∈ dedup F (m :: ms) ∧ dominates F m_better m = truecases 
ms: List ?m.19176
ms
α✝: Type

m: Meas

F: Factory α✝

ih: m ∈ [] →
  last_decreasing [] →
    cost_increasing_non_strict F [] → ∃ m_better, m_better ∈ dedup F [] ∧ dominates F m_better m = true

h_last: last_decreasing [m]

h_cost: cost_increasing_non_strict F [m]

nil
∃ m_better, m_better ∈ dedup F [m] ∧ dominates F m_better m = true
α✝: Type

m: Meas

F: Factory α✝

head✝: Meas

tail✝: List Meas

ih: m ∈ head✝ :: tail✝ →
  last_decreasing (head✝ :: tail✝) →
    cost_increasing_non_strict F (head✝ :: tail✝) →
      ∃ m_better, m_better ∈ dedup F (head✝ :: tail✝) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: head✝ :: tail✝)

h_cost: cost_increasing_non_strict F (m :: head✝ :: tail✝)

cons
∃ m_better, m_better ∈ dedup F (m :: head✝ :: tail✝) ∧ dominates F m_better m = true 
      
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (m :: ms)

h_cost: cost_increasing_non_strict F (m :: ms)

∃ m_better, m_better ∈ dedup F (m :: ms) ∧ dominates F m_better m = truecase nil => 
α✝: Type

m: Meas

F: Factory α✝

ih: m ∈ [] →
  last_decreasing [] →
    cost_increasing_non_strict F [] → ∃ m_better, m_better ∈ dedup F [] ∧ dominates F m_better m = true

h_last: last_decreasing [m]

h_cost: cost_increasing_non_strict F [m]

∃ m_better, m_better ∈ dedup F [m] ∧ dominates F m_better m = truesimp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup, 
dominates_refl: ∀ {α : Type} {m : Meas} (F : Factory α), dominates F m m = true
dominates_refl]
Goals accomplished! 🐙
      
α✝: Type

m: Meas

F: Factory α✝

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (m :: ms)

h_cost: cost_increasing_non_strict F (m :: ms)

∃ m_better, m_better ∈ dedup F (m :: ms) ∧ dominates F m_better m = truecase cons 
y: ?m.19452
y 
ms: List ?m.19452
ms => 
        
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

∃ m_better, m_better ∈ dedup F (m :: y :: ms) ∧ dominates F m_better m = truesimp [
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup]
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

∃ m_better,
  (m_better ∈ if Factory.le F y.cost m.cost = true then dedup F (y :: ms) else m :: dedup F (y :: ms)) ∧     dominates F m_better m = true
        
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

∃ m_better, m_better ∈ dedup F (m :: y :: ms) ∧ dominates F m_better m = truesplit_ifs
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

inl
∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: ¬Factory.le F y.cost m.cost = true

inr
∃ m_better, m_better ∈ m :: dedup F (y :: ms) ∧ dominates F m_better m = true 
        
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

∃ m_better, m_better ∈ dedup F (m :: y :: ms) ∧ dominates F m_better m = truecase inl => 
          
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = truecases h_case : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: Factory α✝
F (
y: ?m.19452
y :: 
ms: List ?m.19452
ms)
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

nil
∃ m_better, m_better ∈ [] ∧ dominates F m_better m = true
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

head✝: Meas

tail✝: List Meas

h_case: dedup F (y :: ms) = head✝ :: tail✝

cons
∃ m_better, m_better ∈ head✝ :: tail✝ ∧ dominates F m_better m = true 
          
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = truecase nil => 
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

∃ m_better, m_better ∈ [] ∧ dominates F m_better m = truehave : 
dedup: {α : Type} → Factory α → List Meas → List Meas
dedup 
F: Factory α✝
F (
y: ?m.19452
y :: 
ms: List ?m.19452
ms) ≠ 
[]: List ?m.22938
[] := 
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

∃ m_better, m_better ∈ [] ∧ dominates F m_better m = trueby
Goals accomplished! 🐙 
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

dedup F (y :: ms) ≠ []{
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

dedup F (y :: ms) ≠ []
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

dedup F (y :: ms) ≠ []apply 
dedup_not_empty: ∀ {α : Type} {ms : List Meas} {F : Factory α}, ms ≠ [] → dedup F ms ≠ []
dedup_not_empty
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

h
y :: ms ≠ []
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

dedup F (y :: ms) ≠ []simp
Goals accomplished! 🐙
            }
Goals accomplished! 🐙
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

h_case: dedup F (y :: ms) = []

∃ m_better, m_better ∈ [] ∧ dominates F m_better m = truecontradiction
Goals accomplished! 🐙
          
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = truecase cons 
hd: ?m.22884
hd 
tl: List ?m.22884
tl => 
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = trueexists 
hd: ?m.22884
hd
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

hd ∈ hd :: tl ∧ dominates F hd m = true 
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = truesimp
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

dominates F hd m = true 
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = truehave 
h_last': ?m.24643
h_last' := 
dedup_last_first: ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas},
  dedup F (m :: ms) = m' :: ms' → last_decreasing (m :: ms) → m.last ≥ m'.last
dedup_last_first 
h_case: dedup F (y :: ms) = hd :: tl
h_case (
last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest 
h_last: last_decreasing (m :: y :: ms)
h_last)
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

dominates F hd m = true
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = truehave 
h_cost': ?m.24673
h_cost' := 
dedup_cost_first: ∀ {α : Type} {F : Factory α} {m : Meas} {ms : List Meas} {m' : Meas} {ms' : List Meas},
  dedup F (m :: ms) = m' :: ms' → cost_increasing_non_strict F (m :: ms) → m.cost = m'.cost
dedup_cost_first 
h_case: dedup F (y :: ms) = hd :: tl
h_case (
cost_increasing_non_strict_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs
cost_increasing_non_strict_rest 
h_cost: cost_increasing_non_strict F (m :: y :: ms)
h_cost)
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

dominates F hd m = true
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = truesimp [
dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

hd.last ≤ m.last ∧ Factory.le F hd.cost m.cost = true
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = trueconstructor
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

left
hd.last ≤ m.last
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

right
Factory.le F hd.cost m.cost = true 
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = truecase left => 
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

hd.last ≤ m.lasthave 
h_last'': ?m.25055
h_last'' := 
last_decreasing_head: ∀ {α : Type} {x y : Meas} {xs : List Meas}, last_decreasing (x :: y :: xs) → x.last > y.last
last_decreasing_head 
h_last: last_decreasing (m :: y :: ms)
h_last
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

h_last'': m.last > y.last

hd.last ≤ m.last 
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

hd.last ≤ m.lastclear * - 
h_last': ?m.24643
h_last' 
h_last'': ?m.25055
h_last''
α✝: Type

m, y, hd: Meas

h_last': y.last ≥ hd.last

h_last'': m.last > y.last

hd.last ≤ m.last
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

hd.last ≤ m.lastlinarith
Goals accomplished! 🐙
            
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

∃ m_better, m_better ∈ hd :: tl ∧ dominates F m_better m = truecase right => 
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

Factory.le F hd.cost m.cost = truerw [
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

Factory.le F hd.cost m.cost = true←
h_cost': ?m.24673
h_cost'
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

Factory.le F y.cost m.cost = true]
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

Factory.le F y.cost m.cost = true
              
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: Factory.le F y.cost m.cost = true

hd: Meas

tl: List Meas

h_case: dedup F (y :: ms) = hd :: tl

h_last': y.last ≥ hd.last

h_cost': y.cost = hd.cost

Factory.le F hd.cost m.cost = trueassumption
Goals accomplished! 🐙
        
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

∃ m_better, m_better ∈ dedup F (m :: y :: ms) ∧ dominates F m_better m = truecase inr => 
α✝: Type

m: Meas

F: Factory α✝

y: Meas

ms: List Meas

ih: m ∈ y :: ms →
  last_decreasing (y :: ms) →
    cost_increasing_non_strict F (y :: ms) → ∃ m_better, m_better ∈ dedup F (y :: ms) ∧ dominates F m_better m = true

h_last: last_decreasing (m :: y :: ms)

h_cost: cost_increasing_non_strict F (m :: y :: ms)

h✝: ¬Factory.le F y.cost m.cost = true

∃ m_better, m_better ∈ m :: dedup F (y :: ms) ∧ dominates F m_better m = truesimp [
dominates_refl: ∀ {α : Type} {m : Meas} (F : Factory α), dominates F m m = true
dominates_refl]
Goals accomplished! 🐙
    
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h: m ∈ x :: ms

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = truecase tail 
h: List.Mem m ms
h => 
      
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h: List.Mem m ms

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = truelet ⟨
m_better: Meas
m_better, 
h: m_better ∈ dedup F ms
h, 
h_dom: dominates F m_better m = true
h_dom⟩ := 
ih: ?m.19177 ms
ih 
h: List.Mem m ms
h (
last_decreasing_rest: ∀ {α : Type} {x : Meas} {xs : List Meas}, last_decreasing (x :: xs) → last_decreasing xs
last_decreasing_rest 
h_last: last_decreasing (x :: ms)
h_last) (
cost_increasing_non_strict_rest: ∀ {α : Type} {F : Factory α} {x : Meas} {xs : List Meas},
  cost_increasing_non_strict F (x :: xs) → cost_increasing_non_strict F xs
cost_increasing_non_strict_rest 
h_cost: cost_increasing_non_strict F (x :: ms)
h_cost)
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h✝: List.Mem m ms

m_better: Meas

h: m_better ∈ dedup F ms

h_dom: dominates F m_better m = true

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = true
      
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h: List.Mem m ms

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = trueexists 
m_better: Meas
m_better
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h✝: List.Mem m ms

m_better: Meas

h: m_better ∈ dedup F ms

h_dom: dominates F m_better m = true

m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = true
      
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h: List.Mem m ms

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = truereplace 
h: ?m.30408
h := 
dedup_cons: ∀ {α : Type} {m : Meas} {F : Factory α} {ms : List Meas} (m' : Meas), m ∈ dedup F ms → m ∈ dedup F (m' :: ms)
dedup_cons 
x: ?m.19176
x 
h: m_better ∈ dedup F ms
h
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h✝: List.Mem m ms

m_better: Meas

h_dom: dominates F m_better m = true

h: m_better ∈ dedup F (x :: ms)

m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = true
      
α✝: Type

m: Meas

F: Factory α✝

x: Meas

ms: List Meas

ih: m ∈ ms →
  last_decreasing ms →
    cost_increasing_non_strict F ms → ∃ m_better, m_better ∈ dedup F ms ∧ dominates F m_better m = true

h_last: last_decreasing (x :: ms)

h_cost: cost_increasing_non_strict F (x :: ms)

h: List.Mem m ms

∃ m_better, m_better ∈ dedup F (x :: ms) ∧ dominates F m_better m = truesimp [
h: ?m.30408
h, 
h_dom: dominates F m_better m = true
h_dom]
Goals accomplished! 🐙     
}
Goals accomplished! 🐙