case H.a
α : Type u_1
β : Type ?u.154829
γ : Type ?u.154832
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ ↑(Equiv.finsetCongr (Equiv.refl α)) x✝ ↔ a✝ ∈ ↑(Equiv.refl (Finset α)) x✝
α : Type u_1
β : Type ?u.154829
γ : Type ?u.154832
⊢ Equiv.finsetCongr (Equiv.refl α) = Equiv.refl (Finset α)
ext
no goals
case H.a
α : Type u_1
β : Type ?u.154829
γ : Type ?u.154832
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ ↑(Equiv.finsetCongr (Equiv.refl α)) x✝ ↔ a✝ ∈ ↑(Equiv.refl (Finset α)) x✝
simp