rw tactic failed

Stream: general

[Kenny Lau]

rewrite tactic failed, did not find instance of the pattern in the target expression
  @has_add.add.{?l_1} ?m_2
    (@add_semigroup.to_has_add.{?l_1} ?m_2
       (@add_monoid.to_add_semigroup.{?l_1} ?m_2 (@add_group.to_add_monoid.{?l_1} ?m_2 ?m_3)))
    (@has_smul.smul.{0 ?l_1} int ?m_2 (@add_group.has_smul.{?l_1} ?m_2 ?m_3) ?m_4 ?m_5)
    (@has_smul.smul.{0 ?l_1} int ?m_2 (@add_group.has_smul.{?l_1} ?m_2 ?m_3) ?m_6 ?m_5)


⊢ [..]
          (@has_add.add.{u₁} α₁
             (@add_semigroup.to_has_add.{u₁} α₁
                (@add_monoid.to_add_semigroup.{u₁} α₁
                   (@add_comm_monoid.to_add_monoid.{u₁} α₁
                      (@add_comm_group.to_add_comm_monoid.{u₁} α₁
                         (@module.to_add_comm_group.{u u₁} α α₁ (@comm_ring.to_ring.{u} α _inst_1) _inst_4)))))
             (@has_smul.smul.{0 u₁} int α₁
                (@add_group.has_smul.{u₁} α₁
                   (@add_comm_group.to_add_group.{u₁} α₁
                      (@module.to_add_comm_group.{u u₁} α α₁ (@comm_ring.to_ring.{u} α _inst_1) _inst_4)))
                n
                (f (@prod.fst.{v w} β γ (@prod.mk.{v w} β γ x y₁))
                   (@prod.snd.{v w} β γ (@prod.mk.{v w} β γ x y₁))))
             (@has_smul.smul.{0 u₁} int α₁
                (@add_group.has_smul.{u₁} α₁
                   (@add_comm_group.to_add_group.{u₁} α₁
                      (@module.to_add_comm_group.{u u₁} α α₁ (@comm_ring.to_ring.{u} α _inst_1) _inst_4)))
                n
                (f (@prod.fst.{v w} β γ (@prod.mk.{v w} β γ x y₂))
                   (@prod.snd.{v w} β γ (@prod.mk.{v w} β γ x y₂)))))

[Kenny Lau]

Lean, it's right there

[Kenny Lau]

I know you want (@add_group.to_add_monoid.{?l_1} ?m_2 ?m_3)

[Kenny Lau]

but isn't (@add_comm_monoid.to_add_monoid.{u₁} α₁ (@add_comm_group.to_add_comm_monoid.{u₁} α₁ (@module.to_add_comm_group.{u u₁} α α₁ (@comm_ring.to_ring.{u} α _inst_1) _inst_4)) good enough for you

[Kevin Buzzard]

they don't look the same to me

[Kenny Lau]

they're both justifying why I have addition

[Kenny Lau]

specifically here they're justifying why I have an add_monoid

[Kevin Buzzard]

can you do some BS "change" or "show" beforehand?

[Kevin Buzzard]

Is this one of these dreaded diamond things?

[Kenny Lau]

yes

[Kenny Lau]

I think the main concern is the one in the gsmul thread

[Kenny Lau]

overloading is not good

[Kevin Buzzard]

This is Mario's doing, right?

[Kevin Buzzard]

So probably he will have some sensible solution

[Kenny Lau]

well but that bullet wasn't in the global namespace before Lean updated

[Kevin Buzzard]

oh so it's Leo's doing?

[Kenny Lau]

I would say so

[Kevin Buzzard]

So probably Mario will have some clever workaround.

[Kevin Buzzard]

I blame myself for all this

[Kenny Lau]

you?

[Kevin Buzzard]

I should never have mentioned that ^ had the wrong associativity

[Kenny Lau]

what happened

[Kevin Buzzard]

I got annoyed that 2^3^2 was 64 not 512

[Kevin Buzzard]

so I opened an issue

[Kevin Buzzard]

and all of a sudden there were lots of changes to ^

[Kenny Lau]

I see

[Kevin Buzzard]

https://github.com/leanprover/lean/issues/1951

[Kevin Buzzard]

led to https://github.com/leanprover/lean/commit/d387103aa2bebfc98220733d9607a16663ec1ef2

[Kevin Buzzard]

and then to https://github.com/leanprover/lean/commit/8f55ec4c50379c612731ced2424fd3eda0cf69a6

[Kevin Buzzard]

and hmm I don't see the bullet

[Kevin Buzzard]

maybe it's not my fault after all

[Kevin Buzzard]

nice to see presheaves being pulled into core lean though

[Kevin Buzzard]

https://github.com/leanprover/lean/commit/6e0bf8473b1980e6692a61a924b4c6eae195619d

[Kenny Lau]

oh

[Kenny Lau]

what a subversion

[Kevin Buzzard]

Talking of presheaves, thanks for trying to fix that tensor product file. Presumably that's where this issue arose.

[Mario Carneiro]

I removed the has_smul typeclass from group_power, which should fix the notation overloading problem. This puts us back at square one local infix type solutions for using gsmul, but it shouldn't interfere with the module smul notation now. I'm not sure about registering every abelian group as a Z-module with an instance, since module still uses an out_param for the scalar ring which might get stuck on int