merge lean-pr-testing-11620

leanprover-community-mathlib4-bot · leanprover-community-mathlib4-bot · commit 2cb7523e3051 · 2025-12-13T08:53:53.000Z
diff --git a/Mathlib/Data/Nat/Find.lean b/Mathlib/Data/Nat/Find.lean
@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Data.Nat.Basic
 public import Mathlib.Tactic.Push
-public import Batteries.WF
 
 /-!
 # `Nat.find` and `Nat.findGreatest`
diff --git a/Mathlib/Data/PFun.lean b/Mathlib/Data/PFun.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
 -/
 module
 
-public import Batteries.WF
 public import Batteries.Tactic.GeneralizeProofs
 public import Mathlib.Data.Part
 public import Mathlib.Data.Rel
diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Logic.IsEmpty
 public import Mathlib.Order.Basic
 public import Mathlib.Tactic.MkIffOfInductiveProp
-public import Batteries.WF
 
 /-!
 # Unbundled relation classes
