Commit 2025-02-11 15:35 35037673

feat: erw?, a tool to explain why erw is necessary (#21643) Zulip Example usage: in

def subalgebraMap (e : A ≃ₐ[R] B) (S : Subalgebra R A) : S ≃ₐ[R] S.map (e : A →ₐ[R] B) :=
  { e.toRingEquiv.subsemiringMap S.toSubsemiring with
    commutes' := fun r => by
      ext; dsimp only
      erw [RingEquiv.subsemiringMap_apply_coe]
      exact e.commutes _ }

replace erw with erw?. You'll get the informational message:

(e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun
  and
⇑(e.toRingEquiv.subsemiringMap S.toSubsemiring)
  are defeq at default transparency, but not at reducible transparency.

and this then suggests to a sufficiently expert reader which simp lemmas are missing! (In this particular case, I'd first replace the dsimp only with dsimp, and then run erw?, which tell you something more useful.) Note that erw? only accepts a single lemma, so any erw [X1, X2, X3] need to be broken up first (this is probably good practice anyway, to record which steps really need the erw).