case refl
α✝ : Type u
β : Type v
γ : Type ?u.18268
δ : Type ?u.18271
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
α✝ : Type u
β : Type v
γ : Type ?u.18268
δ : Type ?u.18271
α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
cases PartialOrder.ext H
case refl.h
α✝ : Type u
β : Type v
γ : Type ?u.18268
δ : Type ?u.18271
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤
case refl
α✝ : Type u
β : Type v
γ : Type ?u.18268
δ : Type ?u.18271
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
apply top_unique
no goals
case refl.h
α✝ : Type u
β : Type v
γ : Type ?u.18268
δ : Type ?u.18271
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤
exact @le_top _ _ A _