chore: work around simp issues in future nightlies (#11546)

Author: Ruben-VandeVelde

Mathlib/CategoryTheory/CofilteredSystem.lean

@@ -185,11 +185,15 @@ def toPreimages : J ⥤ Type v where
     rw [← mem_preimage, preimage_preimage, mem_preimage]
     convert h (g ≫ f); rw [F.map_comp]; rfl
   map_id j := by
-    simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_id]
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_id]
+    simp only [MapsTo.restrict, Subtype.map_def, F.map_id]
     ext
     rfl
   map_comp f g := by
-    simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_comp]
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_comp]
+    simp only [MapsTo.restrict, Subtype.map_def, F.map_comp]
     rfl
 #align category_theory.functor.to_preimages CategoryTheory.Functor.toPreimages
 
@@ -272,11 +276,15 @@ def toEventualRanges : J ⥤ Type v where
   obj j := F.eventualRange j
   map f := (F.eventualRange_mapsTo f).restrict _ _ _
   map_id i := by
-    simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_id]
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_id]
+    simp only [MapsTo.restrict, Subtype.map_def, F.map_id]
     ext
     rfl
   map_comp _ _ := by
-    simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_comp]
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp (config := { unfoldPartialApp := true }) only [MapsTo.restrict, Subtype.map, F.map_comp]
+    simp only [MapsTo.restrict, Subtype.map_def, F.map_comp]
     rfl
 #align category_theory.functor.to_eventual_ranges CategoryTheory.Functor.toEventualRanges
 

Mathlib/Control/Fold.lean

@@ -123,7 +123,12 @@ def Foldl.ofFreeMonoid (f : β → α → β) : FreeMonoid α →* Monoid.Foldl
   toFun xs := op <| flip (List.foldl f) (FreeMonoid.toList xs)
   map_one' := rfl
   map_mul' := by
-    intros; simp only [FreeMonoid.toList_mul, flip, unop_op, List.foldl_append, op_inj]; rfl
+    intros
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp only [FreeMonoid.toList_mul, flip, unop_op, List.foldl_append, op_inj]
+    simp only [FreeMonoid.toList_mul, unop_op, List.foldl_append, op_inj, Function.flip_def,
+      List.foldl_append]
+    rfl
 #align monoid.foldl.of_free_monoid Monoid.Foldl.ofFreeMonoid
 
 @[reducible]
@@ -316,16 +321,22 @@ theorem foldr.ofFreeMonoid_comp_of (f : β → α → α) :
 theorem foldlm.ofFreeMonoid_comp_of {m} [Monad m] [LawfulMonad m] (f : α → β → m α) :
     foldlM.ofFreeMonoid f ∘ FreeMonoid.of = foldlM.mk ∘ flip f := by
   ext1 x
-  simp only [foldlM.ofFreeMonoid, flip, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply,
-    FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure, foldlM.mk, op_inj]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp only [foldlM.ofFreeMonoid, flip, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply,
+  --   FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure, foldlM.mk, op_inj]
+  simp only [foldlM.ofFreeMonoid, Function.flip_def, MonoidHom.coe_mk, OneHom.coe_mk,
+    Function.comp_apply, FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure,
+    foldlM.mk, op_inj]
   rfl
 #align traversable.mfoldl.of_free_monoid_comp_of Traversable.foldlm.ofFreeMonoid_comp_of
 
 @[simp]
 theorem foldrm.ofFreeMonoid_comp_of {m} [Monad m] [LawfulMonad m] (f : β → α → m α) :
     foldrM.ofFreeMonoid f ∘ FreeMonoid.of = foldrM.mk ∘ f := by
   ext
-  simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, flip]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, flip]
+  simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, Function.flip_def]
 #align traversable.mfoldr.of_free_monoid_comp_of Traversable.foldrm.ofFreeMonoid_comp_of
 
 theorem toList_spec (xs : t α) : toList xs = FreeMonoid.toList (foldMap FreeMonoid.of xs) :=
