invalid 'simp' G ≃ₜ G in !4#2420

Stream: mathlib4

[Arien Malec]

In !4#2420, (Topology.Algebra.Group.Compact), G ≃ₜ G fails as a simp proposition expected, but works on the Lean3 side... Is there a trivial way to transform the hypothesis, or some missing machinery in the port here?

[Arien Malec]

The answer was Homeomorph.coe_toEquiv

[Adam Topaz]

You can just do by simp [Homeomorph.mulLeft_symm] (without the F) in this case, since F was introduced locally with a let.

[Arien Malec]

Ah, that works as well. Though I tried that :-)

[Arien Malec]

It's weird, because simp [Homeomorph.mulLeft_symm] works, but simp only [Homeomorph.mulLeft_symm] doesn't, and any use of simp? suggests simp only [Homeomorph.mulLeft_symm] & simp only [Homeomorph.coe_toEquiv F Homeomorph.mulLeft_symm]] doesn't work either...

[Adam Topaz]

simp? gave me

by
    simp only [Homeomorph.mulLeft_symm, mul_inv_rev,
      inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]

which works

[Arien Malec]

not on my side? So weird?

[Adam Topaz]

That is strange.

[Adam Topaz]

I'm using simp? [Homeomorph.mulLeft_symm], is that what you're using as well?

[Arien Malec]

Oh, I was using simp? only [Homeomorph.mulLeft_symm]

[Adam Topaz]

ah that's the issue :)

[Adam Topaz]

that tells lean to look for the lemmas used but also to only use Homeomorph.mulLeft_symm :rofl:

[Adam Topaz]

I'm surprised that syntax is even allowed with simp?

[Arien Malec]

it's slightly counterintuitive, yes.

[Yaël Dillies]

It is useful syntax, yes. I sometimes wanted to reduce 3 lines simp calls without opening the the door the new simp lemmas being added, because I was purposefully introducing non-confluency locally.

[Arien Malec]

Arien Malec said:

The answer was Homeomorph.coe_toEquiv

Actually, I don't think that's true; I just handed simp an equality, and the fact that it closed was a coincidence. So again, did Lean3 simp accept an Equiv and Lean4 simp doesn't?