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

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

State before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) ↔ ∃ a, ∃ (ha : a ∈ s), f a ha = b
Tactic:
constructor
State after:
case mp
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) → ∃ a, ∃ (ha : a ∈ s), f a ha = b

case mpr
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a, ∃ (ha : a ∈ s), f a ha = b) → ∃ a ∈ s, ∃ (i : a ∈ s), f a i = b

State before:
case mp
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) → ∃ a, ∃ (ha : a ∈ s), f a ha = b
Tactic:
rintro ⟨a, _, ha, rfl⟩
State after:
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
left✝ ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha

State before:
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
left✝ 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

State before:
case mpr
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a, ∃ (ha : a ∈ s), f a ha = b) → ∃ a ∈ s, ∃ (i : a ∈ s), f a i = b
Tactic:
rintro ⟨a, ha, rfl⟩
State after:
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1 ∈ s, ∃ (i : a_1 ∈ s), f a_1 i = f a ha

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