# Like arbitrary, but for nonempty instead of inhabited

I wrote some code that used a [inhabited ι] assumption, and then used arbitrary ι in the proof. The mathlib linter then complained

The following inhabited instances should be nonempty. argument 2: [_inst_3 : inhabited ι]


I can change the types as suggested, but what do I do with the arbitrary ι expression in my proofs?

What you're seeing here is the behavior of the inhabited_nonempty linter:

import tactic

lemma foo {α} [inhabited α] : ∃ x : α, x = x :=
begin
exact ⟨default, rfl⟩
end

#lint only inhabited_nonempty
/- Checking 1 declarations (plus 1 automatically generated ones) in the current file with 1 linters -/

/- The inhabited_nonempty linter reports: -/
/- USES OF inhabited SHOULD BE REPLACED WITH nonempty. -/


You can use the inhabit tactic to solve this problem

import tactic

lemma foo {α} [nonempty α] : ∃ x : α, x = x :=
begin
inhabit α,
exact ⟨default, rfl⟩
end

#lint only inhabited_nonempty  -- All linting checks passed!


Note this has the advantage over classical.arbitrary of not introducing the axiom of choice:

#print axioms foo  -- no axioms


while being less cumbersome than the nonempty.elim ‹nonempty α› $λ a, suggested in the other answer. The most convenient option is classical.arbitrary (or nonempty.some if your nonempty α is an explicit ssumption rather than an instance one). Note that this is exactly the axiom of choice. If your target is Prop, you can get away without using choice by writing something like nonempty.elim ‹nonempty α›$ λ a, the_rest_of_your_proof, which is arguably a bit cumbersome.