Theorem: HFSet.toFinset_eq_empty_iff (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ x = ∅
Tactic:
ext z
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom x = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom x = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Tactic:
simpa using h'
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
⊢ isAtom ∅ = false

case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅
Tactic:
simp
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h : toFinset x = ∅
h' : ¬isAtom x = true
z : HFSet atoms
⊢ z ∈ x ↔ z ∈ ∅

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
⊢ isAtom x = true ∨ x = ∅ → toFinset x = ∅
Tactic:
rintro (h'|rfl)
State after:
case inl
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h' : isAtom x = true
⊢ toFinset x = ∅

case inr
atoms : Type u_1
inst✝ : DecidableEq atoms
⊢ toFinset ∅ = ∅

State before:
case inl
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
h' : isAtom x = true
⊢ toFinset x = ∅
Tactic:
obtain ⟨a, rfl⟩ := isAtom_eq_true_iff.mp h'
State after:
case inl.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
a : atoms
h' : isAtom (atom a) = true
⊢ toFinset (atom a) = ∅

State before:
case inl.intro
atoms : Type u_1
inst✝ : DecidableEq atoms
a : atoms
h' : isAtom (atom a) = true
⊢ toFinset (atom a) = ∅
Tactic:
rfl
State after:
no goals

State before:
case inr
atoms : Type u_1
inst✝ : DecidableEq atoms
⊢ toFinset ∅ = ∅
Tactic:
rfl
State after:
no goals