inhabited should be nonempty

Stream: new members

[Joachim Breitner]

I am getting

free_group.injective_lift_of_ping_pong - The following `inhabited` instances should be `nonempty`. argument 2: [_inst_3 : inhabited ι]

from the linter. I can change that parameter, but what do I use instead of default ι in my proofs now?

[Yaël Dillies]

docs#classical.arbitrary

[Joachim Breitner]

Ah, thanks. I was already doing things like

    exact nonempty.elim (by apply_instance) (λ (i : ι),
      begin … end)

:-D.

[Joachim Breitner]

Maybe I’ll add a pointer to classical.arbitrary from https://leanprover-community.github.io/mathlib_docs/init/logic.html#nonempty? Ah, but that doesn’t work because it’d point form core into mathlib. I’ll maybe improve the linter message then.

Hmm, but that would lose some conciseness there. I’ll leave it and let others learn via Zulip as well :-)

[Joachim Breitner]

I’ll leave a question on the SE site, for future users googling for this.
@Yaël Dillies , do you want to answer https://proofassistants.stackexchange.com/questions/1168/like-arbitrary-but-for-nonempty-instead-of-inhabited for SE reputation points, or should I just do it?

[Yaël Dillies]

Oh I guess I should because I still haven't been active at all here.

[Joachim Breitner]

I wonder if there is a black market for SE rep points already, where people pay with lines of lean proof scripts…

[Eric Rodriguez]

there's also the inhabit tactic if you want to keep using default

[Eric Wieser]

docs#tactic.interactive.inhabit