Theorem: Partial.Nonempty.exists_mem (ReactorModel/Extensions.lean)

State before:
α : Type u_1
β : Type u_2
f : α ⇀ β
n : Nonempty f
⊢ ∃ a, a ∈ f
Tactic:
simp [iff_ids_nonempty, mem_def] at *
State after:
α : Type u_1
β : Type u_2
f : α ⇀ β
n : Set.Nonempty (ids f)
⊢ ∃ a, a ∈ ids f

State before:
α : Type u_1
β : Type u_2
f : α ⇀ β
n : Set.Nonempty (ids f)
⊢ ∃ a, a ∈ ids f
Tactic:
exact ⟨_, n.some_mem⟩
State after:
no goals