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

/-! 
## Various lemmas about domination
-/

lemma dominates_refl: ∀ {α : Type} {m : Meas} (F : Factory α), dominates F m m = true
dominates_refl (F: Factory α
F : Factory: Type → Type
Factory α: ?m.3
α) : dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m: ?m.11
m m: ?m.11
m := by
Goals accomplished! 🐙 α: Type

m: Meas

F: Factory α

dominates F m m = true{α: Type

m: Meas

F: Factory α

dominates F m m = true
  α: Type

m: Meas

F: Factory α

dominates F m m = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates, Factory.le_refl: ∀ {α : Type} {F : Factory α} (c : α), Factory.le F c c = true
Factory.le_refl]
Goals accomplished! 🐙
}
Goals accomplished! 🐙

lemma dominates_trans: ∀ {α : Type} {m₁ m₂ m₃ : Meas} {F : Factory α},
  dominates F m₁ m₂ = true → dominates F m₂ m₃ = true → dominates F m₁ m₃ = true
dominates_trans {F: Factory α
F : Factory: Type → Type
Factory α: ?m.233
α} (h: dominates F m₁ m₂ = true
h : dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₁: ?m.241
m₁ m₂: ?m.249
m₂) (h': dominates F m₂ m₃ = true
h' : dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₂: ?m.249
m₂ m₃: ?m.273
m₃) : dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₁: ?m.241
m₁ m₃: ?m.273
m₃ := by
Goals accomplished! 🐙 α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: dominates F m₁ m₂ = true

h': dominates F m₂ m₃ = true

dominates F m₁ m₃ = true{α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: dominates F m₁ m₂ = true

h': dominates F m₂ m₃ = true

dominates F m₁ m₃ = true
  α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: dominates F m₁ m₂ = true

h': dominates F m₂ m₃ = true

dominates F m₁ m₃ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates] at *α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

m₁.last ≤ m₃.last ∧ Factory.le F m₁.cost m₃.cost = true 
  α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: dominates F m₁ m₂ = true

h': dominates F m₂ m₃ = true

dominates F m₁ m₃ = trueconstructorα: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

leftm₁.last ≤ m₃.last
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

rightFactory.le F m₁.cost m₃.cost = true 
  α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: dominates F m₁ m₂ = true

h': dominates F m₂ m₃ = true

dominates F m₁ m₃ = truecase left => 
    α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

m₁.last ≤ m₃.lastapply le_trans: ∀ {α : Type ?u.1470} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_transα: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

am₁.last ≤ ?b
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

a?b ≤ m₃.last
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

bℕ 
    α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

m₁.last ≤ m₃.last. α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

am₁.last ≤ ?b
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

a?b ≤ m₃.last
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

bℕapply h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true
h.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙 
    α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

m₁.last ≤ m₃.last. α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

am₂.last ≤ m₃.lastapply h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true
h'.left: ∀ {a b : Prop}, a ∧ b → a
left
Goals accomplished! 🐙
  α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: dominates F m₁ m₂ = true

h': dominates F m₂ m₃ = true

dominates F m₁ m₃ = truecase right => 
    α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

Factory.le F m₁.cost m₃.cost = trueapply F: Factory α
F.le_trans: ∀ {α : Type} (self : Factory α) {c₁ c₂ c₃ : α},
  Factory.le self c₁ c₂ = true → Factory.le self c₂ c₃ = true → Factory.le self c₁ c₃ = true
le_transα: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

aFactory.le F m₁.cost ?m.1551 = true
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

aFactory.le F ?m.1551 m₃.cost = true
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

α 
    α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

Factory.le F m₁.cost m₃.cost = true. α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

aFactory.le F m₁.cost ?m.1551 = true
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

aFactory.le F ?m.1551 m₃.cost = true
α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

αapply h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true
h.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙
    α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

Factory.le F m₁.cost m₃.cost = true. α: Type

