Squashed commit of lean-pr-testing-4154

commit 6d957dc
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 22 15:10:57 2024 +0200

    Fix proof

commit 5b95381
Merge: 48bea5e bc78dd4
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 22 11:24:01 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 48bea5e
Author: Joachim Breitner <[email protected]>
Date:   Wed Aug 21 18:35:50 2024 +0200

    Switch to Mathlib.Init

commit 4d38bbd
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Wed Aug 21 18:25:08 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit f84b84d
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Wed Aug 21 09:58:00 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit f958309
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Wed Aug 21 09:39:13 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 4b976ec
Author: Joachim Breitner <[email protected]>
Date:   Wed Aug 21 10:54:32 2024 +0200

    Try to remove some nolints

commit 0cbb129
Author: Joachim Breitner <[email protected]>
Date:   Wed Aug 21 10:53:14 2024 +0200

    Reduce diff

commit a485ac8
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Tue Aug 20 08:02:41 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit b5cb54a
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon Aug 19 13:09:14 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 8b1ce21
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 12:56:07 2024 +0200

    Like this?

commit e6ce4b5
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:38:06 2024 +0200

    nolint attributes

commit e24f1c6
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:15:52 2024 +0200

    Another simp only gone

commit a9d54a8
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:11:30 2024 +0200

    aesop_cat broke :-(

commit b4edcec
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:03:43 2024 +0200

    Use dsimp only

commit 8e66ddd
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:28:04 2024 +0200

    Fixes in ComposableArrows

commit 471b000
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:18:56 2024 +0200

    Use cond_false

commit 8120390
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:14:41 2024 +0200

    No rfl after simp needed anymore

commit 0544693
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:13:00 2024 +0200

    Less dsimp only

commit 5cffe6e
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:10:21 2024 +0200

    More autoParam

commit 8e019f8
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:16:43 2024 +0200

    More fixes

commit 7b6f094
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:13:46 2024 +0200

    More fixes

commit 3151f57
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:10:35 2024 +0200

    More [autoParam]

commit 54a6616
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:07:19 2024 +0200

    Some fixes

commit 9c41f64
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 12:15:03 2024 +0200

    Check for cold cache

commit 66ff376
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 14:54:25 2024 +0200

    No longer needed dsimps?

commit 2298410
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 12:24:02 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 8bca337
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 12:17:43 2024 +0200

    Some reasonable fixes

commit 14247a2
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 12:16:08 2024 +0200

    Revert "work-around dsimp Function.eval"

    This reverts commit 8c36154.

commit 0c86721
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 10:35:28 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 4b2124e
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 09:45:57 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 125f713
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 08:51:57 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit af7ab6c
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 08:16:31 2024 +0200

    Style exception

commit f11401e
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 08:08:49 2024 +0200

    toAdditive: transport MatcherInfo

commit 8c36154
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 15 18:27:00 2024 +0200

    work-around dsimp Function.eval

commit 5fcef86
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 14:24:51 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit d4e2758
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 13:59:06 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit af1456c
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 15 15:49:23 2024 +0200

    Fix call to getEqnsFor?

commit c62ab2f
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 12:30:12 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit d9bc3e9
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 11:47:22 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 40bc4fe
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 15 10:50:26 2024 +0000

    chore: do not set release-ci label upon failed PR test (#15775)

    with leanprover/lean4#5022 the need for this
    should have disappeared

commit 2ff3b31
Merge: 33a583e b8ad879
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 10:32:05 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 33a583e
Merge: 1c951db 85647f2
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon Jun 3 15:24:02 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 1c951db
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon May 13 18:13:38 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit f05d463
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon May 13 17:26:47 2024 +0000

    Update lean-toolchain for testing leanprover/lean4#4154

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -249,7 +249,7 @@ theorem of_s_head_aux (v : K) : (of v).s.get? 0 = (IntFractPair.stream v 1).bind
   rw [of, IntFractPair.seq1]
   simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head,
     Stream'.Seq.get?, Stream'.map]
-  rw [← Stream'.get_succ, Stream'.get, Option.map]
+  rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
   split <;> simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]
 
 /-- This gives the first pair of coefficients of the continued fraction of a non-integer `v`.

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -159,7 +159,7 @@ lemma exact_iff_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) :
 lemma exact₀ (S : ComposableArrows C 0) : S.Exact where
   toIsComplex := S.isComplex₀
   -- See https://github.com/leanprover/lean4/issues/2862
