Theorem: SetTheory.union_pair_eq_inter_pair (SetTheory/Basic.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y ↔ x = y
Tactic:
constructor
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y → x = y

case mpr
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = y → {x} ∪ pair x y = {x} ∩ pair x y

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ {x} ∪ pair x y = {x} ∩ pair x y → x = y
Tactic:
intro h
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : {x} ∪ pair x y = {x} ∩ pair x y
⊢ x = y

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h : {x} ∪ pair x y = {x} ∩ pair x y
⊢ x = y
Tactic:
rw [ext_iff] at h
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ x = y

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ x = y
Tactic:
have := (h y).mp ?_
State after:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y ∈ {x} ∩ pair x y
⊢ x = y

case mp.refine_1
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ y ∈ {x} ∪ pair x y

State before:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y ∈ {x} ∩ pair x y
⊢ x = y
Tactic:
rw [mem_inter_iff, mem_singleton_iff] at this
State after:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y = x ∧ y ∈ pair x y
⊢ x = y

State before:
case mp.refine_2
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
this : y = x ∧ y ∈ pair x y
⊢ x = y
Tactic:
exact this.1.symm
State after:
no goals

State before:
case mp.refine_1
V : Type u_1
inst✝ : Zermelo V
x y z : V
h✝ : {x} ∪ pair x y = {x} ∩ pair x y
h : ∀ (z : V), z ∈ {x} ∪ pair x y ↔ z ∈ {x} ∩ pair x y
⊢ y ∈ {x} ∪ pair x y
Tactic:
simp
State after:
no goals

State before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x = y → {x} ∪ pair x y = {x} ∩ pair x y
Tactic:
rintro rfl
State after:
case mpr
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ {x} ∪ pair x x = {x} ∩ pair x x

State before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x z : V
⊢ {x} ∪ pair x x = {x} ∩ pair x x
Tactic:
simp
State after:
no goals