Lake `FamilyOut.fam_eq` leads to timeouts?

Stream: lean4

[Christian Merten]

Not a mathlib free MWE, but I don't think it is needed here. Lake.FamilyOut.fam_eq is a simp lemma with a very permissive discrimination tree key (@Eq _ _ _). The file Lake.Util.Family is currently not imported in mathlib, but I recently transitively imported it in some meta program, which lead to some very confusing timeouts.

A random example (from our favorite JacobiZariski.lean):

import Mathlib
import Lake.Util.Family

/-- info: @Eq _ _ _ -/
#guard_msgs in
#discr_tree_key Lake.FamilyOut.fam_eq

-- adding this line fixes the timeout
-- attribute [-simp] Lake.FamilyOut.fam_eq

open Algebra KaehlerDifferential Module MvPolynomial TensorProduct

universe w₁ w₂ w₃ w₄ w₅ u₁ u₂ u₃

variable {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S]
  {T : Type u₃} [CommRing T] [Algebra R T]
  [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂}
  (Q : Generators S T ι) (P : Generators R S σ)

lemma map_comp_cotangentComplex_baseChange :
    (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T ∘ₗ
      P.toExtension.cotangentComplex.baseChange T =
    (Q.comp P).toExtension.cotangentComplex ∘ₗ
      (Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T := by
  ext x; simp [Extension.CotangentSpace.map_cotangentComplex]

[Christian Merten]

Could the simp attribute on Lake.FamilyOut.fam_eq be scoped to the Lake namespace?

[Kim Morrison]

Good catch! I've made it [scoped simp] in lean#12178