-  exact i hi := by simp [autoParam] at hi
+  exact i hi := by simp at hi
 
 lemma exact₁ (S : ComposableArrows C 1) : S.Exact where
   toIsComplex := S.isComplex₁

Mathlib/AlgebraicTopology/DoldKan/Normalized.lean

@@ -124,10 +124,13 @@ def N₁_iso_normalizedMooreComplex_comp_toKaroubi : N₁ ≅ normalizedMooreCom
           comm := by erw [inclusionOfMooreComplexMap_comp_PInfty, id_comp] }
       naturality := fun X Y f => by
         ext
-        simp only [Functor.comp_map, normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f,
-          HomologicalComplex.comp_f, NormalizedMooreComplex.map_f,
-          inclusionOfMooreComplexMap_f, factorThru_arrow, N₁_map_f,
-          inclusionOfMooreComplexMap_comp_PInfty_assoc, AlternatingFaceMapComplex.map_f] }
+        simp only [Functor.comp_obj, normalizedMooreComplex_obj, toKaroubi_obj_X,
+          NormalizedMooreComplex.obj_X, N₁_obj_X, AlternatingFaceMapComplex.obj_X, Functor.comp_map,
+          normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f, HomologicalComplex.comp_f,
+          NormalizedMooreComplex.map_f, inclusionOfMooreComplexMap_f, NormalizedMooreComplex.objX,
+          factorThru_arrow, N₁_map_f, inclusionOfMooreComplexMap_comp_PInfty_assoc,
+          AlternatingFaceMapComplex.map_f]
+         }
   hom_inv_id := by
     ext X : 3
     simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,

Mathlib/CategoryTheory/GradedObject/Monoidal.lean

