chore: adaptations for nightly-2024-06-19 (#13981)

This contains adaptations for 
* leanprover/lean4#4481
* leanprover/lean4#4497
* leanprover/lean4#4387 (Thanks to @JovanGerb  for these)
* leanprover/lean4#4487

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -148,7 +148,7 @@ section Terminal
 def punitIsTerminal : IsTerminal (CommRingCat.of.{u} PUnit) := by
   refine IsTerminal.ofUnique (h := fun X => ⟨⟨⟨⟨1, rfl⟩, fun _ _ => rfl⟩, ?_, ?_⟩, ?_⟩)
   · rfl
-  · intros; dsimp
+  · intros; simp; ext
   · intros f; ext; rfl
 set_option linter.uppercaseLean3 false in
 #align CommRing.punit_is_terminal CommRingCat.punitIsTerminal

Mathlib/Algebra/Group/Pi/Basic.lean

@@ -54,7 +54,12 @@ instance instOne [∀ i, One <| f i] : One (∀ i : I, f i) :=
 #align pi.has_one Pi.instOne
 #align pi.has_zero Pi.instZero
 
-@[to_additive (attr := simp)]
+#adaptation_note
+/--
+After https://github.com/leanprover/lean4/pull/4481
+the `simpNF` linter incorrectly claims this lemma can't be applied by `simp`.
+-/
+@[to_additive (attr := simp, nolint simpNF)]
 theorem one_apply [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 :=
   rfl
 #align pi.one_apply Pi.one_apply

Mathlib/Algebra/Lie/Classical.lean

@@ -179,14 +179,14 @@ theorem pso_inv {i : R} (hi : i * i = -1) : Pso p q R i * Pso p q R (-i) = 1 :=
   ext (x y); rcases x with ⟨x⟩|⟨x⟩ <;> rcases y with ⟨y⟩|⟨y⟩
   · -- x y : p
     by_cases h : x = y <;>
-    simp [Pso, indefiniteDiagonal, h]
+    simp [Pso, indefiniteDiagonal, h, one_apply]
   · -- x : p, y : q
     simp [Pso, indefiniteDiagonal]
   · -- x : q, y : p
     simp [Pso, indefiniteDiagonal]
   · -- x y : q
     by_cases h : x = y <;>
-    simp [Pso, indefiniteDiagonal, h, hi]
+    simp [Pso, indefiniteDiagonal, h, hi, one_apply]
 #align lie_algebra.orthogonal.Pso_inv LieAlgebra.Orthogonal.pso_inv
 
 /-- There is a constructive inverse of `Pso p q R i`. -/
@@ -199,14 +199,14 @@ theorem indefiniteDiagonal_transform {i : R} (hi : i * i = -1) :
   ext (x y); rcases x with ⟨x⟩|⟨x⟩ <;> rcases y with ⟨y⟩|⟨y⟩
   · -- x y : p
     by_cases h : x = y <;>
-    simp [Pso, indefiniteDiagonal, h]
+    simp [Pso, indefiniteDiagonal, h, one_apply]
   · -- x : p, y : q
     simp [Pso, indefiniteDiagonal]
   · -- x : q, y : p
     simp [Pso, indefiniteDiagonal]
   · -- x y : q
     by_cases h : x = y <;>
-    simp [Pso, indefiniteDiagonal, h, hi]
+    simp [Pso, indefiniteDiagonal, h, hi, one_apply]
 #align lie_algebra.orthogonal.indefinite_diagonal_transform LieAlgebra.Orthogonal.indefiniteDiagonal_transform
 
 /-- An equivalence between the indefinite and definite orthogonal Lie algebras, over a ring

Mathlib/Analysis/Analytic/Composition.lean

@@ -492,7 +492,7 @@ theorem comp_summable_nnreal (q : FormalMultilinearSeries 𝕜 F G) (p : FormalM
           (‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊) * r ^ n :=
         mul_le_mul' (q.compAlongComposition_nnnorm p c) le_rfl
       _ = ‖q c.length‖₊ * rq ^ n * ((∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n) * r0 ^ n := by
-        simp only [mul_pow]; ring
+        ring
       _ ≤ Cq * Cp ^ n * r0 ^ n := mul_le_mul' (mul_le_mul' A B) le_rfl
       _ = Cq / 4 ^ n := by
         simp only [r0]

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -439,8 +439,7 @@ theorem norm_iteratedFDerivWithin_comp_le_aux {Fu Gu : Type u} [NormedAddCommGro
     -- assumption for `g' ∘ f`).
     _ ≤ ∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * (i ! * C * D ^ i) * D ^ (n - i + 1) := by
       gcongr with i hi
-      · simp only [mul_assoc (n.choose i : ℝ)]
-        exact I i hi
+      · exact I i hi
       · exact J i
     -- We are left with trivial algebraic manipulations to see that this is smaller than
     -- the claimed bound.

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -67,7 +67,12 @@ end Module
 
 namespace FormalMultilinearSeries
 
-@[simp]
+#adaptation_note
+/--
+After https://github.com/leanprover/lean4/pull/4481
+the `simpNF` linter incorrectly claims this lemma can't be applied by `simp`.
+-/
+@[simp, nolint simpNF]
 theorem zero_apply (n : ℕ) : (0 : FormalMultilinearSeries 𝕜 E F) n = 0 := rfl
 
 @[simp]

Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

@@ -350,8 +350,7 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
   have : 𝓝 (0 : G) = 𝓝 (0 + 0 + 0) := by simp only [add_zero]
   rw [this]
   refine Tendsto.add (Tendsto.add ?_ ?_) ?_
-  · simp only
-    have := difference_quotients_converge_uniformly hf' hf hfg
+  · have := difference_quotients_converge_uniformly hf' hf hfg
     rw [Metric.tendstoUniformlyOnFilter_iff] at this
     rw [Metric.tendsto_nhds]
     intro ε hε

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -257,7 +257,8 @@ theorem _root_.IsSelfAdjoint.dense_domain (hA : IsSelfAdjoint A) : Dense (A.doma
     intro x
     rw [mem_adjoint_domain_iff, ← hA]
     refine (innerSL 𝕜 x).cont.comp ?_
-    simp [adjoint, h, continuous_const]
+    simp only [adjoint, h]
+    exact continuous_const
   simp [h'] at h
 
 end LinearPMap

Mathlib/Analysis/NormedSpace/PiLp.lean

@@ -99,7 +99,14 @@ variable [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
 variable [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] (c : 𝕜)
 variable (x y : PiLp p β) (i : ι)
 
-@[simp]
+#adaptation_note
+/--
+After https://github.com/leanprover/lean4/pull/4481
+the `simpNF` linter incorrectly claims this lemma can't be applied by `simp`.
+
+(It appears to also be unused in Mathlib.)
+-/
+@[simp, nolint simpNF]
 theorem zero_apply : (0 : PiLp p β) i = 0 :=
   rfl
 #align pi_Lp.zero_apply PiLp.zero_apply

Mathlib/CategoryTheory/GradedObject.lean

@@ -231,7 +231,12 @@ theorem shiftFunctor_map_apply {β : Type*} [AddCommGroup β] (s : β)
 instance [HasZeroMorphisms C] (β : Type w) (X Y : GradedObject β C) :
   Zero (X ⟶ Y) := ⟨fun _ => 0⟩
 
-@[simp]
+#adaptation_note
+/--
+After https://github.com/leanprover/lean4/pull/4481
+the `simpNF` linter incorrectly claims this lemma can't be applied by `simp`.
+-/
+@[simp, nolint simpNF]
 theorem zero_apply [HasZeroMorphisms C] (β : Type w) (X Y : GradedObject β C) (b : β) :
     (0 : X ⟶ Y) b = 0 :=
   rfl

Mathlib/CategoryTheory/Preadditive/Biproducts.lean

@@ -947,7 +947,7 @@ def preservesBiproductOfMonoBiproductComparison {f : J → C} [HasBiproduct f]
       (F.mapIso (biproduct.isoProduct f)).inv ≫
         biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
     ext j
-    convert piComparison_comp_π F f j; simp [← Functor.map_comp]
+    convert piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]
   haveI : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
   haveI : IsIso (piComparison F f) := by
     rw [that]

Mathlib/CategoryTheory/Sites/Canonical.lean

@@ -255,10 +255,10 @@ into the sheaf category.
 -/
 @[simps]
 def yoneda : C ⥤ Sheaf J (Type v) where
-  obj X := ⟨yoneda.obj X, by
+  obj X := ⟨CategoryTheory.yoneda.obj X, by
     rw [isSheaf_iff_isSheaf_of_type]
     apply hJ.isSheaf_of_representable⟩
-  map f := ⟨yoneda.map f⟩
+  map f := ⟨CategoryTheory.yoneda.map f⟩
 
 /--
 The yoneda embedding into the presheaf category factors through the one

Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean

@@ -57,7 +57,12 @@ instance : Group (ZeroCochain G U) := Pi.group
 
 namespace Cochain₀
 
-@[simp]
+#adaptation_note
+/--
+After https://github.com/leanprover/lean4/pull/4481
+the `simpNF` linter incorrectly claims this lemma can't be applied by `simp`.
+-/
+@[simp, nolint simpNF]
 lemma one_apply (i : I) : (1 : ZeroCochain G U) i = 1 := rfl
 
 @[simp]

Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

@@ -267,7 +267,7 @@ lemma FarFromTriangleFree.lt_half (hG : G.FarFromTriangleFree ε) : ε < 2⁻¹
     _ < card α ^ 2 := ?_
   rw [edgeFinset_top, filter_not, card_sdiff (subset_univ _), card_univ, Sym2.card,]
   simp_rw [choose_two_right, Nat.add_sub_cancel, Nat.mul_comm _ (card α),
-    Sym2.isDiag_iff_mem_range_diag, univ_filter_mem_range, mul_tsub,
+    funext (propext <| Sym2.isDiag_iff_mem_range_diag ·), univ_filter_mem_range, mul_tsub,
     Nat.mul_div_cancel' (card α).even_mul_succ_self.two_dvd]
   rw [card_image_of_injective _ Sym2.diag_injective, card_univ, mul_add_one (α := ℕ), two_mul, sq,
     add_tsub_add_eq_tsub_right]

Mathlib/Computability/TuringMachine.lean

@@ -92,7 +92,7 @@ theorem BlankExtends.refl {Γ} [Inhabited Γ] (l : List Γ) : BlankExtends l l :
 theorem BlankExtends.trans {Γ} [Inhabited Γ] {l₁ l₂ l₃ : List Γ} :
     BlankExtends l₁ l₂ → BlankExtends l₂ l₃ → BlankExtends l₁ l₃ := by
   rintro ⟨i, rfl⟩ ⟨j, rfl⟩
-  exact ⟨i + j, by simp [List.replicate_add]⟩
+  exact ⟨i + j, by simp⟩
 #align turing.blank_extends.trans Turing.BlankExtends.trans
 
 theorem BlankExtends.below_of_le {Γ} [Inhabited Γ] {l l₁ l₂ : List Γ} :

Mathlib/Data/DFinsupp/Basic.lean

@@ -685,7 +685,7 @@ theorem filter_single (p : ι → Prop) [DecidablePred p] (i : ι) (x : β i) :
   rw [filter_apply, this]
   obtain rfl | hij := Decidable.eq_or_ne i j
   · rfl
-  · rw [single_eq_of_ne hij, ite_self, ite_self]
+  · rw [single_eq_of_ne hij, ite_self, Pi.zero_apply, ite_self]
 #align dfinsupp.filter_single DFinsupp.filter_single
 
 @[simp]

Mathlib/Data/Finset/Basic.lean

@@ -3355,7 +3355,7 @@ theorem mem_toList {a : α} {s : Finset α} : a ∈ s.toList ↔ a ∈ s :=
 
 @[simp]
 theorem toList_eq_nil {s : Finset α} : s.toList = [] ↔ s = ∅ :=
-  toList_eq_nil.trans val_eq_zero
+  Multiset.toList_eq_nil.trans val_eq_zero
 #align finset.to_list_eq_nil Finset.toList_eq_nil
 
 @[simp]

Mathlib/Data/Finset/Card.lean

@@ -69,7 +69,7 @@ theorem card_le_card : s ⊆ t → s.card ≤ t.card :=
 theorem card_mono : Monotone (@card α) := by apply card_le_card
 #align finset.card_mono Finset.card_mono
 
-@[simp] lemma card_eq_zero : s.card = 0 ↔ s = ∅ := card_eq_zero.trans val_eq_zero
+@[simp] lemma card_eq_zero : s.card = 0 ↔ s = ∅ := Multiset.card_eq_zero.trans val_eq_zero
 lemma card_ne_zero : s.card ≠ 0 ↔ s.Nonempty := card_eq_zero.ne.trans nonempty_iff_ne_empty.symm
 @[simp] lemma card_pos : 0 < s.card ↔ s.Nonempty := Nat.pos_iff_ne_zero.trans card_ne_zero
 @[simp] lemma one_le_card : 1 ≤ s.card ↔ s.Nonempty := card_pos

Mathlib/Data/Finsupp/Basic.lean

@@ -1741,7 +1741,10 @@ theorem extendDomain_subtypeDomain (f : α →₀ M) (hf : ∀ a ∈ f.support,
   ext a
   by_cases h : P a
   · exact dif_pos h
-  · dsimp
+  · #adaptation_note
+    /-- Prior to nightly-2024-06-18, this `rw` was done by `dsimp`. -/
+    rw [extendDomain_toFun]
+    dsimp
     rw [if_neg h, eq_comm, ← not_mem_support_iff]
     refine mt ?_ h
     exact @hf _
@@ -1750,7 +1753,9 @@ theorem extendDomain_subtypeDomain (f : α →₀ M) (hf : ∀ a ∈ f.support,
 theorem extendDomain_single (a : Subtype P) (m : M) :
     (single a m).extendDomain = single a.val m := by
   ext a'
-  dsimp only [extendDomain_toFun]
+  #adaptation_note
+  /-- Prior to nightly-2024-06-18, this `rw` was instead `dsimp only`. -/
+  rw [extendDomain_toFun]
   obtain rfl | ha := eq_or_ne a.val a'
   · simp_rw [single_eq_same, dif_pos a.prop]
   · simp_rw [single_eq_of_ne ha, dite_eq_right_iff]

Mathlib/Data/Finsupp/ToDFinsupp.lean

@@ -259,8 +259,7 @@ def finsuppLequivDFinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M]
 @[simp]
 theorem finsuppLequivDFinsupp_apply_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]
     [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
-      (↑(finsuppLequivDFinsupp (M := M) R) : (ι →₀ M) → _) = Finsupp.toDFinsupp := by
-       simp only [@LinearEquiv.coe_coe]; rfl
+    (↑(finsuppLequivDFinsupp (M := M) R) : (ι →₀ M) → _) = Finsupp.toDFinsupp := rfl
 
 @[simp]
 theorem finsuppLequivDFinsupp_symm_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]

Mathlib/Data/List/Basic.lean

@@ -408,13 +408,11 @@ theorem append_left_injective (t : List α) : Injective fun s ↦ s ++ t :=
 
 /-! ### replicate -/
 
-@[simp] lemma replicate_zero (a : α) : replicate 0 a = [] := rfl
 #align list.replicate_zero List.replicate_zero
 
 attribute [simp] replicate_succ
 #align list.replicate_succ List.replicate_succ
 
-lemma replicate_one (a : α) : replicate 1 a = [a] := rfl
 #align list.replicate_one List.replicate_one
 
 #align list.length_replicate List.length_replicate
@@ -431,7 +429,7 @@ theorem eq_replicate_length {a : α} : ∀ {l : List α}, l = replicate l.length
 #align list.eq_replicate List.eq_replicate
 
 theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a := by
-  induction m <;> simp [*, succ_add, replicate]
+  rw [append_replicate_replicate]
 #align list.replicate_add List.replicate_add
 
 theorem replicate_succ' (n) (a : α) : replicate (n + 1) a = replicate n a ++ [a] :=
@@ -446,17 +444,12 @@ theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = r
   simp only [eq_replicate, subset_def, mem_singleton, exists_eq_left']
 #align list.subset_singleton_iff List.subset_singleton_iff
 
-@[simp] theorem map_replicate (f : α → β) (n) (a : α) :
-    map f (replicate n a) = replicate n (f a) := by
-  induction n <;> [rfl; simp only [*, replicate, map]]
 #align list.map_replicate List.map_replicate
 
 @[simp] theorem tail_replicate (a : α) (n) :
     tail (replicate n a) = replicate (n - 1) a := by cases n <;> rfl
 #align list.tail_replicate List.tail_replicate
 
-@[simp] theorem join_replicate_nil (n : ℕ) : join (replicate n []) = @nil α := by
-  induction n <;> [rfl; simp only [*, replicate, join, append_nil]]
 #align list.join_replicate_nil List.join_replicate_nil
 
 theorem replicate_right_injective {n : ℕ} (hn : n ≠ 0) : Injective (@replicate α n) :=
@@ -468,7 +461,7 @@ theorem replicate_right_inj {a b : α} {n : ℕ} (hn : n ≠ 0) :
   (replicate_right_injective hn).eq_iff
 #align list.replicate_right_inj List.replicate_right_inj
 
-@[simp] theorem replicate_right_inj' {a b : α} : ∀ {n},
+theorem replicate_right_inj' {a b : α} : ∀ {n},
     replicate n a = replicate n b ↔ n = 0 ∨ a = b
   | 0 => by simp
   | n + 1 => (replicate_right_inj n.succ_ne_zero).trans <| by simp only [n.succ_ne_zero, false_or]
@@ -478,7 +471,7 @@ theorem replicate_left_injective (a : α) : Injective (replicate · a) :=
   LeftInverse.injective (length_replicate · a)
 #align list.replicate_left_injective List.replicate_left_injective
 
-@[simp] theorem replicate_left_inj {a : α} {n m : ℕ} : replicate n a = replicate m a ↔ n = m :=
+theorem replicate_left_inj {a : α} {n m : ℕ} : replicate n a = replicate m a ↔ n = m :=
   (replicate_left_injective a).eq_iff
 #align list.replicate_left_inj List.replicate_left_inj
 
@@ -592,10 +585,6 @@ theorem map_reverseAux (f : α → β) (l₁ l₂ : List α) :
 
 #align list.mem_reverse List.mem_reverse
 
-@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a :=
-  eq_replicate.2
-    ⟨by rw [length_reverse, length_replicate],
-     fun b h => eq_of_mem_replicate (mem_reverse.1 h)⟩
 #align list.reverse_replicate List.reverse_replicate
 
 /-! ### empty -/
@@ -695,11 +684,13 @@ theorem getLast?_cons_cons (a b : α) (l : List α) :
     getLast? (a :: b :: l) = getLast? (b :: l) := rfl
 
 @[simp]
-theorem getLast?_isNone : ∀ {l : List α}, (getLast? l).isNone ↔ l = []
+theorem getLast?_eq_none : ∀ {l : List α}, getLast? l = none ↔ l = []
   | [] => by simp
   | [a] => by simp
-  | a :: b :: l => by simp [@getLast?_isNone (b :: l)]
-#align list.last'_is_none List.getLast?_isNone
+  | a :: b :: l => by simp [@getLast?_eq_none (b :: l)]
+#align list.last'_is_none List.getLast?_eq_none
+
+@[deprecated (since := "2024-06-20")] alias getLast?_isNone := getLast?_eq_none
 
 @[simp]
 theorem getLast?_isSome : ∀ {l : List α}, l.getLast?.isSome ↔ l ≠ []
@@ -1358,7 +1349,7 @@ theorem ext_get?' {l₁ l₂ : List α} (h' : ∀ n < max l₁.length l₂.lengt
   intro n
   rcases Nat.lt_or_ge n <| max l₁.length l₂.length with hn | hn
   · exact h' n hn
-  · simp_all [Nat.max_le, getElem?_eq_none.mpr]
+  · simp_all [Nat.max_le, getElem?_eq_none]
 
 theorem ext_get?_iff {l₁ l₂ : List α} : l₁ = l₂ ↔ ∀ n, l₁.get? n = l₂.get? n :=
   ⟨by rintro rfl _; rfl, ext_get?⟩
@@ -2913,12 +2904,12 @@ theorem Sublist.map (f : α → β) {l₁ l₂ : List α} (s : l₁ <+ l₂) : m
 
 theorem filterMap_eq_bind_toList (f : α → Option β) (l : List α) :
     l.filterMap f = l.bind fun a ↦ (f a).toList := by
-  induction' l with a l ih <;> simp
+  induction' l with a l ih <;> simp [filterMap_cons]
   rcases f a <;> simp [ih]
 
 theorem filterMap_congr {f g : α → Option β} {l : List α}
     (h : ∀ x ∈ l, f x = g x) : l.filterMap f = l.filterMap g := by
-  induction' l with a l ih <;> simp
+  induction' l with a l ih <;> simp [filterMap_cons]
   simp [ih (fun x hx ↦ h x (List.mem_cons_of_mem a hx))]
   cases' hfa : f a with b
   · have : g a = none := Eq.symm (by simpa [hfa] using h a (by simp))
@@ -2931,7 +2922,7 @@ theorem filterMap_eq_map_iff_forall_eq_some {f : α → Option β} {g : α → 
   mp := by
     induction' l with a l ih
     · simp
-    cases' ha : f a with b <;> simp [ha]
+    cases' ha : f a with b <;> simp [ha, filterMap_cons]
     · intro h
       simpa [show (filterMap f l).length = l.length + 1 from by simp[h], Nat.add_one_le_iff]
         using List.length_filterMap_le f l
@@ -3089,12 +3080,6 @@ theorem dropWhile_eq_nil_iff : dropWhile p l = [] ↔ ∀ x ∈ l, p x := by
   · by_cases hp : p x <;> simp [hp, dropWhile, IH]
 #align list.drop_while_eq_nil_iff List.dropWhile_eq_nil_iff
 
-theorem takeWhile_cons {x : α} :
-    List.takeWhile p (x :: l) = (match p x with
-      | true  => x :: takeWhile p l
-      | false => []) :=
-  rfl
-
 theorem takeWhile_cons_of_pos {x : α} (h : p x) :
     List.takeWhile p (x :: l) = x :: takeWhile p l := by
   simp [takeWhile_cons, h]

Mathlib/Data/List/GetD.lean

@@ -73,7 +73,7 @@ alias getD_singleton_default_eq := getElem?_getD_singleton_default_eq
 theorem getElem?_getD_replicate_default_eq (r n : ℕ) : (replicate r d)[n]?.getD d = d := by
   induction r generalizing n with
   | zero => simp
-  | succ n ih => simp at ih; cases n <;> simp [ih]
+  | succ n ih => simp at ih; cases n <;> simp [ih, replicate_succ]
 #align list.nthd_replicate_default_eq List.getElem?_getD_replicate_default_eqₓ -- argument order
 
 @[deprecated (since := "2024-06-12")]