Theorem: HFSet.mem_toFinset_iff (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ toFinset (Quotient.mk PreHFSet.instSetoidPreHFSet s) ↔
    Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Tactic:
rw [toFinset, Quotient.lift_mk, List.mem_toFinset (a := ⟦x⟧)]
State after:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
      List.map (fun z => Quotient.mk PreHFSet.instSetoidPreHFSet z) (PreHFSet.toList s) ↔
    Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈
      List.map (fun z => Quotient.mk PreHFSet.instSetoidPreHFSet z) (PreHFSet.toList s) ↔
    Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Tactic:
simp only [List.mem_map, Quotient.eq, ← PreHFSet.mem_toList_iff]
State after:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ x ∈ s ↔ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x✝ s✝ : HFSet atoms
s x : PreHFSet atoms
⊢ x ∈ s ↔ Quotient.mk PreHFSet.instSetoidPreHFSet x ∈ Quotient.mk PreHFSet.instSetoidPreHFSet s
Tactic:
rfl
State after:
no goals