α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a, a ∈ s ∧ ↑(Equiv.toEmbedding f) a = b) ↔ ↑f.symm b ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ b ∈ map (Equiv.toEmbedding f) s ↔ ↑f.symm b ∈ s
rw [mem_map]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a, a ∈ s ∧ ↑(Equiv.toEmbedding f) a = b) ↔ ↑f.symm b ∈ s
exact
  ⟨by
    rintro ⟨a, H, rfl⟩
    simpa, fun h => ⟨_, h, by simp⟩⟩
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
a : α
H : a ∈ s
⊢ ↑f.symm (↑(Equiv.toEmbedding f) a) ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a, a ∈ s ∧ ↑(Equiv.toEmbedding f) a = b) → ↑f.symm b ∈ s
rintro ⟨a, H, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
a : α
H : a ∈ s
⊢ ↑f.symm (↑(Equiv.toEmbedding f) a) ∈ s
simpa
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3584
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
h : ↑f.symm b ∈ s
⊢ ↑(Equiv.toEmbedding f) (↑f.symm b) = b
simp