Theorem: HFSet.mem_insert_iff (Hfzfa.lean)

State before:
atoms : Type u_1
x y z : HFSet atoms
⊢ x ∈ insert y z ↔ isAtom z = false ∧ (x = y ∨ x ∈ z)
Tactic:
constructor
State after:
case mp
atoms : Type u_1
x y z : HFSet atoms
⊢ x ∈ insert y z → isAtom z = false ∧ (x = y ∨ x ∈ z)

case mpr
atoms : Type u_1
x y z : HFSet atoms
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z) → x ∈ insert y z

State before:
case mp
atoms : Type u_1
x y z : HFSet atoms
⊢ x ∈ insert y z → isAtom z = false ∧ (x = y ∨ x ∈ z)
Tactic:
intro h
State after:
case mp
atoms : Type u_1
x y z : HFSet atoms
h : x ∈ insert y z
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z)

State before:
case mp
atoms : Type u_1
x y z : HFSet atoms
h : x ∈ insert y z
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z)
Tactic:
exact eq_or_mem_of_mem_insert h
State after:
no goals

State before:
case mpr
atoms : Type u_1
x y z : HFSet atoms
⊢ isAtom z = false ∧ (x = y ∨ x ∈ z) → x ∈ insert y z
Tactic:
rintro ⟨h₁, rfl|h₂⟩
State after:
case mpr.intro.inl
atoms : Type u_1
x z : HFSet atoms
h₁ : isAtom z = false
⊢ x ∈ insert x z

case mpr.intro.inr
atoms : Type u_1
x y z : HFSet atoms
h₁ : isAtom z = false
h₂ : x ∈ z
⊢ x ∈ insert y z

State before:
case mpr.intro.inl
atoms : Type u_1
x z : HFSet atoms
h₁ : isAtom z = false
⊢ x ∈ insert x z
Tactic:
exact mem_insert_self _ _ h₁
State after:
no goals

State before:
case mpr.intro.inr
atoms : Type u_1
x y z : HFSet atoms
h₁ : isAtom z = false
h₂ : x ∈ z
⊢ x ∈ insert y z
Tactic:
exact mem_insert_of_mem h₂
State after:
no goals