chore: adaptations for nightly-2024-11-14 (#19059)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Mathlib/Algebra/Category/Ring/Epi.lean

@@ -24,7 +24,7 @@ lemma CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S]
   constructor
   · intro H
     have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom (R := R))
-      (CommRingCat.ofHom <| Algebra.TensorProduct.includeRight.toRingHom)
+      (CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom)
       (by ext r; show algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
           simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])
     exact RingHom.congr_fun this

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -212,7 +212,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal
   set K := s'.sup id
   suffices I ≤ K by
     obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
-    exact ⟨t, hts'.trans hs'.subset, htI⟩
+    exact ⟨t, Finset.Subset.trans hts' hs'.subset, htI⟩
   -- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
   -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
   intro x hx

Mathlib/Algebra/Ring/Subring/Defs.lean

@@ -98,15 +98,16 @@ instance (priority := 75) toHasIntCast : IntCast s :=
 -- Prefer subclasses of `Ring` over subclasses of `SubringClass`.
 /-- A subring of a ring inherits a ring structure -/
 instance (priority := 75) toRing : Ring s :=
-  Subtype.coe_injective.ring (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
+  Subtype.coe_injective.ring Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
     (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl
 
 -- Prefer subclasses of `Ring` over subclasses of `SubringClass`.
 /-- A subring of a `CommRing` is a `CommRing`. -/
 instance (priority := 75) toCommRing {R} [CommRing R] [SetLike S R] [SubringClass S R] :
     CommRing s :=
-  Subtype.coe_injective.commRing (↑) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
-    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl
+  Subtype.coe_injective.commRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl)
+    (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
+    (fun _ => rfl) fun _ => rfl
 
 -- Prefer subclasses of `Ring` over subclasses of `SubringClass`.
 /-- A subring of a domain is a domain. -/

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -294,7 +294,7 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb :
   #adaptation_note /-- 2024-11-10 added `(R := A)` -/
   conv_rhs =>
     rw [← sq_le_one_iff₀ (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul,
-      IsSelfAdjoint.of_nonneg (R := A)sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg,
+      IsSelfAdjoint.of_nonneg (R := A) sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg,
       ← mul_assoc, mul_assoc _ _ (sqrt a), sqrt_mul_sqrt_self a,
       CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab]
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -157,8 +157,14 @@ theorem cmp_dist_eq_cmp_dist_coe_center (z w : ℍ) (r : ℝ) :
       ((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm]
   have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity
   have hzw₀ : 0 < 2 * z.im * w.im := by positivity
-  simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀, ←
-    (pow_left_strictMonoOn₀ two_ne_zero).cmp_map_eq dist_nonneg hr₀', dist_coe_center_sq]
+  #adaptation_note
+  /--
+  After the bug fix in https://github.com/leanprover/lean4/pull/6024,
+  we need to give Lean the hint `(y := w.im * Real.sinh r)`.
+  -/
+  simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀,
+    ← (pow_left_strictMonoOn₀ two_ne_zero).cmp_map_eq dist_nonneg (y := w.im * Real.sinh r) hr₀',
+    dist_coe_center_sq]
   rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
 
 theorem dist_eq_iff_dist_coe_center_eq :

Mathlib/Data/DFinsupp/Sigma.lean

@@ -63,14 +63,14 @@ theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] :
 
 @[simp]
 theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) :
-    sigmaCurry (f + g) = sigmaCurry f + sigmaCurry g := by
+    sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j) := by
   ext (i j)
   rfl
 
 @[simp]
 theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)]
     (r : γ) (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
-    sigmaCurry (r • f) = r • sigmaCurry f := by
+    sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j) := by
   ext (i j)
   rfl
 

Mathlib/Data/Finset/Defs.lean

@@ -213,6 +213,8 @@ instance partialOrder : PartialOrder (Finset α) where
   le_trans _ _ _ hst htu _ ha := htu <| hst ha
   le_antisymm _ _ hst hts := ext fun _ => ⟨@hst _, @hts _⟩
 
+theorem subset_of_le : s ≤ t → s ⊆ t := id
+
 instance : IsRefl (Finset α) (· ⊆ ·) :=
   show IsRefl (Finset α) (· ≤ ·) by infer_instance
 

Mathlib/Data/Finset/SDiff.lean

@@ -111,11 +111,11 @@ theorem sdiff_empty : s \ ∅ = s :=
 
 @[mono, gcongr]
 theorem sdiff_subset_sdiff (hst : s ⊆ t) (hvu : v ⊆ u) : s \ u ⊆ t \ v :=
-  sdiff_le_sdiff hst hvu
+  subset_of_le (sdiff_le_sdiff hst hvu)
 
 theorem sdiff_subset_sdiff_iff_subset {r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) :
-    r \ s ⊆ r \ t ↔ t ⊆ s :=
-  sdiff_le_sdiff_iff_le hs ht
+    r \ s ⊆ r \ t ↔ t ⊆ s := by
+  simpa only [← le_eq_subset] using sdiff_le_sdiff_iff_le hs ht
 
 @[simp, norm_cast]
 theorem coe_sdiff (s₁ s₂ : Finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : Set α) :=