m₁, m₂, m₃: Meas

F: Factory α

h: m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true

h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true

aFactory.le F m₂.cost m₃.cost = trueapply h': m₂.last ≤ m₃.last ∧ Factory.le F m₂.cost m₃.cost = true
h'.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙
}
Goals accomplished! 🐙

inductive FourCases: {α : Type} → (F : Factory α) → (m₁ : Meas) → Meas → Prop
FourCases (F: Factory α
F : Factory: Type → Type
Factory α: ?m.1580
α) (m₁: Meas
m₁ m₂: Meas
m₂ : Meas: {α : Type} → Type
Meas) : Prop: Type
Prop where 
  | first_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, dominates F m₁ m₂ = true → FourCases F m₁ m₂
first_dom  (h_dom: dominates F m₁ m₂ = true
h_dom : dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₁: Meas
m₁ m₂: Meas
m₂)
  | second_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, ¬dominates F m₁ m₂ = true → dominates F m₂ m₁ = true → FourCases F m₁ m₂
second_dom (h_non_dom: ¬dominates F m₁ m₂ = true
h_non_dom : ¬ (dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₁: Meas
m₁ m₂: Meas
m₂)) 
               (h_dom: dominates F m₂ m₁ = true
h_dom : dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₂: Meas
m₂ m₁: Meas
m₁) 
  | first_last: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas},
  ¬dominates F m₁ m₂ = true → ¬dominates F m₂ m₁ = true → m₁.last > m₂.last → FourCases F m₁ m₂
first_last (h_non_dom₁: ¬dominates F m₁ m₂ = true
h_non_dom₁ : ¬ (dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₁: Meas
m₁ m₂: Meas
m₂)) 
             (h_non_dom₂: ¬dominates F m₂ m₁ = true
h_non_dom₂ : ¬ (dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₂: Meas
m₂ m₁: Meas
m₁))
             (h: m₁.last > m₂.last
h : m₁: Meas
m₁.last: {α : Type} → Meas → ℕ
last > m₂: Meas
m₂.last: {α : Type} → Meas → ℕ
last) 
  | second_last: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas},
  ¬dominates F m₁ m₂ = true → ¬dominates F m₂ m₁ = true → m₂.last > m₁.last → FourCases F m₁ m₂
second_last (h_non_dom₁: ¬dominates F m₁ m₂ = true
h_non_dom₁ : ¬ (dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₁: Meas
m₁ m₂: Meas
m₂)) 
              (h_non_dom₂: ¬dominates F m₂ m₁ = true
h_non_dom₂ : ¬ (dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates F: Factory α
F m₂: Meas
m₂ m₁: Meas
m₁))
              (h: m₂.last > m₁.last
h : m₂: Meas
m₂.last: {α : Type} → Meas → ℕ
last > m₁: Meas
m₁.last: {α : Type} → Meas → ℕ
last) 

/--
In the `merge` operation, there are four possible cases
based on domination of two measures. 
This lemma creates an exhaustive case analysis for these four cases.
-/
lemma four_cases: ∀ {α : Type} (F : Factory α) (m₁ m₂ : Meas), FourCases F m₁ m₂
four_cases (F: Factory α
F : Factory: Type → Type
Factory α: ?m.1859
α) (m₁: Meas
m₁ m₂: Meas
m₂ : Meas: {α : Type} → Type
Meas) : FourCases: {α : Type} → Factory α → Meas → Meas → Prop
FourCases F: Factory α
F m₁: Meas
m₁ m₂: Meas
m₂ := by
Goals accomplished! 🐙 α: Type

F: Factory α

m₁, m₂: Meas

