[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


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : β ≃o γ
y : γ
⊢ IsLUB {x | (↑e ∘ f) x ≤ y} ((g ∘ ↑(OrderIso.symm e)) y)
[PROOFSTEP]
simpa [e.le_symm_apply] using h (e.symm y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
⊢ IsOrderRightAdjoint (f ∘ ↑e) (↑(OrderIso.symm e) ∘ g)
[PROOFSTEP]
intro y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | (f ∘ ↑e) x ≤ y} ((↑(OrderIso.symm e) ∘ g) y)
[PROOFSTEP]
change IsLUB (e ⁻¹' {x | f x ≤ y}) (e.symm (g y))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB (↑e ⁻¹' {x | f x ≤ y}) (↑(OrderIso.symm e) (g y))
[PROOFSTEP]
rw [e.isLUB_preimage, e.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | f x ≤ y} (g y)
[PROOFSTEP]
exact h y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' ↑fb ↑fa
[PROOFSTEP]
refine' fun y => (hg' _).unique _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ ↑fb y} (↑fa (g' y))
[PROOFSTEP]
rw [← fa.surjective.image_preimage {x | g x ≤ fb y}, preimage_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (↑fa '' {a | g (↑fa a) ≤ ↑fb y}) (↑fa (g' y))
[PROOFSTEP]
simp only [h.eq, fb.le_iff_le, fa.leftOrdContinuous (hg' _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
⊢ Semiconj h ↑(↑f₂ g) ↑(↑f₁ g)
[PROOFSTEP]
refine' fun y => (H _).unique _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
y : α
⊢ IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') (↑(↑f₂ g) y))) (↑(↑f₁ g) (h y))
[PROOFSTEP]
have := (f₁ g).leftOrdContinuous (H y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (↑(↑f₁ g) '' range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') y)) (↑(↑f₁ g) (h y))
⊢ IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') (↑(↑f₂ g) y))) (↑(↑f₁ g) (h y))
[PROOFSTEP]
rw [← range_comp, ← (Equiv.mulRight g).surjective.range_comp _] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (range ((↑(↑f₁ g) ∘ fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') y)) ∘ ↑(Equiv.mulRight g))) (↑(↑f₁ g) (h y))
⊢ IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') (↑(↑f₂ g) y))) (↑(↑f₁ g) (h y))
[PROOFSTEP]
simpa [(· ∘ ·)] using this


[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
⊢ Unbounded (fun x x_1 => x ≤ x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a < b
[PROOFSTEP]
simp only [Unbounded, not_le]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
⊢ Unbounded (fun x x_1 => x < x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b
[PROOFSTEP]
simp only [Unbounded, not_lt]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ Bounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
refine' ⟨fun h => _, bounded_le_of_bounded_lt⟩
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
h : Bounded (fun x x_1 => x ≤ x_1) s
⊢ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
cases' h with a ha
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun x x_1 => x ≤ x_1) b a
⊢ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
cases' exists_gt a with b hb
[GOAL]
case intro.intro
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun x x_1 => x ≤ x_1) b a
b : α
hb : a < b
⊢ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
exact ⟨b, fun c hc => lt_of_le_of_lt (ha c hc) hb⟩
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ Unbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
simp_rw [← not_bounded_iff, bounded_le_iff_bounded_lt]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x x_1 => x < x_1) (Iic a)
[PROOFSTEP]
simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
a : α
⊢ Bounded (fun x x_1 => x > x_1) (Ici a)
[PROOFSTEP]
simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) ↔ Bounded r s
[PROOFSTEP]
refine' ⟨_, Bounded.mono (Set.inter_subset_left s _)⟩
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) → Bounded r s
[PROOFSTEP]
rintro ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
s t : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b | ¬r b a} → r b_1 b
⊢ Bounded r s
[PROOFSTEP]
cases' H a b with m hm
[GOAL]
case intro.intro
α : Type u_1
r : α → α → Prop
s t : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b | ¬r b a} → r b_1 b
m : α
hm : ∀ (c : α), r c a ∨ r c b → r c m
⊢ Bounded r s
[PROOFSTEP]
exact ⟨m, fun c hc => hm c (or_iff_not_imp_left.2 fun hca => hb c ⟨hc, hca⟩)⟩
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s
[PROOFSTEP]
simp_rw [← not_bounded_iff, bounded_inter_not H]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | ¬b ≤ a}) ↔ Unbounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | ¬b ≤ a}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
exact bounded_le_inter_not_le a
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
simp_rw [← not_le, bounded_le_inter_not_le]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Unbounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
convert @unbounded_le_inter_not_le _ s _ a
[GOAL]
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a < x✝ ↔ ¬x✝ ≤ a
[PROOFSTEP]
exact lt_iff_not_le
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
refine' ⟨_, Bounded.mono (Set.inter_subset_left s _)⟩
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
rw [← @bounded_le_inter_lt _ s _ a]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b})
[PROOFSTEP]
exact Bounded.mono fun x ⟨hx, hx'⟩ => ⟨hx, le_of_lt hx'⟩
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
exact bounded_le_inter_le a
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Unbounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Unbounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : SemilatticeSup α
a : α
⊢ Bounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
exact bounded_lt_inter_not_lt a
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x < x_1) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
convert @bounded_lt_inter_not_lt _ s _ a
[GOAL]
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a ≤ x✝ ↔ ¬x✝ < a
[PROOFSTEP]
exact not_lt.symm
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x x_1 => x < x_1) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
convert @unbounded_lt_inter_not_lt _ s _ a
[GOAL]
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a ≤ x✝ ↔ ¬x✝ < a
[PROOFSTEP]
exact not_lt.symm
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
[PROOFSTEP]
exact bounded_le_inter_lt a
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Unbounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Unbounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
[GOAL]
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x < x_1) s
[PROOFSTEP]
exact bounded_lt_inter_lt a


