extracting to_fun

Stream: new members

[Sigma]

When using lean ive run into this issue a lot where there are certain terms that become completely opaque. For example,

import ring_theory.power_series.basic

noncomputable theory

variables {M : Type*} [ring M]

instance coer : has_coe M (power_series M) := {
  coe := λ m, power_series.mk (λ n, ite (0 = n) m 0),
}

lemma coe_hom : ring_hom M (power_series M) := {
  to_fun := λ m, ↑m,
  map_one' := sorry,
  map_mul' := sorry,
  map_zero' := sorry,
  map_add' := sorry,
}

lemma opaque : coe_hom.to_fun = (λ m : M, ↑m) := begin
  sorry,
end

I cannot interact with the coe_hom.to_fun in any way, besides when i simp it becomes ⇑coe_hom. refl fails, simp doesn't do anything useful, unfold coe_hom.to_fun fails, what's happening and how do I get around it?

[Huỳnh Trần Khanh]

disclaimer: I'm not a mathematician. lemma coe_hom should be def coe_hom though because ring_hom isn't a Prop

once you fix this things should work as usual but don't quote me on this

[Yaël Dillies]

ext works

[Yaël Dillies]

But mostly coe_hom is a lemma when it should be a def. This works

def coe_hom : ring_hom M (power_series M) := {
  to_fun := λ m, ↑m,
  map_one' := sorry,
  map_mul' := sorry,
  map_zero' := sorry,
  map_add' := sorry }

lemma opaque : coe_hom.to_fun = (λ m : M, ↑m) := by { ext, refl }

but if you replace it with lemma coe_hom ... it fails, because that makes Lean throw away the definition.