Zulip Chat Archive

Stream: mathlib4

Topic: Issue porting Algebra.Hom.Centroid.coe_to_add_monoid_hom...


Maxwell Thum (Jan 05 2023 at 08:07):

I'm stuck trying to port docs#centroid_hom.coe_to_add_monoid_hom_injective to mathlib4. Here is the original from mathlib:

lemma coe_to_add_monoid_hom_injective : injective (coe : centroid_hom α  α →+ α) :=
λ f g h, ext $ λ a, by { have := fun_like.congr_fun h a, exact this }

Here is the current port in mathlib4:

theorem coe_to_add_monoid_hom_injective : Injective (coe : CentroidHom α  α →+ α) := fun f g h =>
  ext fun a =>
    haveI := FunLike.congr_fun h a
    this

With set_option autoImplicit false, I get the error unknown identifier 'coe'.
When I comment it out , I get

type mismatch
  FunLike.congr_fun h a
has type
  (coe f) a = (coe g) a : Prop
but is expected to have type
  f a = g a : Prop

I'm more confused about the former. Not sure what to do here.

Kevin Buzzard (Jan 05 2023 at 08:51):

If you comment out set_option autoImplicit false then you're just saying "let coe be a random function CentroidHom α → α →+ α" which is clearly not what you want.

Kevin Buzzard (Jan 05 2023 at 08:54):

Try replacing coe with fun x => \u x perhaps?

Yaël Dillies (Jan 05 2023 at 08:55):

(\u) should do

Maxwell Thum (Jan 05 2023 at 19:06):

Yaël Dillies said:

(\u) should do

Oh, I see. This worked. Thanks!

Maxwell Thum (Jan 05 2023 at 23:02):

Does ↑f a equal (↑f) a or ↑(f a)?

Maxwell Thum (Jan 05 2023 at 23:05):

I ask because I'm getting this error message (and have been getting similar ones):

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑↑?f
fg: CentroidHom α
ab: α
 ↑↑(f + g) (a * b) = a * ↑↑(f + g) b

Yaël Dillies (Jan 05 2023 at 23:14):

It equals the first. The code snippet you just gave is very hard to debug because there are probably three different functions called coe in it!

Maxwell Thum (Jan 05 2023 at 23:20):

Hence my confusion :/

Maxwell Thum (Jan 05 2023 at 23:23):

Is there a way to get Lean to stop using \u and \u= so that I can figure out what's wrong?

Henrik Böving (Jan 05 2023 at 23:24):

set_option pp.notation false + set_option pp.notation.explicit true maybe?

Maxwell Thum (Jan 05 2023 at 23:30):

It looks like set_option pp.coercions false is what I was looking for. Thanks for pointing me in the right direction.

Yaël Dillies (Jan 06 2023 at 00:08):

Do you know you can click on any term on the infoview to inspect its type and definition? This would also have given you the information you want


Last updated: Dec 20 2023 at 11:08 UTC