diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index b1b84020d3..2fd9503ea2 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/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."
 }
diff --git a/src/lake/Lake/Util/Family.lean b/src/lake/Lake/Util/Family.lean
index ffbb7ab6eb..02432e413a 100644
--- a/src/lake/Lake/Util/Family.lean
+++ b/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
diff --git a/tests/elab/simpVarHead.lean b/tests/elab/simpVarHead.lean
index 61f86f7e09..f8532e3af9 100644
--- a/tests/elab/simpVarHead.lean
+++ b/tests/elab/simpVarHead.lean
@@ -1,5 +1,3 @@
-set_option warning.simp.varHead true
-
 section
 theorem broken1 (x : Nat) : x = x + 0 := by simp