[GOAL]
α : Type u_1
s : Set α
a : α
⊢ op a ∈ Set.op s ↔ a ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ a.unop ∈ Set.unop s ↔ a ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
x : α
⊢ Set.op {x} = {op x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x} ↔ x✝ ∈ {op x}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x} → x✝ ∈ {op x}
[PROOFSTEP]
apply unop_injective
[GOAL]
case h.mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ Set.op {x}
[PROOFSTEP]
apply op_injective
[GOAL]
α : Type u_1
x : αᵒᵖ
⊢ Set.unop {x} = {x.unop}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} ↔ x✝ ∈ {x.unop}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} → x✝ ∈ {x.unop}
[PROOFSTEP]
apply op_injective
[GOAL]
case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
[PROOFSTEP]
apply unop_injective
[GOAL]
α : Type u_1
x : α
⊢ Set.unop {op x} = {x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x x✝ : α
⊢ x✝ ∈ Set.unop {op x} ↔ x✝ ∈ {x}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ Set.unop {op x} → x✝ ∈ {x}
[PROOFSTEP]
apply op_injective
[GOAL]
case h.mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ Set.unop {op x}
[PROOFSTEP]
apply unop_injective
[GOAL]
α : Type u_1
x : αᵒᵖ
⊢ Set.op {x.unop} = {x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x.unop} ↔ x✝ ∈ {x}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x.unop} → x✝ ∈ {x}
[PROOFSTEP]
apply unop_injective
[GOAL]
case h.mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ Set.op {x.unop}
[PROOFSTEP]
apply op_injective
