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

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

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