Regression in simp because of missing congr

Stream: mathlib4

[Bhavik Mehta]

This simp succeeds in Lean 3, but in Lean 4 the [congr] attribute doesn't apply to docs#forall_prop_congr', so the equivalent in Lean 4 doesn't work

@[congr] lemma forall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
propext ⟨λ h1 h2, (hq _).1 (h1 (hp.2 _)), λ h1 h2, (hq _).2 (h1 (hp.1 h2))⟩

example {α : Type} (x y : α) (P : ∀ {x y : α}, x ≠ y → Prop) :
  (∀ (h : x ≠ x), P h) :=
begin
  simp only [ne.def],
end

Lean 4:

-- Porting note: `@[congr]` commented out for now.
-- @[congr]
theorem forall_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
  propext  ⟨fun h1 h2 ↦ (hq _).1 (h1 (hp.2 h2)), fun h1 h2 ↦ (hq _).2 (h1 (hp.1 h2))⟩

example {α : Type} (x : α) (P : ∀ {x y : α}, x ≠ y → Prop) : (∀ (h : x ≠ x), P h) := by
  simp only [ne_eq]

What's missing in Lean 4 which is stopping us adding the congr attribute?

(With extra imports, Lean 3 simp can close this goal, but Lean 4 simp gets stuck at this first rewrite. This showed up for me when trying to port :( )

[Mauricio Collares]

This seems very related to the comment in https://github.com/leanprover/lean4/commit/a7323c98053ea992210f11b03e8fbeddcde57cb2, if not to the fix itself. Maybe this is fixed in the latest nightly? If you want to try, you can use the nightly-testing mathlib4 branch.

[Bhavik Mehta]

Oh that is very related, thank you!

[Mauricio Collares]

Unfortunately this will only show up in tomorrow's nightly

[Bhavik Mehta]

I'll wait until tomorrow - I don't trust myself to build it without screwing something up :)

[Eric Wieser]

Yes, this should have been fixed by lean4#2732 (you still can't use @[congr], but now you don't need to)

[Bhavik Mehta]

Great, I'll try again once that version of lean is released

[Mauricio Collares]

Nightly's out