Theorem: PreHFSet.mem_toList_iff (Hfzfa.lean)

State before:
atoms : Type u_1
x y : PreHFSet atoms
a✝ : atoms
⊢ x ∈ atom a✝ ↔ ∃ x', x' ∈ toList (atom a✝) ∧ x' ≈ x
Tactic:
simp [toList, not_mem_atom]
State after:
no goals

State before:
atoms : Type u_1
x y : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
x✝ : ∃ x', x' ∈ toList (lst b) ∧ x' ≈ x
x' : PreHFSet atoms
h₁ : x' ∈ toList (lst b)
h₂ : x' ≈ x
⊢ x ∈ lst b
Tactic:
obtain ⟨i, rfl⟩ := (List.mem_ofFn _ _).mp h₁
State after:
case intro
atoms : Type u_1
x y : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
x✝ : ∃ x', x' ∈ toList (lst b) ∧ x' ≈ x
i : Fin n✝
h₁ : b i ∈ toList (lst b)
h₂ : b i ≈ x
⊢ x ∈ lst b

State before:
case intro
atoms : Type u_1
x y : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
x✝ : ∃ x', x' ∈ toList (lst b) ∧ x' ≈ x
i : Fin n✝
h₁ : b i ∈ toList (lst b)
h₂ : b i ≈ x
⊢ x ∈ lst b
Tactic:
exact ⟨i, h₂.symm⟩
State after:
no goals