congr not doing anything in the presence of dependent fields

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

congr not working as expected

Steps to Reproduce

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ := by
  intro m₁ m₂
  cases m₁ with
  | @mk one₁ mul₁ one_mul₁ mul_one₁ =>
    cases one₁ with | mk one₁ => 
    cases mul₁ with | mk mul₁ => 
    cases m₂ with
    | @mk one₂ mul₂ one_mul₂ mul_one₂ =>
      cases one₂ with | mk one₂ => 
      cases mul₂ with | mk mul₂ => 
        simp
        intro h
        cases h
        congr -- Does nothing
        -- So this fails
        exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Expected behavior: [What you expect to happen]

congr to change the goal to one₁ = one₂, as it would have in Lean3.

Actual behavior:

congr succeeds, but does not change the goal.

Versions

Lean (version 4.0.0-nightly-2022-10-09, commit 5ef9a2ac7d1f, Release)

Start with the self-contained reproducer in the issue, especially the congr call in MulOneClass.ext. Run it against the stated Lean version and inspect the behavior of congr around dependent fields. Done means the tactic changes the goal to one₁ = one₂ in this example, with the reproducer succeeding.