Mathlib/Data/List/Sublists.lean

@@ -44,7 +44,7 @@ theorem sublists'Aux_eq_array_foldl (a : α) : ∀ (r₁ r₂ : List (List α)),
     sublists'Aux a r₁ r₂ = ((r₁.toArray).foldl (init := r₂.toArray)
       (fun r l => r.push (a :: l))).toList := by
   intro r₁ r₂
-  rw [sublists'Aux, Array.foldl_eq_foldl_toList]
+  rw [sublists'Aux, Array.foldl_toList]
   have := List.foldl_hom Array.toList (fun r l => r.push (a :: l))
     (fun r l => r ++ [a :: l]) r₁ r₂.toArray (by simp)
   simpa using this
@@ -106,7 +106,7 @@ theorem sublistsAux_eq_array_foldl :
       (r.toArray.foldl (init := #[])
         fun r l => (r.push l).push (a :: l)).toList := by
   funext a r
-  simp only [sublistsAux, Array.foldl_eq_foldl_toList, Array.mkEmpty]
+  simp only [sublistsAux, Array.foldl_toList, Array.mkEmpty]
   have := foldl_hom Array.toList (fun r l => (r.push l).push (a :: l))
     (fun (r : List (List α)) l => r ++ [l, a :: l]) r #[]
     (by simp)
@@ -127,7 +127,7 @@ theorem sublistsAux_eq_flatMap :
   ext α l : 2
   trans l.foldr sublistsAux [[]]
   · rw [sublistsAux_eq_flatMap, sublists]
-  · simp only [sublistsFast, sublistsAux_eq_array_foldl, Array.foldr_eq_foldr_toList]
+  · simp only [sublistsFast, sublistsAux_eq_array_foldl, Array.foldr_toList]
     rw [← foldr_hom Array.toList]
     · intros _ _; congr
 

Mathlib/FieldTheory/KummerExtension.lean

@@ -425,7 +425,7 @@ def adjoinRootXPowSubCEquiv (hζ : (primitiveRoots n K).Nonempty) (H : Irreducib
   AlgEquiv.ofBijective (AdjoinRoot.liftHom (X ^ n - C a) α (by simp [hα])) <| by
     haveI := Fact.mk H
     letI := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
-    refine ⟨(AlgHom.toRingHom _).injective, ?_⟩
+    refine ⟨(liftHom (X ^ n - C a) α _).injective, ?_⟩
     rw [← AlgHom.range_eq_top, ← IsSplittingField.adjoin_rootSet _ (X ^ n - C a),
       eq_comm, adjoin_rootSet_eq_range, IsSplittingField.adjoin_rootSet]
     exact IsSplittingField.splits _ _

Mathlib/FieldTheory/Relrank.lean

@@ -35,11 +35,13 @@ variable {E : Type v} [Field E] {L : Type w} [Field L]
 
 variable (A B C : Subfield E)
 
+set_option synthInstance.maxHeartbeats 400000 in
 /-- `Subfield.relrank A B` is defined to be `[B : A ⊓ B]` as a `Cardinal`, in particular,
 when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`.
 This is similar to `Subgroup.relindex` but it is `Cardinal` valued. -/
 noncomputable def relrank := Module.rank ↥(A ⊓ B) (extendScalars (inf_le_right : A ⊓ B ≤ B))
 
+set_option synthInstance.maxHeartbeats 400000 in
 /-- The `Nat` version of `Subfield.relrank`.
 If `B / A ⊓ B` is an infinite extension, then it is zero. -/
 noncomputable def relfinrank := finrank ↥(A ⊓ B) (extendScalars (inf_le_right : A ⊓ B ≤ B))
@@ -55,12 +57,14 @@ theorem relrank_eq_of_inf_eq (h : A ⊓ C = B ⊓ C) : relrank A C = relrank B C
 theorem relfinrank_eq_of_inf_eq (h : A ⊓ C = B ⊓ C) : relfinrank A C = relfinrank B C :=
   congr(toNat $(relrank_eq_of_inf_eq h))
 
+set_option synthInstance.maxHeartbeats 400000 in
 /-- If `A ≤ B`, then `Subfield.relrank A B` is `[B : A]` -/
 theorem relrank_eq_rank_of_le (h : A ≤ B) : relrank A B = Module.rank A (extendScalars h) := by
   rw [relrank]
   have := inf_of_le_left h
   congr!
 
+set_option synthInstance.maxHeartbeats 400000 in
 /-- If `A ≤ B`, then `Subfield.relfinrank A B` is `[B : A]` -/
 theorem relfinrank_eq_finrank_of_le (h : A ≤ B) : relfinrank A B = finrank A (extendScalars h) :=
   congr(toNat $(relrank_eq_rank_of_le h))
@@ -112,6 +116,7 @@ theorem relrank_top_left : relrank ⊤ A = 1 := relrank_eq_one_of_le le_top
 @[simp]
 theorem relfinrank_top_left : relfinrank ⊤ A = 1 := relfinrank_eq_one_of_le le_top
 
+set_option synthInstance.maxHeartbeats 400000 in
 @[simp]
 theorem relrank_top_right : relrank A ⊤ = Module.rank A E := by
   rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,

Mathlib/Geometry/Manifold/Instances/Real.lean

@@ -98,6 +98,7 @@ theorem interior_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
   change interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a
   rw [f.interior_preimage, interior_Ici]
   apply Function.surjective_eval
+
 @[deprecated (since := "2024-11-12")] alias interior_halfspace := interior_halfSpace
 
 open ENNReal in
@@ -108,6 +109,7 @@ theorem closure_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
   change closure (f ⁻¹' Ici a) = f ⁻¹' Ici a
   rw [f.closure_preimage, closure_Ici]
   apply Function.surjective_eval
+
 @[deprecated (since := "2024-11-12")] alias closure_halfspace := closure_halfSpace
 
 open ENNReal in
@@ -118,6 +120,7 @@ theorem closure_open_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n)
   change closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a
   rw [f.closure_preimage, closure_Ioi]
   apply Function.surjective_eval
+
 @[deprecated (since := "2024-11-12")] alias closure_open_halfspace := closure_open_halfSpace
 
 open ENNReal in

Mathlib/GroupTheory/Congruence/Basic.lean

@@ -256,7 +256,7 @@ lemma comapQuotientEquivOfSurj_symm_mk (c : Con M) {f : N →* M} (hf) (x : N) :
 MulEquiv function"]
 lemma comapQuotientEquivOfSurj_symm_mk' (c : Con M) (f : N ≃* M) (x : N) :
     ((@MulEquiv.symm (Con.Quotient (comap ⇑f _ c)) _ _ _
-      (comapQuotientEquivOfSurj c f f.surjective)) ⟦f x⟧) = ↑x :=
+      (comapQuotientEquivOfSurj c (f : N →* M) f.surjective)) ⟦f x⟧) = ↑x :=
   (MulEquiv.symm_apply_eq (@comapQuotientEquivOfSurj M N _ _ c f _)).mpr rfl
 
 /-- The **second isomorphism theorem for monoids**. -/

Mathlib/MeasureTheory/Group/Measure.lean

@@ -764,7 +764,7 @@ nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [TopologicalGrou
     [TopologicalGroup H] (e : G ≃* H) (he : Continuous e) (hesymm : Continuous e.symm) :
     IsHaarMeasure (Measure.map e μ) :=
   let f : G ≃ₜ H := .mk e
-  isHaarMeasure_map μ e he e.surjective f.isClosedEmbedding.tendsto_cocompact
+  isHaarMeasure_map μ e.toMonoidHom he e.surjective f.isClosedEmbedding.tendsto_cocompact
 
 /-- A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`. -/
 instance _root_.ContinuousLinearEquiv.isAddHaarMeasure_map

Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

@@ -507,8 +507,10 @@ def arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableS
   measurable_toFun _ h := by
     simp_rw [Equiv.arrowProdEquivProdArrow, coe_fn_mk]
     exact MeasurableSet.preimage h (Measurable.prod_mk
-        (measurable_pi_lambda (fun a c ↦ (a c).1) fun a ↦ (measurable_pi_apply a).fst)
-        (measurable_pi_lambda (fun a c ↦ (a c).2) fun a ↦ (measurable_pi_apply a).snd ))
+        (measurable_pi_lambda (fun (a : γ → α × β) c ↦ (a c).1)
+          fun a ↦ (measurable_pi_apply a).fst)
+        (measurable_pi_lambda (fun (a : γ → α × β) c ↦ (a c).2)
+          fun a ↦ (measurable_pi_apply a).snd))
   measurable_invFun _ h := by
     simp_rw [Equiv.arrowProdEquivProdArrow, coe_fn_symm_mk]
     exact MeasurableSet.preimage h (by measurability)

Mathlib/RingTheory/Jacobson.lean

@@ -704,7 +704,7 @@ lemma finite_of_finite_type_of_isJacobsonRing (R S : Type*) [CommRing R] [Field
   obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
   have : (algebraMap R S).IsIntegral := by
     rw [← f.comp_algebraMap]
-    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f hf
+    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf
   have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this
   exact Algebra.IsIntegral.finite
 

Mathlib/RingTheory/Polynomial/UniqueFactorization.lean

@@ -125,7 +125,7 @@ instance (priority := 100) uniqueFactorizationMonoid :
   exact
     ⟨w.map (rename (↑)), fun b hb =>
       let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb
-      he ▸ (prime_rename_iff ↑s).2 (h b' hb'),
+      he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'),
       Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by
       erw [Multiset.prod_hom, ← map_mul, hw]⟩
 

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ee6767b2157766c8aa451bb93d1434436e593a2",
+   "rev": "0fc755a2a762bd228db724df926de7d3e2306a34",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b4fc3aa9ae06e749417a101d5a95de2c5e8b1b6",
+   "rev": "70fef96b919e8d032bbf6016cd284867d503d2d8",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83b4115edfea21c2b9d3cc33742941ea1f9ba2e4",
+   "rev": "2ed85f320805f9d3a455ced3b181562ed146bc20",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-13
+leanprover/lean4:nightly-2024-11-14