Stream: new members

Topic: lift to units?

Jalex Stark (May 10 2020 at 00:13):

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 (May 10 2020 at 00:16):

1. 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?

Last updated: May 14 2021 at 03:27 UTC