Theorem: Finset.mem_imageOfFinset (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ f a ha ∈ s.imageOfFinset f
Tactic:
simp[mem_imageOfFinset_iff]
State after:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha

State before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha
Tactic:
exact ⟨a, ha, rfl⟩
State after:
no goals