Theorem: HFSet.eq_or_mem_of_mem_insert (Hfzfa.lean)

State before:
atoms : Type u_1
x✝ y✝ z✝ : HFSet atoms
x y z : PreHFSet atoms
h :
  Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
    insert (Quotient.mk PreHFSet.instSetoidPreHFSet y) (Quotient.mk PreHFSet.instSetoidPreHFSet z)
⊢ isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet z) = false ∧
    (Quotient.mk PreHFSet.instSetoidPreHFSet x = Quotient.mk PreHFSet.instSetoidPreHFSet y ∨
      Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet z)
Tactic:
rw [Quotient.eq]
State after:
atoms : Type u_1
x✝ y✝ z✝ : HFSet atoms
x y z : PreHFSet atoms
h :
  Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
    insert (Quotient.mk PreHFSet.instSetoidPreHFSet y) (Quotient.mk PreHFSet.instSetoidPreHFSet z)
⊢ isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet z) = false ∧
    (x ≈ y ∨ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet z)

State before:
atoms : Type u_1
x✝ y✝ z✝ : HFSet atoms
x y z : PreHFSet atoms
h :
  Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
    insert (Quotient.mk PreHFSet.instSetoidPreHFSet y) (Quotient.mk PreHFSet.instSetoidPreHFSet z)
⊢ isAtom (Quotient.mk PreHFSet.instSetoidPreHFSet z) = false ∧
    (x ≈ y ∨ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet z)
Tactic:
exact PreHFSet.eq_or_mem_of_mem_insert h
State after:
no goals