case h
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} ↔ x✝ ∈ {x.unop}
α : Type u_1
x : αᵒᵖ
⊢ Set.unop {x} = {x.unop}
ext
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} → x✝ ∈ {x.unop}

case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
case h
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} ↔ x✝ ∈ {x.unop}
constructor
case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} → x✝ ∈ {x.unop}

case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
. apply op_injective
no goals
case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
. apply unop_injective
no goals
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} → x✝ ∈ {x.unop}
apply op_injective
no goals
case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
apply unop_injective