erw and defeq abuse: documentation?

Stream: mathlib4

[Moritz Firsching]

Is there some wiki/documentation explaining the defeq abuse and how to avoid it and alsoerw-avoidance?
I understand erw is discouraged and same for defeq abuse. I sometimes don't understand when a defeq-abuse is considered bad and when it is considered not so bad, perhaps this is best explained with examples (see below)

Is there a or could there be a defeq-abuse linter, that flags problematic places?

As an random example of a proof using two erw that can avoided by using rfl and exact:
https://github.com/leanprover-community/mathlib4/blob/abcae08fdcad503ad41f1f30c52c5440b147955e/Mathlib/RingTheory/Smooth/StandardSmooth.lean#L336

open scoped Classical in
private lemma jacobiMatrix_comp_₂₂_det :
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = algebraMap S T P.jacobian := by
  rw [jacobian_eq_jacobiMatrix_det]
  rw [AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det, RingHom.map_det]
  congr
  ext i j : 1
  simp only [Matrix.toBlocks₂₂, AlgHom.mapMatrix_apply, Matrix.map_apply, Matrix.of_apply,
    RingHom.mapMatrix_apply, Generators.algebraMap_apply, map_aeval, coe_eval₂Hom]
  rw [jacobiMatrix_comp_inr_inr, ← IsScalarTower.algebraMap_eq]
  simp only [aeval, AlgHom.coe_mk, coe_eval₂Hom]
  generalize P.jacobiMatrix i j = p
  induction' p using MvPolynomial.induction_on with a p q hp hq p i hp
  · simp only [algHom_C, algebraMap_eq, eval₂_C]
    -- was: erw [MvPolynomial.eval₂_C]
    exact eval₂_C (algebraMap R T) (Q.comp P).val a
  · simp [hp, hq]
  · simp only [map_mul, rename_X, eval₂_mul, hp, eval₂_X]
    -- was:
    -- erw [Generators.comp_val]
    -- simp
    rfl

The last rfl could also be

  suffices algebraMap S T (P.val i)= (Q.comp P).val (Sum.inr i) by
    rw [this]
  rfl

Are those rfls discouraged?

[Christian Merten]

Side note: this specific source of erws is mostly caused by (Q.comp P).vars not unifying with Q.vars ⊕ P.vars at reducible transparency, which is the transparency level at which most tactics operate, for an attempt to fix this see: #PR reviews > #21099 use unification hints for generators

[Christian Merten]

Back to your question: In my opinion replacing an erw with some reordering terms and a final exact, apply or rfl only hides the issue from the tech-debt statistics, but is not an improvement. A clear improvement is whenever a tactic that operates at default tansparency (such as erw, exact, rfl) is replaced by a tactic that operates at reducible transparency (e.g. simp, rw).

[Moritz Firsching]

is there some way to inspect if a concrete call to rfl, exact or apply is using non-reducible transparency?

[Christian Merten]

You can prepend your tactic with with_reducible, e.g. with_reducible rfl

[Moritz Firsching]

so the last rfl in the example above can be replaced with

    solve_by_elim (config := {transparency := .reducible})

Why does this work, while with_reducible rfl fails?

[Christian Merten]

I can't answer this question, but the proof of this specific lemma can be replaced by:

open scoped Classical in
private lemma jacobiMatrix_comp_₂₂_det :
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = algebraMap S T P.jacobian := by
  rw [jacobian_eq_jacobiMatrix_det]
  rw [AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det, RingHom.map_det]
  congr
  ext i j : 1
  simp only [Matrix.toBlocks₂₂, AlgHom.mapMatrix_apply, Matrix.map_apply, Matrix.of_apply,
    RingHom.mapMatrix_apply, Generators.algebraMap_apply, map_aeval, coe_eval₂Hom]
  rw [jacobiMatrix_comp_inr_inr, ← IsScalarTower.algebraMap_eq]
  generalize P.jacobiMatrix i j = p
  induction' p using MvPolynomial.induction_on with a p q hp hq p i hp
  · simp
  · simp only [map_add, hp, hq, eval₂_add]
  · simp only [comp_val, Presentation.comp_val, Generators.comp_val, map_mul, rename_X,
      aeval_rename, aeval_X, Sum.elim_inr, Function.comp_apply, eval₂_mul, eval₂_X]
    simp [aeval, Function.comp_def]

when adding the same unification hints as in the PR linked above for PreSubmersivePresentation.comp and adding some {Presentation, PreSubmersivePresentation}.comp_val lemmas.

[Christian Merten]

I pushed it to the PR, for the precise changes see the commit.