neg_mem_iff

Stream: mathlib4

[Yury G. Kudryashov]

I'm trying to forward-port #18536, namely generalization of docs#inv_mem_iff. I tried both

@[to_additive (attr := simp)]
theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
    {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
#align inv_mem_iff inv_mem_iff
#align neg_mem_iff neg_mem_iff

and

@[to_additive (attr := simp)]
theorem inv_mem_iff {S G} [InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S}
    {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
#align inv_mem_iff inv_mem_iff
#align neg_mem_iff neg_mem_iff

In both cases, Lean fails to do rw [← inv_mem_iff] in div_mem_comm_iff below.

[Yury G. Kudryashov]

Is there an easy fix? Or should I revert this part of #18536 for now?

[Yury G. Kudryashov]

For now, I'm adding explicit (x := _) here and there.

[Kevin Buzzard]

Are you trying to do the job of the autoporter?

[Yury G. Kudryashov]

I think that I can copy+paste+fix small snippets not worse than mathport. The issue is that Lean 4 rw can't use this lemma unless it knows x.

[Kevin Buzzard]

Oh I see, the issue is the binders

[Yury G. Kudryashov]

The issue is about TC search. It can find SubgroupClass that is right there in the assumptions but it fails to find NegMemClass.

[Eric Wieser]

Does temporarily enabling etaExperiment help?