lift to units?

Stream: new members

[Jalex Stark]

1. Is the following a hole in the library or did I fail to import the correct file or is it intentionally omitted? (or is it a "hole" only in the sense that most people use something other than the lift tactic for passing to a subtype?)

import tactic
universes u
open_locale classical
noncomputable theory

example (R : Type) [comm_ring R] : can_lift R (units R) := begin
refine {coe := _,
    cond :=  λ a:R, ∃ b : R, a * b = (1:R),
    prf := _},
{exact coe},
{exact λ a:R, ∃ b : R, a * b = (1:R)},
intros a ha,
cases ha with b hb,
existsi units.mk_of_mul_eq_one a b hb,
simp only [units.coe_mk_of_mul_eq_one],
end

[Jalex Stark]

2. I kind of expected apply_instance to work on the goal that is closed by the first focusing brace by finding a has_coe instance. It doesn't, but then in order for exact coe to work, Lean must be doing that same search for an instance of has_coe, right? Does this go through something more primitive than apply_instance?