α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
⊢ A = B
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
A B : BoundedOrder α
⊢ A = B
have ht : @BoundedOrder.toOrderTop α _ A = @BoundedOrder.toOrderTop α _ B := OrderTop.ext
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ A = B
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
⊢ A = B
have hb : @BoundedOrder.toOrderBot α _ A = @BoundedOrder.toOrderBot α _ B := OrderBot.ext
case mk
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
B : BoundedOrder α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = B
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
A B : BoundedOrder α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ A = B
cases A
case mk.mk
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = mk
case mk
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
B : BoundedOrder α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = B
cases B
no goals
case mk.mk
α✝ : Type u
β : Type v
γ : Type ?u.28802
δ : Type ?u.28805
α : Type u_1
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
ht : toOrderTop = toOrderTop
hb : toOrderBot = toOrderBot
⊢ mk = mk
congr