no goals
α : Type u_1
β : Type ?u.27118
γ : Type ?u.27121
δ : Type ?u.27124
ι : Sort ?u.27127
κ : ι → Sort ?u.27132
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
s✝ t : Interval α
a b : α
s : Interval α
⊢ ↑(↑dual s) = ↑ofDual ⁻¹' ↑s
cases s with
| none => rfl
| some s₀ => exact NonemptyInterval.coe_dual s₀
no goals
case none
α : Type u_1
β : Type ?u.27118
γ : Type ?u.27121
δ : Type ?u.27124
ι : Sort ?u.27127
κ : ι → Sort ?u.27132
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
s t : Interval α
a b : α
⊢ ↑(↑dual none) = ↑ofDual ⁻¹' ↑none
rfl
no goals
case some
α : Type u_1
β : Type ?u.27118
γ : Type ?u.27121
δ : Type ?u.27124
ι : Sort ?u.27127
κ : ι → Sort ?u.27132
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
s t : Interval α
a b : α
s₀ : NonemptyInterval α
⊢ ↑(↑dual (some s₀)) = ↑ofDual ⁻¹' ↑(some s₀)
exact NonemptyInterval.coe_dual s₀