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

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
⊢ ¬power x ⊆ x
Tactic:
intro h
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ False

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ False
Tactic:
refine russellSet_not_mem x (h ?_)
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ∈ power x

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ∈ power x
Tactic:
rw [mem_power_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ⊆ x

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : power x ⊆ x
⊢ russellSet x ⊆ x
Tactic:
exact russellSet_subset x
State after:
no goals