[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
b : β
⊢ b ∈ upperBounds (l '' s) ↔ b ∈ u ⁻¹' upperBounds s
[PROOFSTEP]
simp [upperBounds, gc _ _]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
x✝ : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
⊢ u x ∈ upperBounds s
[PROOFSTEP]
rwa [gc.upperBounds_l_image] at hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s
[PROOFSTEP]
rwa [gc.upperBounds_l_image] at hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y
[PROOFSTEP]
rintro rfl x
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y
[PROOFSTEP]
exact (gc x y).symm
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z
[PROOFSTEP]
exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
⊢ l x = z ↔ ∀ (y : β), z ≤ y ↔ x ≤ u y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
⊢ l x = z → ∀ (y : β), z ≤ y ↔ x ≤ u y
[PROOFSTEP]
rintro rfl y
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
y : β
⊢ l x ≤ y ↔ x ≤ u y
[PROOFSTEP]
exact gc x y
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
⊢ (∀ (y : β), z ≤ y ↔ x ≤ u y) → l x = z
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
H : ∀ (y : β), z ≤ y ↔ x ≤ u y
⊢ l x = z
[PROOFSTEP]
exact ((gc _ _).mpr <| (H z).mp le_rfl).antisymm ((H <| l x).mpr (gc.le_u_l x))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ IsLUB (l '' {a₁, a₂}) (l a₁ ⊔ l a₂)
[PROOFSTEP]
simp only [image_pair, isLUB_pair]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))
[PROOFSTEP]
rw [range_comp, ← sSup_range]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))
[PROOFSTEP]
exact gc.isLUB_l_image (isLUB_sSup _)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), l (f i j)
[PROOFSTEP]
simp_rw [gc.l_iSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
⊢ l (sSup s) = ⨆ (a : α) (_ : a ∈ s), l a
[PROOFSTEP]
simp only [sSup_eq_iSup, gc.l_iSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
⊢ GaloisConnection (l2 ∘ l1) (u1 ∘ u2)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
a : α
b : γ
⊢ (l2 ∘ l1) a ≤ b ↔ a ≤ (u1 ∘ u2) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
a : α
b : γ
⊢ l2 (l1 a) ≤ b ↔ a ≤ u1 (u2 b)
[PROOFSTEP]
rw [gc2, gc1]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
[PROOFSTEP]
rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)
[PROOFSTEP]
simp_rw [sSup_image2, ← (h₂ _).l_sSup, ← (h₁ _).l_sSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (l₁ b) (swap u b)
h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)
⊢ sInf (image2 u s t) = u (sInf s) (sInf t)
[PROOFSTEP]
simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (↑e ⁻¹' s) ↔ BddAbove s
[PROOFSTEP]
rw [← e.bddAbove_image, e.image_preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddBelow (↑e ⁻¹' s) ↔ BddBelow s
[PROOFSTEP]
rw [← e.bddBelow_image, e.image_preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b
[PROOFSTEP]
simp only [gi.l_u_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ (i : ι) (hi : p i), u (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi
[PROOFSTEP]
simp only [iSup_subtype', gi.l_iSup_u]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sSup (u '' s)) = sSup s
[PROOFSTEP]
rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
gi : GaloisInsertion l u
a b : β
⊢ l (u (a ⊓ b)) = a ⊓ b
[PROOFSTEP]
simp only [gi.l_u_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨅ (i : ι) (hi : p i), u (f i hi)) = ⨅ (i : ι) (hi : p i), f i hi
[PROOFSTEP]
simp only [iInf_subtype', gi.l_iInf_u]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s
[PROOFSTEP]
rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
f : ι → α
hf : ∀ (i : ι), u (l (f i)) = f i
⊢ l (⨅ (i : ι), f i) = l (⨅ (i : ι), u (l (f i)))
[PROOFSTEP]
simp [hf]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (i : ι) (hi : p i), f i hi) = ⨅ (i : ι) (hi : p i), l (f i hi)
[PROOFSTEP]
rw [iInf_subtype', iInf_subtype']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (x : { i // p i }), f ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), l (f ↑x (_ : p ↑x))
[PROOFSTEP]
exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), a ⊓ b ≤ a
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a
[PROOFSTEP]
exact fun a b => gi.gc.l_le inf_le_left
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), a ⊓ b ≤ b
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b
[PROOFSTEP]
exact fun a b => gi.gc.l_le inf_le_right
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)
[PROOFSTEP]
exact fun a b c hac hbc =>
  (gi.le_l_u a).trans <| gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ ⊤
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤
[PROOFSTEP]
exact fun b => (gi.le_l_u b).trans (gi.gc.monotone_l le_top)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), a ∈ s → sInf s ≤ a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), a ∈ s → choice gi (sInf (u '' s)) (_ : u (l (sInf (u '' s))) ≤ sInf (u '' s)) ≤ a
[PROOFSTEP]
rw [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), a ∈ s → l (sInf (u '' s)) ≤ a
[PROOFSTEP]
exact (gi.isGLB_of_u_image (isGLB_sInf _)).1
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), (∀ (b : β), b ∈ s → a ≤ b) → a ≤ sInf s
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), (∀ (b : β), b ∈ s → a ≤ b) → a ≤ choice gi (sInf (u '' s)) (_ : u (l (sInf (u '' s))) ≤ sInf (u '' s))
[PROOFSTEP]
rw [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), (∀ (b : β), b ∈ s → a ≤ b) → a ≤ l (sInf (u '' s))
[PROOFSTEP]
exact (gi.isGLB_of_u_image (isGLB_sInf _)).2
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeInf β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ a ⊓ b ≤ a
[PROOFSTEP]
exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_left a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeInf β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ a ⊓ b ≤ b
[PROOFSTEP]
exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_right a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeInf β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeSup β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ a ≤ a ⊔ b
[PROOFSTEP]
exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_left a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeSup β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ b ≤ a ⊔ b
[PROOFSTEP]
exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_right a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeSup β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b c : α
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c
[PROOFSTEP]
exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).sup_le a b c