case mk
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
B : OrderTop α
toTop✝ : Top α
ha : ∀ (a : α), a ≤ ⊤
⊢ mk ha = B
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
A B : OrderTop α
⊢ A = B
rcases A with ⟨ha⟩
case mk.mk
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ mk ha = mk hb
case mk
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
B : OrderTop α
toTop✝ : Top α
ha : ∀ (a : α), a ≤ ⊤
⊢ mk ha = B
rcases B with ⟨hb⟩
case mk.mk.e_toTop
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ toTop✝¹ = toTop✝
case mk.mk
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ mk ha = mk hb
congr
case mk.mk.e_toTop.top
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ ⊤ = ⊤
case mk.mk.e_toTop
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ toTop✝¹ = toTop✝
ext
no goals
case mk.mk.e_toTop.top
α✝ : Type u
β : Type v
γ : Type ?u.18573
δ : Type ?u.18576
α : Type u_1
inst✝ : PartialOrder α
toTop✝¹ : Top α
ha : ∀ (a : α), a ≤ ⊤
toTop✝ : Top α
hb : ∀ (a : α), a ≤ ⊤
⊢ ⊤ = ⊤
exact le_antisymm (hb _) (ha _)