FourCases F m₁ m₂{α: Type

F: Factory α

m₁, m₂: Meas

FourCases F m₁ m₂
  α: Type

F: Factory α

m₁, m₂: Meas

FourCases F m₁ m₂cases lt_trichotomy: ∀ {α : Type ?u.1880} [inst : LinearOrder α] (a b : α), a < b ∨ a = b ∨ b < a
lt_trichotomy m₁: Meas
m₁.last: {α : Type} → Meas → ℕ
last m₂: Meas
m₂.last: {α : Type} → Meas → ℕ
lastα: Type

F: Factory α

m₁, m₂: Meas

h✝: m₁.last < m₂.last

inlFourCases F m₁ m₂
α: Type

F: Factory α

m₁, m₂: Meas

h✝: m₁.last = m₂.last ∨ m₂.last < m₁.last

inrFourCases F m₁ m₂
  α: Type

F: Factory α

m₁, m₂: Meas

FourCases F m₁ m₂case inl h: ?m.1915
h => 
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last < m₂.last

FourCases F m₁ m₂simp [h: ?m.1915
h, le_of_lt: ∀ {α : Type ?u.1966} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt h: ?m.1915
h]α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last < m₂.last

FourCases F m₁ m₂
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last < m₂.last

FourCases F m₁ m₂by_cases F: Factory α
F.le: {α : Type} → Factory α → α → α → Bool
le m₁: Meas
m₁.cost: {α : Type} → Meas → α
cost m₂: Meas
m₂.cost: {α : Type} → Meas → α
cost = true: Bool
trueα: Type

F: Factory α

m₁, m₂: Meas

h✝: m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

posFourCases F m₁ m₂
α: Type

F: Factory α

m₁, m₂: Meas

h✝: m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

negFourCases F m₁ m₂
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last < m₂.last

FourCases F m₁ m₂case pos h': ?m.1915
h' => 
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂apply FourCases.first_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, dominates F m₁ m₂ = true → FourCases F m₁ m₂
FourCases.first_domα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

h_domdominates F m₁ m₂ = true
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂case h_dom => 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

dominates F m₁ m₂ = truesimp only [
          dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates, Bool.decide_and: ∀ (p q : Prop) [inst : Decidable p] [inst_1 : Decidable q], decide (p ∧ q) = (decide p && decide q)
Bool.decide_and, Bool.decide_coe: ∀ (b : Bool) {h : Decidable (b = true)}, decide (b = true) = b
Bool.decide_coe, 
          Bool.and_eq_true: ∀ (a b : Bool), ((a && b) = true) = (a = true ∧ b = true)
Bool.and_eq_true, decide_eq_true_eq: ∀ {p : Prop} [inst : Decidable p], (decide p = true) = p
decide_eq_true_eq
        ]α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

dominates F m₁ m₂ = truedwi { α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = trueconstructorα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

leftm₁.last ≤ m₂.last
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

rightFactory.le F m₁.cost m₂.cost = true }α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

leftm₁.last ≤ m₂.last
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

dominates F m₁ m₂ = truecase left => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.lastapply le_of_lt: ∀ {α : Type ?u.2494} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_ltα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

am₁.last < m₂.last
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.lastassumption
Goals accomplished! 🐙
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last < m₂.last

FourCases F m₁ m₂case neg h': ?m.1915
h' => 
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂dwi { α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂apply FourCases.second_last: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas},
  ¬dominates F m₁ m₂ = true → ¬dominates F m₂ m₁ = true → m₂.last > m₁.last → FourCases F m₁ m₂
FourCases.second_lastα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h_non_dom₁¬dominates F m₁ m₂ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h_non_dom₂¬dominates F m₂ m₁ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

hm₂.last > m₁.last }α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h_non_dom₁¬dominates F m₁ m₂ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h_non_dom₂¬dominates F m₂ m₁ = true 
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂case h_non_dom₁ => 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = truesimp only [
          dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates, Bool.decide_and: ∀ (p q : Prop) [inst : Decidable p] [inst_1 : Decidable q], decide (p ∧ q) = (decide p && decide q)
Bool.decide_and, Bool.decide_coe: ∀ (b : Bool) {h : Decidable (b = true)}, decide (b = true) = b
Bool.decide_coe, 
          Bool.and_eq_true: ∀ (a b : Bool), ((a && b) = true) = (a = true ∧ b = true)
Bool.and_eq_true, decide_eq_true_eq: ∀ {p : Prop} [inst : Decidable p], (decide p = true) = p
decide_eq_true_eq, not_and: ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
not_and, Bool.not_eq_true: ∀ (b : Bool), (¬b = true) = (b = false)
Bool.not_eq_true
        ]α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.last → Factory.le F m₁.cost m₂.cost = false
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = trueintroα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

