[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d y : α
x : WithBot α
⊢ unbot' d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d
[PROOFSTEP]
induction x using recBotCoe
[GOAL]
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d y : α
⊢ unbot' d ⊥ = y ↔ ⊥ = ↑y ∨ ⊥ = ⊥ ∧ y = d
[PROOFSTEP]
simp [@eq_comm _ d]
[GOAL]
case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d y a✝ : α
⊢ unbot' d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = ⊥ ∧ y = d
[PROOFSTEP]
simp [@eq_comm _ d]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d : α
x : WithBot α
⊢ unbot' d x = d ↔ x = ↑d ∨ x = ⊥
[PROOFSTEP]
simp [unbot'_eq_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d : α
x y : WithBot α
⊢ unbot' d x = unbot' d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d
[PROOFSTEP]
induction y using recBotCoe
[GOAL]
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d : α
x : WithBot α
⊢ unbot' d x = unbot' d ⊥ ↔ x = ⊥ ∨ x = ↑d ∧ ⊥ = ⊥ ∨ x = ⊥ ∧ ⊥ = ↑d
[PROOFSTEP]
simp [unbot'_eq_iff, or_comm]
[GOAL]
case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b d : α
x : WithBot α
a✝ : α
⊢ unbot' d x = unbot' d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = ⊥ ∨ x = ⊥ ∧ ↑a✝ = ↑d
[PROOFSTEP]
simp [unbot'_eq_iff, or_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
x : WithBot α
h : x ≠ ⊥
⊢ ↑(unbot x h) = x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
h : none ≠ ⊥
⊢ ↑(unbot none h) = none
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b val✝ : α
h : Option.some val✝ ≠ ⊥
⊢ ↑(unbot (Option.some val✝) h) = Option.some val✝
[PROOFSTEP]
exact (h rfl).elim
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b val✝ : α
h : Option.some val✝ ≠ ⊥
⊢ ↑(unbot (Option.some val✝) h) = Option.some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
⊢ Option.some a ≤ Option.some b ↔ a ≤ b
[PROOFSTEP]
simp [LE.le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LE α
inst✝ : OrderTop α
o : WithBot α
a : α
ha : a ∈ o
⊢ ∃ b, b ∈ ⊤ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LE α
inst✝ : OrderTop α
a : α
⊢ ∃ b, b ∈ ⊤ ∧ a ≤ b
[PROOFSTEP]
exact ⟨_, rfl, le_top⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
x : α
⊢ ↑a ≤ Option.some x ↔ ∃ b, Option.some x = ↑b ∧ a ≤ b
[PROOFSTEP]
simp [some_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
⊢ ¬∃ b, none = ↑b ∧ a ≤ b
[PROOFSTEP]
simp [none_eq_bot]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : LE α
b : α
⊢ Option.some b ≤ ↑b✝ ↔ ∀ (a : α), Option.some b = ↑a → a ≤ b✝
[PROOFSTEP]
simp [some_eq_coe, coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
⊢ none ≤ ↑b ↔ ∀ (a : α), none = ↑a → a ≤ b
[PROOFSTEP]
simp [none_eq_bot]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : LE α
a : α
b : WithBot α
h : b ≠ ⊥
⊢ a ≤ unbot b h ↔ ↑a ≤ b
[PROOFSTEP]
match b, h with
| some _, _ => simp only [unbot_coe, coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : LE α
a : α
b : WithBot α
h : b ≠ ⊥
val✝ : α
x✝ : ↑val✝ ≠ ⊥
⊢ a ≤ unbot (↑val✝) x✝ ↔ ↑a ≤ ↑val✝
[PROOFSTEP]
simp only [unbot_coe, coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : LE α
a : WithBot α
h : a ≠ ⊥
b : α
⊢ unbot a h ≤ b ↔ a ≤ ↑b
[PROOFSTEP]
match a, h with
| some _, _ => simp only [unbot_coe, coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : LE α
a : WithBot α
h : a ≠ ⊥
b val✝ : α
x✝ : ↑val✝ ≠ ⊥
⊢ unbot (↑val✝) x✝ ≤ b ↔ ↑val✝ ≤ ↑b
[PROOFSTEP]
simp only [unbot_coe, coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LT α
⊢ Option.some a < Option.some b ↔ a < b
[PROOFSTEP]
simp [LT.lt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : LT α
a : WithBot α
b : α
⊢ a < Option.some b ↔ ∃ p, Option.some b = ↑p ∧ a < ↑p
[PROOFSTEP]
simp [some_eq_coe, coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : LT α
a : WithBot α
⊢ ¬∃ p, none = ↑p ∧ a < ↑p
[PROOFSTEP]
simp [none_eq_bot]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : LT α
b : α
⊢ Option.some b < ↑b✝ ↔ ∀ (a : WithBot α), Option.some b = a → a < ↑b✝
[PROOFSTEP]
simp [some_eq_coe, coe_eq_coe, coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LT α
⊢ none < ↑b ↔ ∀ (a : WithBot α), none = a → a < ↑b
[PROOFSTEP]
simp [none_eq_bot, bot_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LT α
⊢ ⊥ < ⊥ ↔ ⊥ ≠ ⊥
[PROOFSTEP]
simpa using not_lt_none ⊥
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LT α
x : α
⊢ ⊥ < ↑x ↔ ↑x ≠ ⊥
[PROOFSTEP]
simp [bot_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ ∀ (a b : WithBot α), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
intros a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : Preorder α
a b : WithBot α
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : Preorder α
b : WithBot α
⊢ none < b ↔ none ≤ b ∧ ¬b ≤ none
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : Preorder α
b : WithBot α
val✝ : α
⊢ Option.some val✝ < b ↔ Option.some val✝ ≤ b ∧ ¬b ≤ Option.some val✝
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ none < none ↔ none ≤ none ∧ ¬none ≤ none
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
val✝ : α
⊢ none < Option.some val✝ ↔ none ≤ Option.some val✝ ∧ ¬Option.some val✝ ≤ none
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
val✝ : α
⊢ Option.some val✝ < none ↔ Option.some val✝ ≤ none ∧ ¬none ≤ Option.some val✝
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
val✝¹ val✝ : α
⊢ Option.some val✝¹ < Option.some val✝ ↔ Option.some val✝¹ ≤ Option.some val✝ ∧ ¬Option.some val✝ ≤ Option.some val✝¹
[PROOFSTEP]
simp [lt_iff_le_not_le]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
val✝ : α
⊢ none < Option.some val✝ ↔ ¬Option.some val✝ ≤ none
[PROOFSTEP]
simp [LE.le, LT.lt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
o₁ o₂ : WithBot α
h₁ : o₁ ≤ o₂
h₂ : o₂ ≤ o₁
⊢ o₁ = o₂
[PROOFSTEP]
cases' o₁ with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
o₂ : WithBot α
h₁ : none ≤ o₂
h₂ : o₂ ≤ none
⊢ none = o₂
[PROOFSTEP]
cases' o₂ with b
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
h₁ h₂ : none ≤ none
⊢ none = none
[PROOFSTEP]
rfl
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
b : α
h₁ : none ≤ Option.some b
h₂ : Option.some b ≤ none
⊢ none = Option.some b
[PROOFSTEP]
rcases h₂ b rfl with ⟨_, ⟨⟩, _⟩
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
o₂ : WithBot α
a : α
h₁ : Option.some a ≤ o₂
h₂ : o₂ ≤ Option.some a
⊢ Option.some a = o₂
[PROOFSTEP]
rcases h₁ a rfl with ⟨b, ⟨⟩, h₁'⟩
[GOAL]
case some.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
a b : α
h₁' : a ≤ b
h₁ : Option.some a ≤ Option.some b
h₂ : Option.some b ≤ Option.some a
⊢ Option.some a = Option.some b
[PROOFSTEP]
rcases h₂ b rfl with ⟨_, ⟨⟩, h₂'⟩
[GOAL]
case some.intro.intro.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : PartialOrder α
src✝ : Preorder (WithBot α) := preorder
a b : α
h₁' : a ≤ b
h₁ : Option.some a ≤ Option.some b
h₂ : Option.some b ≤ Option.some a
h₂' : b ≤ a
⊢ Option.some a = Option.some b
[PROOFSTEP]
rw [le_antisymm h₁' h₂']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((Monotone fun a => map f ↑a) ∧ ∀ (x : α), map f ⊥ ≤ map f ↑x) ↔ Monotone f
[PROOFSTEP]
simp [Monotone]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ⊥ < map f ↑x) ↔ StrictMono f
[PROOFSTEP]
simp [StrictMono, bot_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
x✝ : WithBot α
⊢ map f ⊥ ≤ map f x✝ ↔ ⊥ ≤ x✝
[PROOFSTEP]
simp only [map_bot, bot_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a : α
⊢ map f ↑a ≤ map f ⊥ ↔ ↑a ≤ ⊥
[PROOFSTEP]
simp only [map_coe, map_bot, coe_ne_bot, not_coe_le_bot _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
a b : α
⊢ map f ↑a ≤ map f ↑b ↔ ↑a ≤ ↑b
[PROOFSTEP]
simpa only [map_coe, coe_le_coe] using mono_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝¹ : LE α
inst✝ : OrderBot α
a : WithBot α
b : α
⊢ unbot' ⊥ a ≤ b ↔ a ≤ ↑b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝¹ : LE α
inst✝ : OrderBot α
b : α
⊢ unbot' ⊥ none ≤ b ↔ none ≤ ↑b
[PROOFSTEP]
simp [none_eq_bot, some_eq_coe]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝¹ : LE α
inst✝ : OrderBot α
b val✝ : α
⊢ unbot' ⊥ (Option.some val✝) ≤ b ↔ Option.some val✝ ≤ ↑b
[PROOFSTEP]
simp [none_eq_bot, some_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : LT α
a : WithBot α
b c : α
ha : a ≠ ⊥
⊢ unbot' b a < c ↔ a < ↑c
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : LT α
b c : α
ha : none ≠ ⊥
⊢ unbot' b none < c ↔ none < ↑c
[PROOFSTEP]
exact (ha rfl).elim
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : LT α
b c val✝ : α
ha : Option.some val✝ ≠ ⊥
⊢ unbot' b (Option.some val✝) < c ↔ Option.some val✝ < ↑c
[PROOFSTEP]
rw [some_eq_coe, unbot'_coe, coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ o₂ : WithBot α
a : α
ha : a ∈ o₁
⊢ ∃ b, b ∈ o₁ ⊔ o₂ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₂ : WithBot α
a : α
⊢ ∃ b, b ∈ Option.some a ⊔ o₂ ∧ a ≤ b
[PROOFSTEP]
cases o₂
[GOAL]
case refl.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a : α
⊢ ∃ b, b ∈ Option.some a ⊔ none ∧ a ≤ b
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
case refl.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a val✝ : α
⊢ ∃ b, b ∈ Option.some a ⊔ Option.some val✝ ∧ a ≤ b
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ o₂ : WithBot α
a : α
ha : a ∈ o₂
⊢ ∃ b, b ∈ o₁ ⊔ o₂ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ : WithBot α
a : α
⊢ ∃ b, b ∈ o₁ ⊔ Option.some a ∧ a ≤ b
[PROOFSTEP]
cases o₁
[GOAL]
case refl.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a : α
⊢ ∃ b, b ∈ none ⊔ Option.some a ∧ a ≤ b
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
case refl.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a val✝ : α
⊢ ∃ b, b ∈ Option.some val✝ ⊔ Option.some a ∧ a ≤ b
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ o₂ o₃ : WithBot α
h₁ : o₁ ≤ o₃
h₂ : o₂ ≤ o₃
a : α
ha : a ∈ o₁ ⊔ o₂
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases' o₁ with b
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₂ o₃ : WithBot α
h₂ : o₂ ≤ o₃
a : α
h₁ : none ≤ o₃
ha : a ∈ none ⊔ o₂
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases' o₂ with c
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₂ o₃ : WithBot α
h₂ : o₂ ≤ o₃
a b : α
h₁ : Option.some b ≤ o₃
ha : a ∈ Option.some b ⊔ o₂
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases' o₂ with c
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a : α
h₁ h₂ : none ≤ o₃
ha : a ∈ none ⊔ none
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a : α
h₁ : none ≤ o₃
c : α
h₂ : Option.some c ≤ o₃
ha : a ∈ none ⊔ Option.some c
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a b : α
h₁ : Option.some b ≤ o₃
h₂ : none ≤ o₃
ha : a ∈ Option.some b ⊔ none
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a b : α
h₁ : Option.some b ≤ o₃
c : α
h₂ : Option.some c ≤ o₃
ha : a ∈ Option.some b ⊔ Option.some c
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case none.some.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a : α
h₁ : none ≤ o₃
h₂ : Option.some a ≤ o₃
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
exact h₂ a rfl
[GOAL]
case some.none.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a : α
h₂ : none ≤ o₃
h₁ : Option.some a ≤ o₃
⊢ ∃ b, b ∈ o₃ ∧ a ≤ b
[PROOFSTEP]
exact h₁ a rfl
[GOAL]
case some.some.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
b : α
h₁ : Option.some b ≤ o₃
c : α
h₂ : Option.some c ≤ o₃
⊢ ∃ b_1, b_1 ∈ o₃ ∧ (fun x x_1 => x ⊔ x_1) b c ≤ b_1
[PROOFSTEP]
rcases h₁ b rfl with ⟨d, ⟨⟩, h₁'⟩
[GOAL]
case some.some.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
b c d : α
h₁' : b ≤ d
h₁ : Option.some b ≤ Option.some d
h₂ : Option.some c ≤ Option.some d
⊢ ∃ b_1, b_1 ∈ Option.some d ∧ (fun x x_1 => x ⊔ x_1) b c ≤ b_1
[PROOFSTEP]
simp at h₂ 
[GOAL]
case some.some.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b✝ : α
inst✝ : SemilatticeSup α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
b c d : α
h₁' : b ≤ d
h₁ : Option.some b ≤ Option.some d
h₂ : c ≤ d
⊢ ∃ b_1, b_1 ∈ Option.some d ∧ (fun x x_1 => x ⊔ x_1) b c ≤ b_1
[PROOFSTEP]
exact ⟨d, rfl, sup_le h₁' h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ o₂ : WithBot α
a : α
ha : a ∈ o₁ ⊓ o₂
⊢ ∃ b, b ∈ o₁ ∧ a ≤ b
[PROOFSTEP]
rcases Option.mem_map₂_iff.1 ha with ⟨a, b, (rfl : _ = _), (rfl : _ = _), rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a b : α
ha : a ⊓ b ∈ Option.some a ⊓ Option.some b
⊢ ∃ b_1, b_1 ∈ Option.some a ∧ a ⊓ b ≤ b_1
[PROOFSTEP]
exact ⟨_, rfl, inf_le_left⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ o₂ : WithBot α
a : α
ha : a ∈ o₁ ⊓ o₂
⊢ ∃ b, b ∈ o₂ ∧ a ≤ b
[PROOFSTEP]
rcases Option.mem_map₂_iff.1 ha with ⟨a, b, (rfl : _ = _), (rfl : _ = _), rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a b : α
ha : a ⊓ b ∈ Option.some a ⊓ Option.some b
⊢ ∃ b_1, b_1 ∈ Option.some b ∧ a ⊓ b ≤ b_1
[PROOFSTEP]
exact ⟨_, rfl, inf_le_right⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₁ o₂ o₃ : WithBot α
h₁ : o₁ ≤ o₂
h₂ : o₁ ≤ o₃
a : α
ha : a ∈ o₁
⊢ ∃ b, b ∈ o₂ ⊓ o₃ ∧ a ≤ b
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₂ o₃ : WithBot α
a : α
h₁ : Option.some a ≤ o₂
h₂ : Option.some a ≤ o₃
⊢ ∃ b, b ∈ o₂ ⊓ o₃ ∧ a ≤ b
[PROOFSTEP]
rcases h₁ a rfl with ⟨b, ⟨⟩, ab⟩
[GOAL]
case refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
o₃ : WithBot α
a : α
h₂ : Option.some a ≤ o₃
b : α
ab : a ≤ b
h₁ : Option.some a ≤ Option.some b
⊢ ∃ b_1, b_1 ∈ Option.some b ⊓ o₃ ∧ a ≤ b_1
[PROOFSTEP]
rcases h₂ a rfl with ⟨c, ⟨⟩, ac⟩
[GOAL]
case refl.intro.intro.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝ : SemilatticeInf α
src✝¹ : PartialOrder (WithBot α) := partialOrder
src✝ : OrderBot (WithBot α) := orderBot
a b : α
ab : a ≤ b
h₁ : Option.some a ≤ Option.some b
c : α
ac : a ≤ c
h₂ : Option.some a ≤ Option.some c
⊢ ∃ b_1, b_1 ∈ Option.some b ⊓ Option.some c ∧ a ≤ b_1
[PROOFSTEP]
exact ⟨_, rfl, le_inf ab ac⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
h : ¬x ≤ y
⊢ ¬(fun x x_1 => x ≤ x_1) (Option.some x) (Option.some y)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
h : (fun x x_1 => x ≤ x_1) (Option.some x) none
⊢ False
[PROOFSTEP]
rcases h x rfl with ⟨y, ⟨_⟩, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : DecidableRel fun x x_1 => x < x_1
x : α
⊢ (fun x x_1 => x < x_1) none (Option.some x)
[PROOFSTEP]
exists x, rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : DecidableRel fun x x_1 => x < x_1
x : α
⊢ ∀ (a : α), a ∈ none → a < x
[PROOFSTEP]
rintro _ ⟨⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
h : x < y
⊢ (fun x x_1 => x < x_1) (Option.some x) (Option.some y)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
h : ¬x < y
⊢ ¬(fun x x_1 => x < x_1) (Option.some x) (Option.some y)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : DecidableRel fun x x_1 => x < x_1
x : WithBot α
⊢ ¬(fun x x_1 => x < x_1) x none
[PROOFSTEP]
rintro ⟨a, ⟨⟨⟩⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LT α
h : WellFounded fun x x_1 => x < x_1
not_lt_bot : ∀ (a : WithBot α), ¬a < ⊥
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun x x_1 => x < x_1) y
[PROOFSTEP]
simp [not_lt_bot]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
⊢ ∀ (a : WithBot α), ∃ b, ¬b ≤ a
[PROOFSTEP]
apply recBotCoe
[GOAL]
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
⊢ ∃ b, ¬b ≤ ⊥
[PROOFSTEP]
exact ‹Nonempty α›.elim fun a => ⟨a, not_coe_le_bot a⟩
[GOAL]
case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
⊢ ∀ (a : α), ∃ b, ¬b ≤ ↑a
[PROOFSTEP]
intro a
[GOAL]
case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
a : α
⊢ ∃ b, ¬b ≤ ↑a
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_not_le a
[GOAL]
case coe.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
a b : α
h : ¬b ≤ a
⊢ ∃ b, ¬b ≤ ↑a
[PROOFSTEP]
exact ⟨b, by rwa [coe_le_coe]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
a b : α
h : ¬b ≤ a
⊢ ¬↑b ≤ ↑a
[PROOFSTEP]
rwa [coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
⊢ ∀ (a : WithBot α), ∃ b, a < b
[PROOFSTEP]
apply WithBot.recBotCoe
[GOAL]
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
⊢ ∃ b, ⊥ < b
[PROOFSTEP]
apply ‹Nonempty α›.elim
[GOAL]
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
⊢ α → ∃ b, ⊥ < b
[PROOFSTEP]
exact fun a => ⟨a, WithBot.bot_lt_coe a⟩
[GOAL]
case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
⊢ ∀ (a : α), ∃ b, ↑a < b
[PROOFSTEP]
intro a
[GOAL]
case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
a : α
⊢ ∃ b, ↑a < b
[PROOFSTEP]
obtain ⟨b, ha⟩ := exists_gt a
[GOAL]
case coe.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b✝ : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
a b : α
ha : a < b
⊢ ∃ b, ↑a < b
[PROOFSTEP]
exact ⟨b, coe_lt_coe.mpr ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
⊢ ↑a ≤ ↑b ↔ a ≤ b
[PROOFSTEP]
simp only [← toDual_le_toDual_iff, toDual_apply_coe, WithBot.coe_le_coe, toDual_le_toDual]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LE α
inst✝ : OrderBot α
o : WithTop α
a : α
ha : a ∈ o
⊢ ∃ b, b ∈ ⊥ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LE α
inst✝ : OrderBot α
a : α
⊢ ∃ b, b ∈ ⊥ ∧ b ≤ a
[PROOFSTEP]
exact ⟨_, rfl, bot_le⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
intro _ hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
h : IsMin a
b✝ : WithTop α
hb : b✝ ≤ ↑a
⊢ ↑a ≤ b✝
[PROOFSTEP]
rw [← toDual_le_toDual_iff] at hb 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : LE α
h : IsMin a
b✝ : WithTop α
hb : ↑WithTop.toDual ↑a ≤ ↑WithTop.toDual b✝
⊢ ↑a ≤ b✝
[PROOFSTEP]
simpa [toDual_le_iff] using (IsMax.withBot h : IsMax (toDual a : WithBot αᵒᵈ)) hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a b : α
⊢ ↑a < ↑b ↔ a < b
[PROOFSTEP]
simp only [← toDual_lt_toDual_iff, toDual_apply_coe, WithBot.coe_lt_coe, toDual_lt_toDual]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a✝ b a : α
⊢ ↑a < ⊤
[PROOFSTEP]
simp [← toDual_lt_toDual_iff, WithBot.bot_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a✝ b : α
a : WithTop α
⊢ ¬none < a
[PROOFSTEP]
rw [← toDual_lt_toDual_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a✝ b : α
a : WithTop α
⊢ ¬↑WithTop.toDual a < ↑WithTop.toDual none
[PROOFSTEP]
exact WithBot.not_lt_none _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a✝ b✝ : α
a b : WithTop α
⊢ a < b ↔ ∃ p, a = ↑p ∧ ↑p < b
[PROOFSTEP]
rw [← toDual_lt_toDual_iff, WithBot.lt_iff_exists_coe, OrderDual.exists]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a✝ b✝ : α
a b : WithTop α
⊢ (∃ a_1, ↑WithTop.toDual a = ↑(↑toDual a_1) ∧ ↑WithTop.toDual b < ↑(↑toDual a_1)) ↔ ∃ p, a = ↑p ∧ ↑p < b
[PROOFSTEP]
exact exists_congr fun _ => and_congr_left' Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
a b : α
x : WithTop α
⊢ ↑a < x ↔ ∀ (b : WithTop α), x = b → ↑a < b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Preorder α
x✝² x✝¹ x✝ : WithTop α
⊢ x✝² ≤ x✝¹ → x✝¹ ≤ x✝ → x✝² ≤ x✝
[PROOFSTEP]
simp_rw [← toDual_le_toDual_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Preorder α
x✝² x✝¹ x✝ : WithTop α
⊢ ↑WithTop.toDual x✝¹ ≤ ↑WithTop.toDual x✝² →
    ↑WithTop.toDual x✝ ≤ ↑WithTop.toDual x✝¹ → ↑WithTop.toDual x✝ ≤ ↑WithTop.toDual x✝²
[PROOFSTEP]
exact Function.swap le_trans
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Preorder α
⊢ ∀ (a b : WithTop α), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
simp [← toDual_lt_toDual_iff, lt_iff_le_not_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : PartialOrder α
src✝ : Preorder (WithTop α) := preorder
x✝¹ x✝ : WithTop α
⊢ x✝¹ ≤ x✝ → x✝ ≤ x✝¹ → x✝¹ = x✝
[PROOFSTEP]
simp_rw [← toDual_le_toDual_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : PartialOrder α
src✝ : Preorder (WithTop α) := preorder
x✝¹ x✝ : WithTop α
⊢ ↑WithTop.toDual x✝ ≤ ↑WithTop.toDual x✝¹ → ↑WithTop.toDual x✝¹ ≤ ↑WithTop.toDual x✝ → x✝¹ = x✝
[PROOFSTEP]
exact Function.swap le_antisymm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((Monotone fun a => map f ↑a) ∧ ∀ (x : α), map f ↑x ≤ map f ⊤) ↔ Monotone f
[PROOFSTEP]
simp [Monotone]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ↑x < map f ⊤) ↔ StrictMono f
[PROOFSTEP]
simp [StrictMono, coe_lt_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
a b : WithTop α
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f a ≤ map f b ↔ a ≤ b
[PROOFSTEP]
erw [← toDual_le_toDual_iff, toDual_map, toDual_map, WithBot.map_le_iff, toDual_le_toDual_iff]
[GOAL]
case mono_iff
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
a b : WithTop α
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ ∀ {a b : αᵒᵈ}, (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual) a ≤ (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual) b ↔ a ≤ b
[PROOFSTEP]
simp [mono_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ : WithTop α
a : α
ha : a ∈ o₁
⊢ ∃ b, b ∈ o₁ ⊓ o₂ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₂ : WithTop α
a : α
⊢ ∃ b, b ∈ Option.some a ⊓ o₂ ∧ b ≤ a
[PROOFSTEP]
cases o₂
[GOAL]
case refl.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
a : α
⊢ ∃ b, b ∈ Option.some a ⊓ none ∧ b ≤ a
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
case refl.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
a val✝ : α
⊢ ∃ b, b ∈ Option.some a ⊓ Option.some val✝ ∧ b ≤ a
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ : WithTop α
a : α
ha : a ∈ o₂
⊢ ∃ b, b ∈ o₁ ⊓ o₂ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a : α
⊢ ∃ b, b ∈ o₁ ⊓ Option.some a ∧ b ≤ a
[PROOFSTEP]
cases o₁
[GOAL]
case refl.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
a : α
⊢ ∃ b, b ∈ none ⊓ Option.some a ∧ b ≤ a
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
case refl.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
a val✝ : α
⊢ ∃ b, b ∈ Option.some val✝ ⊓ Option.some a ∧ b ≤ a
[PROOFSTEP]
simp [Option.liftOrGet]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ o₃ : WithTop α
h₁ : o₁ ≤ o₂
h₂ : o₁ ≤ o₃
a : α
ha : a ∈ o₂ ⊓ o₃
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases' o₂ with b
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₃ : WithTop α
h₂ : o₁ ≤ o₃
a : α
h₁ : o₁ ≤ none
ha : a ∈ none ⊓ o₃
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases' o₃ with c
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₃ : WithTop α
h₂ : o₁ ≤ o₃
a b : α
h₁ : o₁ ≤ Option.some b
ha : a ∈ Option.some b ⊓ o₃
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases' o₃ with c
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a : α
h₁ h₂ : o₁ ≤ none
ha : a ∈ none ⊓ none
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a : α
h₁ : o₁ ≤ none
c : α
h₂ : o₁ ≤ Option.some c
ha : a ∈ none ⊓ Option.some c
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a b : α
h₁ : o₁ ≤ Option.some b
h₂ : o₁ ≤ none
ha : a ∈ Option.some b ⊓ none
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a b : α
h₁ : o₁ ≤ Option.some b
c : α
h₂ : o₁ ≤ Option.some c
ha : a ∈ Option.some b ⊓ Option.some c
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case none.some.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a : α
h₁ : o₁ ≤ none
h₂ : o₁ ≤ Option.some a
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
exact h₂ a rfl
[GOAL]
case some.none.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
a : α
h₂ : o₁ ≤ none
h₁ : o₁ ≤ Option.some a
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
exact h₁ a rfl
[GOAL]
case some.some.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ : WithTop α
b : α
h₁ : o₁ ≤ Option.some b
c : α
h₂ : o₁ ≤ Option.some c
⊢ ∃ b_1, b_1 ∈ o₁ ∧ b_1 ≤ (fun x x_1 => x ⊓ x_1) b c
[PROOFSTEP]
rcases h₁ b rfl with ⟨d, ⟨⟩, h₁'⟩
[GOAL]
case some.some.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
b c d : α
h₁' : d ≤ b
h₁ : Option.some d ≤ Option.some b
h₂ : Option.some d ≤ Option.some c
⊢ ∃ b_1, b_1 ∈ Option.some d ∧ b_1 ≤ (fun x x_1 => x ⊓ x_1) b c
[PROOFSTEP]
simp at h₂ 
[GOAL]
case some.some.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeInf α
src✝ : PartialOrder (WithTop α) := partialOrder
b c d : α
h₁' : d ≤ b
h₁ : Option.some d ≤ Option.some b
h₂ : d ≤ c
⊢ ∃ b_1, b_1 ∈ Option.some d ∧ b_1 ≤ (fun x x_1 => x ⊓ x_1) b c
[PROOFSTEP]
exact ⟨d, rfl, le_inf h₁' h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ : WithTop α
a : α
ha : a ∈ o₁ ⊔ o₂
⊢ ∃ b, b ∈ o₁ ∧ b ≤ a
[PROOFSTEP]
rcases Option.mem_map₂_iff.1 ha with ⟨a, b, (rfl : _ = _), (rfl : _ = _), rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
a b : α
ha : a ⊔ b ∈ Option.some a ⊔ Option.some b
⊢ ∃ b_1, b_1 ∈ Option.some a ∧ b_1 ≤ a ⊔ b
[PROOFSTEP]
exact ⟨_, rfl, le_sup_left⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ : WithTop α
a : α
ha : a ∈ o₁ ⊔ o₂
⊢ ∃ b, b ∈ o₂ ∧ b ≤ a
[PROOFSTEP]
rcases Option.mem_map₂_iff.1 ha with ⟨a, b, (rfl : _ = _), (rfl : _ = _), rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
a b : α
ha : a ⊔ b ∈ Option.some a ⊔ Option.some b
⊢ ∃ b_1, b_1 ∈ Option.some b ∧ b_1 ≤ a ⊔ b
[PROOFSTEP]
exact ⟨_, rfl, le_sup_right⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ o₃ : WithTop α
h₁ : o₁ ≤ o₃
h₂ : o₂ ≤ o₃
a : α
ha : a ∈ o₃
⊢ ∃ b, b ∈ o₁ ⊔ o₂ ∧ b ≤ a
[PROOFSTEP]
cases ha
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
o₁ o₂ : WithTop α
a : α
h₁ : o₁ ≤ Option.some a
h₂ : o₂ ≤ Option.some a
⊢ ∃ b, b ∈ o₁ ⊔ o₂ ∧ b ≤ a
[PROOFSTEP]
rcases h₁ a rfl with ⟨b, ⟨⟩, ab⟩
[GOAL]
case refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
o₂ : WithTop α
a : α
h₂ : o₂ ≤ Option.some a
b : α
ab : b ≤ a
h₁ : Option.some b ≤ Option.some a
⊢ ∃ b_1, b_1 ∈ Option.some b ⊔ o₂ ∧ b_1 ≤ a
[PROOFSTEP]
rcases h₂ a rfl with ⟨c, ⟨⟩, ac⟩
[GOAL]
case refl.intro.intro.refl.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : SemilatticeSup α
src✝ : PartialOrder (WithTop α) := partialOrder
a b : α
ab : b ≤ a
h₁ : Option.some b ≤ Option.some a
c : α
ac : c ≤ a
h₂ : Option.some c ≤ Option.some a
⊢ ∃ b_1, b_1 ∈ Option.some b ⊔ Option.some c ∧ b_1 ≤ a
[PROOFSTEP]
exact ⟨_, rfl, sup_le ab ac⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LE α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x✝¹ x✝ : WithTop α
⊢ x✝¹ ≤ x✝ ∨ x✝ ≤ x✝¹
[PROOFSTEP]
simp_rw [← toDual_le_toDual_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LE α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x✝¹ x✝ : WithTop α
⊢ ↑WithTop.toDual x✝ ≤ ↑WithTop.toDual x✝¹ ∨ ↑WithTop.toDual x✝¹ ≤ ↑WithTop.toDual x✝
[PROOFSTEP]
exact total_of _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
have : Acc (· < ·) (WithTop.toDual a) := WellFounded.apply (WithBot.wellFounded_lt (by convert h using 1)) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
convert h using 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
this : Acc (fun x x_1 => x < x_1) (↑WithTop.toDual a)
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
revert this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
⊢ Acc (fun x x_1 => x < x_1) (↑WithTop.toDual a) → Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
generalize ha : WithBot.toDual a = b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a = b
⊢ Acc (fun x x_1 => x < x_1) b → Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
intro ac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a = b
ac : Acc (fun x x_1 => x < x_1) b
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
dsimp at ac 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithTop α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a = b
ac : Acc (fun x x_1 => x < x_1) b
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
induction' ac with _ H IH generalizing a
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a✝ : WithTop α
b : WithTop αᵒᵈ
ha✝ : ↑WithBot.toDual a✝ = b
x✝ : WithTop αᵒᵈ
H : ∀ (y : WithTop αᵒᵈ), y < x✝ → Acc (fun x x_1 => x < x_1) y
IH : ∀ (y : WithTop αᵒᵈ), y < x✝ → ∀ (a : WithTop α), ↑WithBot.toDual a = y → Acc (fun x x_1 => x > x_1) a
a : WithTop α
ha : ↑WithBot.toDual a = x✝
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
subst ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a✝ : WithTop α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a✝ = b
a : WithTop α
H : ∀ (y : WithTop αᵒᵈ), y < ↑WithBot.toDual a → Acc (fun x x_1 => x < x_1) y
IH :
  ∀ (y : WithTop αᵒᵈ), y < ↑WithBot.toDual a → ∀ (a : WithTop α), ↑WithBot.toDual a = y → Acc (fun x x_1 => x > x_1) a
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
exact ⟨_, fun a' h => IH (WithTop.toDual a') (toDual_lt_toDual.mpr h) _ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
have : Acc (· < ·) (WithBot.toDual a) := WellFounded.apply (WithTop.wellFounded_lt (by convert h using 1)) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
convert h using 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
this : Acc (fun x x_1 => x < x_1) (↑WithBot.toDual a)
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
revert this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
⊢ Acc (fun x x_1 => x < x_1) (↑WithBot.toDual a) → Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
generalize ha : WithBot.toDual a = b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a = b
⊢ Acc (fun x x_1 => x < x_1) b → Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
intro ac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a = b
ac : Acc (fun x x_1 => x < x_1) b
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
dsimp at ac 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a : WithBot α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a = b
ac : Acc (fun x x_1 => x < x_1) b
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
induction' ac with _ H IH generalizing a
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a✝ : WithBot α
b : WithTop αᵒᵈ
ha✝ : ↑WithBot.toDual a✝ = b
x✝ : WithTop αᵒᵈ
H : ∀ (y : WithTop αᵒᵈ), y < x✝ → Acc (fun x x_1 => x < x_1) y
IH : ∀ (y : WithTop αᵒᵈ), y < x✝ → ∀ (a : WithBot α), ↑WithBot.toDual a = y → Acc (fun x x_1 => x > x_1) a
a : WithBot α
ha : ↑WithBot.toDual a = x✝
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
subst ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LT α
h : WellFounded fun x x_1 => x > x_1
a✝ : WithBot α
b : WithTop αᵒᵈ
ha : ↑WithBot.toDual a✝ = b
a : WithBot α
H : ∀ (y : WithTop αᵒᵈ), y < ↑WithBot.toDual a → Acc (fun x x_1 => x < x_1) y
IH :
  ∀ (y : WithTop αᵒᵈ), y < ↑WithBot.toDual a → ∀ (a : WithBot α), ↑WithBot.toDual a = y → Acc (fun x x_1 => x > x_1) a
⊢ Acc (fun x x_1 => x > x_1) a
[PROOFSTEP]
exact ⟨_, fun a' h => IH (WithBot.toDual a') (toDual_lt_toDual.mpr h) _ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x < x_1
⊢ ∀ (a b : WithTop α), a < b ∨ a = b ∨ b < a
[PROOFSTEP]
rintro (a | a) (b | b)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x < x_1
⊢ none < none ∨ none = none ∨ none < none
[PROOFSTEP]
simp
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x < x_1
b : α
⊢ none < Option.some b ∨ none = Option.some b ∨ Option.some b < none
[PROOFSTEP]
simp
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x < x_1
a : α
⊢ Option.some a < none ∨ Option.some a = none ∨ none < Option.some a
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x < x_1
a b : α
⊢ Option.some a < Option.some b ∨ Option.some a = Option.some b ∨ Option.some b < Option.some a
[PROOFSTEP]
simpa [some_eq_coe, IsTrichotomous, coe_eq_coe] using @trichotomous α (· < ·) _ a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x > x_1
⊢ ∀ (a b : WithTop α), a > b ∨ a = b ∨ b > a
[PROOFSTEP]
rintro (a | a) (b | b)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x > x_1
⊢ none > none ∨ none = none ∨ none > none
[PROOFSTEP]
simp
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x > x_1
b : α
⊢ none > Option.some b ∨ none = Option.some b ∨ Option.some b > none
[PROOFSTEP]
simp
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x > x_1
a : α
⊢ Option.some a > none ∨ Option.some a = none ∨ none > Option.some a
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : IsTrichotomous α fun x x_1 => x > x_1
a b : α
⊢ Option.some a > Option.some b ∨ Option.some a = Option.some b ∨ Option.some b > Option.some a
[PROOFSTEP]
simpa [some_eq_coe, IsTrichotomous, coe_eq_coe] using @trichotomous α (· > ·) _ a b