@@ -336,12 +347,14 @@ theorem toList_spec (xs : t α) : toList xs = FreeMonoid.toList (foldMap FreeMon
           by simp only [List.reverse_reverse]
       _ = FreeMonoid.toList (List.foldr cons [] (foldMap FreeMonoid.of xs).reverse).reverse :=
           by simp only [List.foldr_eta]
-      _ = (unop (Foldl.ofFreeMonoid (flip cons) (foldMap FreeMonoid.of xs)) []).reverse :=
-          by simp [flip, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
-      _ = toList xs :=
-          by rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
-             simp only [toList, foldl, List.reverse_inj, Foldl.get, foldl.ofFreeMonoid_comp_of,
-               Function.comp_apply]
+      _ = (unop (Foldl.ofFreeMonoid (flip cons) (foldMap FreeMonoid.of xs)) []).reverse := by
+            -- Adaptation note: nightly-2024-03-16: simp was
+            -- simp [flip, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
+            simp [Function.flip_def, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
+      _ = toList xs := by
+            rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
+            simp only [toList, foldl, List.reverse_inj, Foldl.get, foldl.ofFreeMonoid_comp_of,
+              Function.comp_apply]
 #align traversable.to_list_spec Traversable.toList_spec
 
 theorem foldMap_map [Monoid γ] (f : α → β) (g : β → γ) (xs : t α) :
@@ -370,7 +383,9 @@ theorem toList_map (f : α → β) (xs : t α) : toList (f <$> xs) = f <$> toLis
 @[simp]
 theorem foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : t β) :
     foldl f a (g <$> l) = foldl (fun x y => f x (g y)) a l := by
-  simp only [foldl, foldMap_map, (· ∘ ·), flip]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp only [foldl, foldMap_map, (· ∘ ·), flip]
+  simp only [foldl, foldMap_map, (· ∘ ·), Function.flip_def]
 #align traversable.foldl_map Traversable.foldl_map
 
 @[simp]
@@ -418,7 +433,9 @@ theorem foldrm_toList (f : α → β → m β) (x : β) (xs : t α) :
 @[simp]
 theorem foldlm_map (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) :
     foldlm f a (g <$> l) = foldlm (fun x y => f x (g y)) a l := by
-  simp only [foldlm, foldMap_map, (· ∘ ·), flip]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp only [foldlm, foldMap_map, (· ∘ ·), flip]
+  simp only [foldlm, foldMap_map, (· ∘ ·), Function.flip_def]
 #align traversable.mfoldl_map Traversable.foldlm_map
 
 @[simp]

Mathlib/Data/DFinsupp/WellFounded.lean

@@ -224,7 +224,9 @@ protected theorem DFinsupp.wellFoundedLT [∀ i, Zero (α i)] [∀ i, Preorder (
       refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
       · rintro i ⟨a⟩
         apply hbot
-      · simp (config := { unfoldPartialApp := true }) only [Function.swap]
+      · -- Adaptation note: nightly-2024-03-16: simp was
+        -- simp (config := { unfoldPartialApp := true }) only [Function.swap]
+        simp only [Function.swap_def]
         exact IsWellFounded.wf
     refine Subrelation.wf (fun h => ?_) <| InvImage.wf (mapRange (fun i ↦ e i) fun _ ↦ rfl) this
     have := IsStrictOrder.swap (@WellOrderingRel ι)

Mathlib/Data/Nat/Bitwise.lean

@@ -81,7 +81,9 @@ theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n →
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
     bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by
   conv_lhs => unfold bitwise
-  simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, Bool.cond_eq_ite]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, Bool.cond_eq_ite]
+  simp only [bit, ite_apply, bit1, bit0, Bool.cond_eq_ite]
   have h1 x :     (x + x) % 2 = 0 := by rw [← two_mul, mul_comm]; apply mul_mod_left
   have h2 x : (x + x + 1) % 2 = 1 := by rw [← two_mul, add_comm]; apply add_mul_mod_self_left
   have h3 x :     (x + x) / 2 = x := by rw [← two_mul, mul_comm]; apply mul_div_left _ zero_lt_two
@@ -92,7 +94,10 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by
 
 lemma bit_mod_two (a : Bool) (x : ℕ) :
     bit a x % 2 = if a then 1 else 0 := by
-  simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, ← mul_two, Bool.cond_eq_ite]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, ← mul_two,
+  --   Bool.cond_eq_ite]
+  simp only [bit, ite_apply, bit1, bit0, ← mul_two, Bool.cond_eq_ite]
   split_ifs <;> simp [Nat.add_mod]
 
 @[simp]

Mathlib/Data/Rel.lean

@@ -149,11 +149,15 @@ theorem inv_comp (r : Rel α β) (s : Rel β γ) : inv (r • s) = inv s • inv
 
 @[simp]
 theorem inv_bot : (⊥ : Rel α β).inv = (⊥ : Rel β α) := by
-  simp [Bot.bot, inv, flip]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp [Bot.bot, inv, flip]
+  simp [Bot.bot, inv, Function.flip_def]
 
 @[simp]
 theorem inv_top : (⊤ : Rel α β).inv = (⊤ : Rel β α) := by
-  simp [Top.top, inv, flip]
+  -- Adaptation note: nightly-2024-03-16: simp was
+  -- simp [Top.top, inv, flip]
+  simp [Top.top, inv, Function.flip_def]
 
 /-- Image of a set under a relation -/
 def image (s : Set α) : Set β := { y | ∃ x ∈ s, r x y }

Mathlib/Data/Subtype.lean

@@ -203,6 +203,11 @@ def map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a →
 #align subtype.map Subtype.map
 #align subtype.map_coe Subtype.map_coe
 
+-- Adaptation note: nightly-2024-03-16: added to replace simp [Subtype.map]
+theorem map_def {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ a, p a → q (f a)) :
+    map f h = fun x ↦ ⟨f x, h x x.prop⟩ :=
+  rfl
+
 theorem map_comp {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : Subtype p}
     (f : α → β) (h : ∀ a, p a → q (f a)) (g : β → γ) (l : ∀ a, q a → r (g a)) :
     map g l (map f h x) = map (g ∘ f) (fun a ha ↦ l (f a) <| h a ha) x :=

Mathlib/Geometry/Euclidean/Inversion/Basic.lean

@@ -42,6 +42,11 @@ def inversion (c : P) (R : ℝ) (x : P) : P :=
   (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c
 #align euclidean_geometry.inversion EuclideanGeometry.inversion
 
+-- Adaptation note: nightly-2024-03-16: added to replace simp [inversion]
+theorem inversion_def :
+    inversion = fun (c : P) (R : ℝ) (x : P) => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c :=
+  rfl
+
 /-!
 ### Basic properties
 

Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

@@ -88,7 +88,9 @@ theorem hasFDerivAt_inversion (hx : x ≠ c) :
       ((R / dist x c) ^ 2 • (reflection (ℝ ∙ (x - c))ᗮ : F →L[ℝ] F)) x := by
   rcases add_left_surjective c x with ⟨x, rfl⟩
   have : HasFDerivAt (inversion c R) (_ : F →L[ℝ] F) (c + x) := by
-    simp (config := { unfoldPartialApp := true }) only [inversion]
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp (config := { unfoldPartialApp := true }) only [inversion]
+    simp only [inversion_def]
     simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]
     have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
     have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul

Mathlib/Init/Function.lean

@@ -28,7 +28,12 @@ attribute [eqns comp_def] comp
 
 lemma flip_def {f : α → β → φ} : flip f = fun b a => f a b := rfl
 
-attribute [eqns flip_def] flip
+-- Adaptation note: nightly-2024-03-16
+-- Because of changes in how equation lemmas are generated,
+-- `@[eqns]` will only work properly when used immediately after the definition
+-- (and when none of the default equation lemmas are needed).
+-- Thus this usage is no longer allowed:
+-- attribute [eqns flip_def] flip
 
 /-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
 and type of `f (g x)` depends on `x` and `g x`. -/
@@ -74,6 +79,9 @@ def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ
 def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := fun y x => f x y
 #align function.swap Function.swap
 
+-- Adaptation note: nightly-2024-03-16: added to replace simp [Function.swap]
+theorem swap_def {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : swap f = fun y x => f x y := rfl
+
 @[reducible, deprecated] -- Deprecated since 13 January 2024
 def app {β : α → Sort u₂} (f : ∀ x, β x) (x : α) : β x :=
   f x

Mathlib/Probability/Martingale/Upcrossing.lean

@@ -679,7 +679,10 @@ theorem crossing_pos_eq (hab : a < b) :
   have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]
   induction' n with k ih
   · refine' ⟨rfl, _⟩
-    simp (config := { unfoldPartialApp := true }) only [lowerCrossingTime_zero, hitting,
+    -- Adaptation note: nightly-2024-03-16: simp was
+    -- simp (config := { unfoldPartialApp := true }) only [lowerCrossingTime_zero, hitting,
+    --   Set.mem_Icc, Set.mem_Iic, Nat.zero_eq]
+    simp (config := { unfoldPartialApp := true }) only [lowerCrossingTime_zero, hitting_def,
       Set.mem_Icc, Set.mem_Iic, Nat.zero_eq]
     ext ω
     split_ifs with h₁ h₂ h₂