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

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

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
⊢ False
Tactic:
by_cases h' : russellSet x ∈ russellSet x
State after:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
⊢ False

case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
⊢ False

State before:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
⊢ False
Tactic:
have := mem_russellSet_iff.mp h'
State after:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
this : russellSet x ∈ x ∧ ¬russellSet x ∈ russellSet x
⊢ False

State before:
case pos
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : russellSet x ∈ russellSet x
this : russellSet x ∈ x ∧ ¬russellSet x ∈ russellSet x
⊢ False
Tactic:
exact this.2 h'
State after:
no goals

State before:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
⊢ False
Tactic:
have := h'
State after:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' this : ¬russellSet x ∈ russellSet x
⊢ False

State before:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' this : ¬russellSet x ∈ russellSet x
⊢ False
Tactic:
rw [mem_russellSet_iff, not_and, not_not] at this
State after:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
this : russellSet x ∈ x → russellSet x ∈ russellSet x
⊢ False

State before:
case neg
V : Type u_1
inst✝ : Zermelo V
x✝ y z x : V
h : russellSet x ∈ x
h' : ¬russellSet x ∈ russellSet x
this : russellSet x ∈ x → russellSet x ∈ russellSet x
⊢ False
Tactic:
exact h' (this h)
State after:
no goals