@@ -292,7 +292,13 @@ lemma associator_naturality (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃
     [HasGoodTensor₁₂Tensor X₁ X₂ X₃] [HasGoodTensorTensor₂₃ X₁ X₂ X₃]
     [HasGoodTensor₁₂Tensor Y₁ Y₂ Y₃] [HasGoodTensorTensor₂₃ Y₁ Y₂ Y₃] :
     tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
-      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by aesop_cat
+      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by
+        -- this used to be aesop_cat, but that broke with
+        -- https://github.com/leanprover/lean4/pull/4154
+        ext x i₁ i₂ i₃ h : 2
+        simp only [categoryOfGradedObjects_comp, ιTensorObj₃'_tensorHom_assoc,
+          associator_conjugation, ιTensorObj₃'_associator_hom, assoc, Iso.inv_hom_id_assoc,
+          ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_tensorHom]
 
 end
 
@@ -399,18 +405,18 @@ lemma pentagon_inv :
         tensorHom (associator X₁ X₂ X₃).inv (𝟙 X₄) =
     (associator X₁ X₂ (tensorObj X₃ X₄)).inv ≫ (associator (tensorObj X₁ X₂) X₃ X₄).inv := by
   ext j i₁ i₂ i₃ i₄ h
-  dsimp
+  dsimp only [categoryOfGradedObjects_comp]
   conv_lhs =>
     rw [ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h _ rfl, assoc, ι_tensorHom_assoc]
-    dsimp
+    dsimp only [categoryOfGradedObjects_id, id_eq, eq_mpr_eq_cast, cast_eq]
     rw [id_tensorHom, ← MonoidalCategory.whiskerLeft_comp_assoc, ιTensorObj₃_associator_inv,
       ιTensorObj₃'_eq X₂ X₃ X₄ i₂ i₃ i₄ _ rfl _ rfl, MonoidalCategory.whiskerLeft_comp_assoc,
       MonoidalCategory.whiskerLeft_comp_assoc,
       ← ιTensorObj₃_eq_assoc X₁ (tensorObj X₂ X₃) X₄ i₁ (i₂ + i₃) i₄ j
         (by simp only [← add_assoc, h]) _ rfl, ιTensorObj₃_associator_inv_assoc,
       ιTensorObj₃'_eq_assoc X₁ (tensorObj X₂ X₃) X₄ i₁ (i₂ + i₃) i₄ j
         (by simp only [← add_assoc, h]) (i₁ + i₂ + i₃) (by rw [add_assoc]), ι_tensorHom]
-    dsimp
+    dsimp only [id_eq, eq_mpr_eq_cast, categoryOfGradedObjects_id]
     rw [tensorHom_id, whisker_assoc_symm_assoc, Iso.hom_inv_id_assoc,
       ← MonoidalCategory.comp_whiskerRight_assoc, ← MonoidalCategory.comp_whiskerRight_assoc,
       ← ιTensorObj₃_eq X₁ X₂ X₃ i₁ i₂ i₃ _ rfl _ rfl, ιTensorObj₃_associator_inv,

Mathlib/CategoryTheory/WithTerminal.lean

@@ -70,6 +70,7 @@ def Hom : WithTerminal C → WithTerminal C → Type v
   | of X, of Y => X ⟶ Y
   | star, of _ => PEmpty
   | _, star => PUnit
+attribute [nolint simpNF] Hom.eq_3
 
 /-- Identity morphisms for `WithTerminal C`. -/
 @[simp]
@@ -85,6 +86,8 @@ def comp : ∀ {X Y Z : WithTerminal C}, Hom X Y → Hom Y Z → Hom X Z
   | star, of _X, _ => fun f _g => PEmpty.elim f
   | _, star, of _Y => fun _f g => PEmpty.elim g
   | star, star, star => fun _ _ => PUnit.unit
+attribute [nolint simpNF] comp.eq_3
+attribute [nolint simpNF] comp.eq_4
 
 instance : Category.{v} (WithTerminal C) where
   Hom X Y := Hom X Y
@@ -371,6 +374,7 @@ def Hom : WithInitial C → WithInitial C → Type v
   | of X, of Y => X ⟶ Y
   | of _, _ => PEmpty
   | star, _ => PUnit
+attribute [nolint simpNF] Hom.eq_2
 
 /-- Identity morphisms for `WithInitial C`. -/
 @[simp]
@@ -386,6 +390,8 @@ def comp : ∀ {X Y Z : WithInitial C}, Hom X Y → Hom Y Z → Hom X Z
   | _, of _X, star => fun _f g => PEmpty.elim g
   | of _Y, star, _ => fun f _g => PEmpty.elim f
   | star, star, star => fun _ _ => PUnit.unit
+attribute [nolint simpNF] comp.eq_3
+attribute [nolint simpNF] comp.eq_4
 
 instance : Category.{v} (WithInitial C) where
   Hom X Y := Hom X Y

Mathlib/Computability/TMToPartrec.lean

@@ -898,6 +898,7 @@ def natEnd : Γ' → Bool
   | Γ'.consₗ => true
   | Γ'.cons => true
   | _ => false
+attribute [nolint simpNF] natEnd.eq_3
 
 /-- Pop a value from the stack and place the result in local store. -/
 @[simp]

Mathlib/Computability/TuringMachine.lean

@@ -2353,7 +2353,7 @@ theorem tr_respects_aux₂ [DecidableEq K] {k : K} {q : Stmt₂₁} {v : σ} {S
     · refine
         ⟨_, fun k' ↦ ?_, by
           erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst,
-            cond, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
+            cond_false, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head,
             Tape.mk'_nth_nat, Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k none),
             addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd,
             stk_nth_val _ (hL k), e,
@@ -2487,7 +2487,6 @@ theorem trCfg_init (k) (L : List (Γ k)) : TrCfg (TM2.init k L) (TM1.init (trIni
       rw [ListBlank.nth_mk, List.getI_eq_iget_get?, List.map, List.reverse_nil]
       cases L.reverse.get? i <;> rfl
   · rw [trInit, TM1.init]
-    dsimp only
     congr <;> cases L.reverse <;> try rfl
     simp only [List.map_map, List.tail_cons, List.map]
     rfl

Mathlib/Data/PFunctor/Multivariate/W.lean

@@ -169,7 +169,7 @@ theorem wRec_eq {α : TypeVec n} {C : Type*}
     (g : ∀ a : P.A, P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C) (a : P.A)
     (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) :
     P.wRec g (P.wMk a f' f) = g a f' f fun i => P.wRec g (f i) := by
-  rw [wMk, wRec]; dsimp; rw [wpRec_eq]
+  rw [wMk, wRec]; rw [wpRec_eq]
   dsimp only [wPathDestLeft_wPathCasesOn, wPathDestRight_wPathCasesOn]
   congr
 

Mathlib/Data/PFunctor/Univariate/M.lean

@@ -281,9 +281,7 @@ theorem mk_dest (x : M F) : M.mk (dest x) = x := by
   cases' h : x.approx (succ n) with _ hd ch
   have h' : hd = head' (x.approx 1) := by
     rw [← head_succ' n, h, head']
-    · split
-      injections
-    · apply x.consistent
+    apply x.consistent
   revert ch
   rw [h']
   intros ch h

Mathlib/Data/Seq/Computation.lean

@@ -246,6 +246,7 @@ def BisimO : α ⊕ (Computation α) → α ⊕ (Computation α) → Prop
   | _, _ => False
 
 attribute [simp] BisimO
+attribute [nolint simpNF] BisimO.eq_3
 
 /-- Attribute expressing bisimilarity over two `Computation`s-/
 def IsBisimulation :=

Mathlib/Data/Seq/Parallel.lean

@@ -128,7 +128,6 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
     · have C : corec parallel.aux1 (l, S) = pure a := by
         apply destruct_eq_pure
         rw [corec_eq, parallel.aux1]
-        dsimp only []
         rw [h]
         simp only [rmap]
       rw [C]
@@ -146,7 +145,6 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
     · have C : corec parallel.aux1 (l, S) = pure a := by
         apply destruct_eq_pure
         rw [corec_eq, parallel.aux1]
-        dsimp only []
         rw [h]
         simp only [rmap]
       rw [C]

Mathlib/Data/Seq/Seq.lean

@@ -315,6 +315,7 @@ def BisimO : Option (Seq1 α) → Option (Seq1 α) → Prop
   | _, _ => False
 
 attribute [simp] BisimO
+attribute [nolint simpNF] BisimO.eq_3
 
 /-- a relation is bisimilar if it meets the `BisimO` test-/
 def IsBisimulation :=

Mathlib/Data/Seq/WSeq.lean

@@ -394,6 +394,7 @@ def LiftRelO (R : α → β → Prop) (C : WSeq α → WSeq β → Prop) :
   | none, none => True
   | some (a, s), some (b, t) => R a b ∧ C s t
   | _, _ => False
+attribute [nolint simpNF] LiftRelO.eq_3
 
 theorem LiftRelO.imp {R S : α → β → Prop} {C D : WSeq α → WSeq β → Prop} (H1 : ∀ a b, R a b → S a b)
     (H2 : ∀ s t, C s t → D s t) : ∀ {o p}, LiftRelO R C o p → LiftRelO S D o p

Mathlib/RingTheory/Binomial.lean

@@ -241,7 +241,7 @@ instance Int.instBinomialRing : BinomialRing ℤ where
   nsmul_right_injective n hn r s hrs := Int.eq_of_mul_eq_mul_left (Int.ofNat_ne_zero.mpr hn) hrs
   multichoose := Int.multichoose
   factorial_nsmul_multichoose r k := by
-    rw [Int.multichoose, nsmul_eq_mul]
+    rw [Int.multichoose.eq_def, nsmul_eq_mul]
     cases r with
     | ofNat n =>
       simp only [multichoose, nsmul_eq_mul, Int.ofNat_eq_coe, Int.ofNat_mul_out]

Mathlib/RingTheory/IsAdjoinRoot.lean

@@ -393,12 +393,10 @@ def basis (h : IsAdjoinRootMonic S f) : Basis (Fin (natDegree f)) R S :=
         ext i
         simp only [h.modByMonicHom_map, Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]
         rw [(Polynomial.modByMonic_eq_self_iff h.Monic).mpr, Polynomial.coeff]
-        · dsimp only -- Porting note (#10752): added `dsimp only`
-          rw [Finsupp.mapDomain_apply Fin.val_injective]
+        · rw [Finsupp.mapDomain_apply Fin.val_injective]
         rw [degree_eq_natDegree h.Monic.ne_zero, degree_lt_iff_coeff_zero]
         intro m hm
         rw [Polynomial.coeff]
-        dsimp only -- Porting note (#10752): added `dsimp only`
         rw [Finsupp.mapDomain_notin_range]
         rw [Set.mem_range, not_exists]
         rintro i rfl

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -1572,21 +1572,21 @@ theorem coprime_iff_inf_one {a b : α} (ha0 : a ≠ 0) (hb0 : b ≠ 0) :
 theorem factors_self [Nontrivial α] {p : Associates α} (hp : Irreducible p) :
     p.factors = WithTop.some {⟨p, hp⟩} :=
   eq_of_prod_eq_prod
-    (by rw [factors_prod, FactorSet.prod]; dsimp; rw [prod_singleton])
+    (by rw [factors_prod, FactorSet.prod.eq_def]; dsimp; rw [prod_singleton])
 
 theorem factors_prime_pow [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ℕ) :
     factors (p ^ k) = WithTop.some (Multiset.replicate k ⟨p, hp⟩) :=
   eq_of_prod_eq_prod
     (by
-      rw [Associates.factors_prod, FactorSet.prod]
+      rw [Associates.factors_prod, FactorSet.prod.eq_def]
       dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])
 
 theorem prime_pow_le_iff_le_bcount [DecidableEq (Associates α)] {m p : Associates α}
     (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} : p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors := by
   rcases Associates.exists_non_zero_rep h₁ with ⟨m, hm, rfl⟩
   have := nontrivial_of_ne _ _ hm
-  rw [bcount, factors_mk, Multiset.le_count_iff_replicate_le, ← factors_le, factors_prime_pow,
-    factors_mk, WithTop.coe_le_coe] <;> assumption
+  rw [bcount.eq_def, factors_mk, Multiset.le_count_iff_replicate_le, ← factors_le,
+    factors_prime_pow, factors_mk, WithTop.coe_le_coe] <;> assumption
 
 @[simp]
 theorem factors_one [Nontrivial α] : factors (1 : Associates α) = 0 := by

Mathlib/Tactic/ToAdditive/Frontend.lean

@@ -818,10 +818,7 @@ partial def transformDeclAux
   if isProtected (← getEnv) src then
     setEnv <| addProtected (← getEnv) tgt
   if let some matcherInfo ← getMatcherInfo? src then
-    -- Use
-    --   Match.addMatcherInfo tgt matcherInfo
-    -- once on lean 4.13.
-    modifyEnv fun env => Match.Extension.addMatcherInfo env tgt matcherInfo
+    Match.addMatcherInfo tgt matcherInfo
 
 /-- Copy the instance attribute in a `to_additive`
 

Mathlib/Topology/UniformSpace/CompactConvergence.lean

@@ -330,7 +330,7 @@ theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} [TopologicalS
   have h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂ := fun K ↦ h_proper₂.isCompact_preimage
   have h_cover' : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂ := fun S _ ↦ h_cover ▸ subset_univ _
   -- ... and we just pull it back.
-  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq, inferInstanceAs, inferInstance,
+  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq,
     UniformOnFun.uniformSpace_eq_inf_precomp_of_cover _ _ _ _ _
       h_image₁ h_image₂ h_preimage₁ h_preimage₂ h_cover',
     UniformSpace.comap_inf, ← UniformSpace.comap_comap]
@@ -351,7 +351,7 @@ theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} [∀ i, Topolo
       inter_eq_right.mp ?_⟩
     simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
   -- ... and we just pull it back.
-  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq, inferInstanceAs, inferInstance,
+  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq,
     UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover',
     UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
   rfl

lakefile.lean

@@ -42,11 +42,15 @@ package mathlib where
 ## Mathlib dependencies on upstream projects.
 -/
 
-require "leanprover-community" / "batteries" @ git "nightly-testing"
-require "leanprover-community" / "Qq" @ git "nightly-testing"
-require "leanprover-community" / "aesop" @ git "nightly-testing"
-require "leanprover-community" / "proofwidgets" @ git "v0.0.42-pre2"
-require "leanprover-community" / "importGraph" @ git "main"
+meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+
+require batteries from git "https://github.com/leanprover-community/batteries" @ "nightly-testing-2024-05-11"
+require Qq from git "https://github.com/leanprover-community/quote4" @ "nightly-testing"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "nightly-testing"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.36"
+require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
+require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"
 
 /-!
 ## Mathlib libraries

scripts/style-exceptions.txt

@@ -55,7 +55,7 @@ Mathlib/SetTheory/Game/PGame.lean : line 1 : ERR_NUM_LIN : 1900 file contains 17
 Mathlib/SetTheory/Ordinal/Arithmetic.lean : line 1 : ERR_NUM_LIN : 2400 file contains 2269 lines, try to split it up
 Mathlib/SetTheory/ZFC/Basic.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1549 lines, try to split it up
 Mathlib/Tactic/CC/Addition.lean : line 1 : ERR_NUM_LIN : 2300 file contains 2100 lines, try to split it up
-Mathlib/Tactic/ToAdditive/Frontend.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1502 lines, try to split it up
+Mathlib/Tactic/ToAdditive/Frontend.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1504 lines, try to split it up
 Mathlib/Topology/Algebra/Group/Basic.lean : line 1 : ERR_NUM_LIN : 2100 file contains 1932 lines, try to split it up
 Mathlib/Topology/Algebra/Module/Basic.lean : line 1 : ERR_NUM_LIN : 2600 file contains 2405 lines, try to split it up
 Mathlib/Topology/Basic.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1731 lines, try to split it up