case refl
α✝ : Type u
β : Type v
γ : Type ?u.25129
δ : Type ?u.25132
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
α✝ : Type u
β : Type v
γ : Type ?u.25129
δ : Type ?u.25132
α : Type u_1
hA : PartialOrder α
A : OrderBot α
hB : PartialOrder α
B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
cases PartialOrder.ext H
case refl.h
α✝ : Type u
β : Type v
γ : Type ?u.25129
δ : Type ?u.25132
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ ≤ ⊥
case refl
α✝ : Type u
β : Type v
γ : Type ?u.25129
δ : Type ?u.25132
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥
apply bot_unique
no goals
case refl.h
α✝ : Type u
β : Type v
γ : Type ?u.25129
δ : Type ?u.25132
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ ≤ ⊥
exact @bot_le _ _ A _