a✝: m₁.last ≤ m₂.last

Factory.le F m₁.cost m₂.cost = false
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = truesimp at h: ?m.2074
hα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

a✝: m₁.last ≤ m₂.last

h: Factory.le F m₁.cost m₂.cost = false

Factory.le F m₁.cost m₂.cost = false
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = trueassumption
Goals accomplished! 🐙
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂case h_non_dom₂ => 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₂ m₁ = truesimp only [
          dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates, Bool.decide_and: ∀ (p q : Prop) [inst : Decidable p] [inst_1 : Decidable q], decide (p ∧ q) = (decide p && decide q)
Bool.decide_and, Bool.decide_coe: ∀ (b : Bool) {h : Decidable (b = true)}, decide (b = true) = b
Bool.decide_coe,
          Bool.and_eq_true: ∀ (a b : Bool), ((a && b) = true) = (a = true ∧ b = true)
Bool.and_eq_true, decide_eq_true_eq: ∀ {p : Prop} [inst : Decidable p], (decide p = true) = p
decide_eq_true_eq, not_and: ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
not_and, Bool.not_eq_true: ∀ (b : Bool), (¬b = true) = (b = false)
Bool.not_eq_true
        ]α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₂.last ≤ m₁.last → Factory.le F m₂.cost m₁.cost = false
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₂ m₁ = trueintroα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

a✝: m₂.last ≤ m₁.last

Factory.le F m₂.cost m₁.cost = false
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₂ m₁ = truereplace h': ?m.3372
h' := not_le_of_lt: ∀ {α : Type ?u.3373} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le_of_lt h': ?m.1915
h'α: Type

F: Factory α

m₁, m₂: Meas

h: ¬Factory.le F m₁.cost m₂.cost = true

a✝: m₂.last ≤ m₁.last

h': ¬m₂.last ≤ m₁.last

Factory.le F m₂.cost m₁.cost = false 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last < m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₂ m₁ = truecontradiction
Goals accomplished! 🐙
  α: Type

F: Factory α

m₁, m₂: Meas

FourCases F m₁ m₂case inr h: ?m.1916
h =>
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last = m₂.last ∨ m₂.last < m₁.last

FourCases F m₁ m₂cases h: ?m.1916
hα: Type

F: Factory α

m₁, m₂: Meas

h✝: m₁.last = m₂.last

inlFourCases F m₁ m₂
α: Type

F: Factory α

m₁, m₂: Meas

h✝: m₂.last < m₁.last

inrFourCases F m₁ m₂ 
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last = m₂.last ∨ m₂.last < m₁.last

FourCases F m₁ m₂case inl h': ?m.3530
h' => 
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

