nonzero thing in `with_zero X`

Stream: Is there code for X?

[Kevin Buzzard]

Because with_zero is irreducible I would expect to see some kind of with_zero.rec or with_zero.elim which I can use to do basic stuff. But I can't find it. How do I make the following definition without locally marking with_zero as reducible? Or am I supposed to make it reducible for the purposes of the definition and then make the API?

import tactic

/-- The term of type α corresponding to a non-zero element of `with_zero α`. -/
def to_nonzero {α : Type} {P : with_zero α} (hP : P ≠ 0) : α := sorry

-- is `rfl` too much to ask for?
example (α : Type) (P : α) : to_nonzero (@with_zero.coe_ne_zero α P) = P := sorry

[Adam Topaz]

import tactic

/-- The term of type α corresponding to a non-zero element of `with_zero α`. -/
noncomputable def to_nonzero {α : Type} {P : with_zero α} (hP : P ≠ 0) : α :=
(with_zero.ne_zero_iff_exists.mp hP).some

@[simp]
lemma to_nonzero_spec {α : Type} {P : with_zero α} (hP : P ≠ 0) : ↑(to_nonzero hP) = P :=
(with_zero.ne_zero_iff_exists.mp hP).some_spec


-- is `rfl` too much to ask for?
example (α : Type) (P : α) : to_nonzero (@with_zero.coe_ne_zero α P) = P :=
begin
  apply_fun (λ e : α, (e : with_zero α )),
  simp,
  -- now I can't find the fact that coe is injective...
  sorry
end

[Adam Topaz]

Oh, that's silly... we have docs#with_zero.coe_inj but it's an iff not a function.injective statement.

[Adam Topaz]

I guess this is just like when one has an injective map $\iota : X \to Y$ and you want to produce an element of $X$ given a proof that $y : Y$ is in the image of $\iota$.

[Adam Topaz]

We probably have some API for this more general question.

[Kevin Buzzard]

import tactic

local attribute [reducible] with_zero

/-- The term of type α corresponding to a non-zero element of `with_zero α`. -/
def to_nonzero {α : Type} {P : with_zero α} (hP : P ≠ 0) : α :=
begin
  cases P,
  { exact false.elim (hP rfl)},
  { exact P}
end

example (α : Type) (P : α) : to_nonzero (@with_zero.coe_ne_zero α P) = P := rfl

is one way of doing it, but I feel a bit dirty making with_zero locally reducible (not least because I was one of the people clamouring to make it irreducible)

[Eric Wieser]

Do we have an analog to docs#with_bot.rec_bot_coe?