case mk
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
B : OrderBot α
toBot✝ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = B
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
A B : OrderBot α
⊢ A = B
rcases A with ⟨ha⟩
case mk.mk
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = mk hb
case mk
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
B : OrderBot α
toBot✝ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = B
rcases B with ⟨hb⟩
case mk.mk.e_toBot
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ toBot✝¹ = toBot✝
case mk.mk
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ mk ha = mk hb
congr
case mk.mk.e_toBot.bot
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ ⊥ = ⊥
case mk.mk.e_toBot
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ toBot✝¹ = toBot✝
ext
no goals
case mk.mk.e_toBot.bot
α✝ : Type u
β : Type v
γ : Type ?u.25434
δ : Type ?u.25437
α : Type u_1
inst✝ : PartialOrder α
toBot✝¹ : Bot α
ha : ∀ (a : α), ⊥ ≤ a
toBot✝ : Bot α
hb : ∀ (a : α), ⊥ ≤ a
⊢ ⊥ = ⊥
exact le_antisymm (ha _) (hb _)