case H.a
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ ↑((Equiv.finsetCongr e).trans (Equiv.finsetCongr e')) x✝ ↔ a✝ ∈ ↑(Equiv.finsetCongr (e.trans e')) x✝
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ (Equiv.finsetCongr e).trans (Equiv.finsetCongr e') = Equiv.finsetCongr (e.trans e')
ext
no goals
case H.a
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ ↑((Equiv.finsetCongr e).trans (Equiv.finsetCongr e')) x✝ ↔ a✝ ∈ ↑(Equiv.finsetCongr (e.trans e')) x✝
simp [-Finset.mem_map, -Equiv.trans_toEmbedding]