FourCases F m₁ m₂simp [h': ?m.3530
h']α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

FourCases F m₁ m₂
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

FourCases F m₁ m₂by_cases F: Factory α
F.le: {α : Type} → Factory α → α → α → Bool
le m₁: Meas
m₁.cost: {α : Type} → Meas → α
cost m₂: Meas
m₂.cost: {α : Type} → Meas → α
cost = true: Bool
trueα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

posFourCases F m₁ m₂
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

negFourCases F m₁ m₂
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

FourCases F m₁ m₂case pos => 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂apply FourCases.first_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, dominates F m₁ m₂ = true → FourCases F m₁ m₂
FourCases.first_domα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

h_domdominates F m₁ m₂ = true 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂case h_dom => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

dominates F m₁ m₂ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = true
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

dominates F m₁ m₂ = truedwi { α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.last ∧ Factory.le F m₁.cost m₂.cost = trueconstructorα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

leftm₁.last ≤ m₂.last
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

rightFactory.le F m₁.cost m₂.cost = true }α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

leftm₁.last ≤ m₂.last 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

dominates F m₁ m₂ = truecase left => α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.lastsimp [h': ?m.3530
h']
Goals accomplished! 🐙
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

FourCases F m₁ m₂case neg =>
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂apply FourCases.second_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, ¬dominates F m₁ m₂ = true → dominates F m₂ m₁ = true → FourCases F m₁ m₂
FourCases.second_domα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h_non_dom¬dominates F m₁ m₂ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h_domdominates F m₂ m₁ = true
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂case h_non_dom =>
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₁.last ≤ m₂.last → Factory.le F m₁.cost m₂.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = trueintroα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

a✝: m₁.last ≤ m₂.last

Factory.le F m₁.cost m₂.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = truesimp at h: ?m.3617
hα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

a✝: m₁.last ≤ m₂.last

h: Factory.le F m₁.cost m₂.cost = false

Factory.le F m₁.cost m₂.cost = false 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

¬dominates F m₁ m₂ = trueassumption
Goals accomplished! 🐙
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

FourCases F m₁ m₂case h_dom => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

dominates F m₂ m₁ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₂.last ≤ m₁.last ∧ Factory.le F m₂.cost m₁.cost = true
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

dominates F m₂ m₁ = trueconstructorα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

leftm₂.last ≤ m₁.last
α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

rightFactory.le F m₂.cost m₁.cost = true
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

dominates F m₂ m₁ = truecase left => 
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₂.last ≤ m₁.lastapply le_of_eq: ∀ {α : Type ?u.5212} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le_of_eqα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

am₂.last = m₁.last
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₂.last ≤ m₁.lastsymmα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

am₁.last = m₂.last
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

m₂.last ≤ m₁.lastassumption
Goals accomplished! 🐙
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

dominates F m₂ m₁ = truecase right => 
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

Factory.le F m₂.cost m₁.cost = trueapply Factory.le_of_lt: ∀ {α : Type} {F : Factory α} {c c' : α}, Factory.lt F c c' → Factory.le F c c' = true
Factory.le_of_ltα: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

h₁Factory.lt F m₂.cost m₁.cost
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

Factory.le F m₂.cost m₁.cost = truecase h₁ => α: Type

F: Factory α

m₁, m₂: Meas

h': m₁.last = m₂.last

h: ¬Factory.le F m₁.cost m₂.cost = true

Factory.lt F m₂.cost m₁.costsimp [← 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, h: ?m.3617
h]
Goals accomplished! 🐙
    α: Type

F: Factory α

m₁, m₂: Meas

h: m₁.last = m₂.last ∨ m₂.last < m₁.last

FourCases F m₁ m₂case inr h': ?m.3531
h' => 
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

FourCases F m₁ m₂by_cases Factory.le: {α : Type} → Factory α → α → α → Bool
Factory.le F: Factory α
F m₂: Meas
m₂.cost: {α : Type} → Meas → α
cost m₁: Meas
m₁.cost: {α : Type} → Meas → α
cost = true: Bool
trueα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

posFourCases F m₁ m₂
α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

negFourCases F m₁ m₂
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

FourCases F m₁ m₂case pos => 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂apply FourCases.second_dom: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas}, ¬dominates F m₁ m₂ = true → dominates F m₂ m₁ = true → FourCases F m₁ m₂
FourCases.second_domα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

h_non_dom¬dominates F m₁ m₂ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

h_domdominates F m₂ m₁ = true 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂case h_non_dom => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

m₁.last ≤ m₂.last → Factory.le F m₁.cost m₂.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = trueintroα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

a✝: m₁.last ≤ m₂.last

Factory.le F m₁.cost m₂.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = truereplace h': ?m.6157
h' := not_le_of_lt: ∀ {α : Type ?u.6158} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le_of_lt h': ?m.3531
h'α: Type

F: Factory α

m₁, m₂: Meas

h: Factory.le F m₂.cost m₁.cost = true

a✝: m₁.last ≤ m₂.last

h': ¬m₁.last ≤ m₂.last

Factory.le F m₁.cost m₂.cost = false 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = truecontradiction
Goals accomplished! 🐙
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂case h_dom => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

dominates F m₂ m₁ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

m₂.last ≤ m₁.last ∧ Factory.le F m₂.cost m₁.cost = true
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

dominates F m₂ m₁ = truedwi { α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

m₂.last ≤ m₁.last ∧ Factory.le F m₂.cost m₁.cost = trueconstructorα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

leftm₂.last ≤ m₁.last
α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

rightFactory.le F m₂.cost m₁.cost = true }α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

leftm₂.last ≤ m₁.last
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

dominates F m₂ m₁ = truecase left => 
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

m₂.last ≤ m₁.lastapply le_of_lt: ∀ {α : Type ?u.6810} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_ltα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

am₂.last < m₁.last 
            α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: Factory.le F m₂.cost m₁.cost = true

m₂.last ≤ m₁.lastassumption
Goals accomplished! 🐙
      α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

FourCases F m₁ m₂case neg => 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂dwi { α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂apply FourCases.first_last: ∀ {α : Type} {F : Factory α} {m₁ m₂ : Meas},
  ¬dominates F m₁ m₂ = true → ¬dominates F m₂ m₁ = true → m₁.last > m₂.last → FourCases F m₁ m₂
FourCases.first_lastα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

h_non_dom₁¬dominates F m₁ m₂ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

h_non_dom₂¬dominates F m₂ m₁ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

hm₁.last > m₂.last }α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

h_non_dom₁¬dominates F m₁ m₂ = true
α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

h_non_dom₂¬dominates F m₂ m₁ = true 
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂case h_non_dom₁ => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

m₁.last ≤ m₂.last → Factory.le F m₁.cost m₂.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = trueintroα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

a✝: m₁.last ≤ m₂.last

Factory.le F m₁.cost m₂.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = truereplace h': ?m.7795
h' := not_le_of_lt: ∀ {α : Type ?u.7796} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le_of_lt h': ?m.3531
h'α: Type

F: Factory α

m₁, m₂: Meas

h: ¬Factory.le F m₂.cost m₁.cost = true

a✝: m₁.last ≤ m₂.last

h': ¬m₁.last ≤ m₂.last

Factory.le F m₁.cost m₂.cost = false 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₁ m₂ = truecontradiction
Goals accomplished! 🐙
        α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

FourCases F m₁ m₂case h_non_dom₂ => 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₂ m₁ = truesimp [dominates: {α : Type} → Factory α → Meas → Meas → Bool
dominates]α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

m₂.last ≤ m₁.last → Factory.le F m₂.cost m₁.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₂ m₁ = trueintroα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

a✝: m₂.last ≤ m₁.last

Factory.le F m₂.cost m₁.cost = false 
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₂ m₁ = truesimp at h: ?m.5396
hα: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

a✝: m₂.last ≤ m₁.last

h: Factory.le F m₂.cost m₁.cost = false

Factory.le F m₂.cost m₁.cost = false
          α: Type

F: Factory α

m₁, m₂: Meas

h': m₂.last < m₁.last

h: ¬Factory.le F m₂.cost m₁.cost = true

¬dominates F m₂ m₁ = trueassumption
Goals accomplished! 🐙
}
Goals accomplished! 🐙