The two examples below fail, but work if you replace Nat → Nat by Nat.

opaque partiallyApplied (p : Prop) [Decidable p] : Nat → Nat

example : partiallyApplied (True ∧ True) = partiallyApplied True := by
  simp

example : partiallyApplied (True ∧ True) = partiallyApplied True := by
  congr
  decide

As reported on Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mkCongrSimp.3F.20error.20for.20Set/near/338881269

This is causing issues in mathlib because Set α is defined as α → Prop, so a lot of terms are actually partially-applied functions, like for example Set.image f s.