chore: enable warning.simp.varHead (#13403)

This PR globally enables `warning.simp.varHead` (added in #13325) and
silences the warning in `Lake.Util.Family.Mathlib` adaptations were
already merged as part of adaptations for #13325. This is a separate PR
from #13325 due to warning appearing when re-bootstrapping, so we needed
`stage0` update before enabling this option.

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -51,7 +51,7 @@ register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
 }
 
 register_builtin_option warning.simp.varHead : Bool := {
-  defValue := false
+  defValue := true
   descr := "If true, warns when the head symbol of the left-hand side of a `@[simp]` theorem \
     is a variable. Such lemmas are tried on every simp step, which can be slow."
 }

src/lake/Lake/Util/Family.lean

@@ -154,6 +154,7 @@ public class FamilyOut {α : Type u} {β : Type v} (f : α → β) (a : α) (b :
 -- Simplifies proofs involving open type families.
 -- Scoped to avoid slowing down `simp` in downstream projects (the discrimination
 -- tree key is `_`, so it would be attempted on every goal).
+set_option warning.simp.varHead false in
 attribute [scoped simp] FamilyOut.fam_eq
 
 public instance [FamilyDef f a b] : FamilyOut f a b where

tests/elab/simpVarHead.lean

@@ -1,5 +1,3 @@
-set_option warning.simp.varHead true
-
 section
 theorem broken1 (x : Nat) : x = x + 0 := by simp