[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
by_cases H : ∀ a : α, ∃ b, ¬b ≤ a
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
exact PSum.inr ⟨H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ¬∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
letI : Top α := ⟨Classical.choose H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
this : Top α := { top := Classical.choose H }
⊢ OrderTop α ⊕' NoTopOrder α
[PROOFSTEP]
exact PSum.inl ⟨Classical.choose_spec H⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ f a
[PROOFSTEP]
rw [h_top]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
[PROOFSTEP]
cases PartialOrder.ext H
[GOAL]
case refl
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
[PROOFSTEP]
apply top_unique
[GOAL]
case refl.h
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤
[PROOFSTEP]
exact @le_top _ _ A _
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : OrderTop α
⊢ A = B
[PROOFSTEP]
rcases A with ⟨ha⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
B : OrderTop α
toTop✝ : Top α
ha : ∀ (a : α), a ≤ ⊤
⊢ mk ha = B
[PROOFSTEP]
rcases B with ⟨hb⟩
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ mk ha = mk hb
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toTop
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ toTop✝¹ = toTop✝
[PROOFSTEP]
ext
[GOAL]
case mk.mk.e_toTop.top
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ ⊤ = ⊤
[PROOFSTEP]
exact le_antisymm (hb _) (ha _)
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
by_cases H : ∀ a : α, ∃ b, ¬a ≤ b
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬a ≤ b
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
exact PSum.inr ⟨H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ¬∀ (a : α), ∃ b, ¬a ≤ b
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), a ≤ b
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
letI : Bot α := ⟨Classical.choose H⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : LE α
H : ∃ a, ∀ (b : α), a ≤ b
this : Bot α := { bot := Classical.choose H }
⊢ OrderBot α ⊕' NoBotOrder α
[PROOFSTEP]
exact PSum.inl ⟨Classical.choose_spec H⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p
[PROOFSTEP]
rw [h_bot]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p
[PROOFSTEP]
exact bot_le
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A : OrderBot α
hB : PartialOrder α
B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
[PROOFSTEP]
cases PartialOrder.ext H
[GOAL]
case refl
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
[PROOFSTEP]
apply bot_unique
[GOAL]
case refl.h
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ ≤ ⊥
[PROOFSTEP]
exact @bot_le _ _ A _
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : OrderBot α
⊢ A = B
[PROOFSTEP]
rcases A with ⟨ha⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
B : OrderBot α
toBot✝ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = B
[PROOFSTEP]
rcases B with ⟨hb⟩
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = mk hb
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toBot
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ toBot✝¹ = toBot✝
[PROOFSTEP]
ext
[GOAL]
case mk.mk.e_toBot.bot
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ ⊥ = ⊥
[PROOFSTEP]
exact le_antisymm (ha _) (hb _)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
[PROOFSTEP]
rw [eq_bot_iff, sup_le_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : BoundedOrder α
⊢ A = B
[PROOFSTEP]
have ht : @BoundedOrder.toOrderTop α _ A = @BoundedOrder.toOrderTop α _ B := OrderTop.ext
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
⊢ A = B
[PROOFSTEP]
have hb : @BoundedOrder.toOrderBot α _ A = @BoundedOrder.toOrderBot α _ B := OrderBot.ext
[GOAL]
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
B : BoundedOrder α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
γ : Type u_1
δ : Type u_2
α : Type u_3
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = mk
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤
[PROOFSTEP]
rw [map_top]
  -- Porting note: lean3 didn't need the type annotation
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤
[PROOFSTEP]
exact @le_top β _ _ _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Bot α
inst✝¹ : LE β
inst✝ : OrderBot β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_bot : f ⊥ = ⊥
a : α
⊢ f ⊥ ≤ f a
[PROOFSTEP]
rw [map_bot]
  -- Porting note: lean3 didn't need the type annotation
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝³ : LE α
inst✝² : Bot α
inst✝¹ : LE β
inst✝ : OrderBot β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_bot : f ⊥ = ⊥
a : α
⊢ ⊥ ≤ f a
[PROOFSTEP]
exact @bot_le β _ _ _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥
[PROOFSTEP]
rw [← coe_bot hbot, ext_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : OrderTop (Subtype p)
htop : p ⊤
x : { x // p x }
⊢ ↑x = ⊤ ↔ x = ⊤
[PROOFSTEP]
rw [← coe_top htop, ext_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
[PROOFSTEP]
simp only [← inf_eq_min, ← le_bot_iff, inf_le_iff]
