fixes

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -267,9 +267,10 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb :
   lift b to Aˣ using hbu
   have hbab : 0 ≤ (b : A) ^ (-(1 / 2) : ℝ) * a * (b : A) ^ (-(1 / 2) : ℝ) :=
     conjugate_nonneg_of_nonneg ha rpow_nonneg
+  #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 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/Combinatorics/Additive/PluenneckeRuzsa.lean

@@ -174,14 +174,14 @@ theorem ruzsa_triangle_inequality_mul_mul_mul (A B C : Finset G) :
   rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hU
   refine cast_le.1 (?_ : (_ : ℚ≥0) ≤ _)
   push_cast
-  refine (le_div_iff₀ <| cast_pos.2 hB.card_pos).1 ?_
-  rw [mul_div_right_comm, mul_comm _ B]
+  rw [← le_div_iff₀ (cast_pos.2 hB.card_pos), mul_div_right_comm, mul_comm _ B]
   refine (Nat.cast_le.2 <| card_le_card_mul_left _ hU.1).trans ?_
   refine le_trans ?_
     (mul_le_mul (hUA _ hB') (cast_le.2 <| card_le_card <| mul_subset_mul_right hU.2)
       (zero_le _) (zero_le _))
-  rw [← mul_div_right_comm, ← mul_assoc]
-  refine (le_div_iff₀ <| cast_pos.2 hU.1.card_pos).2 ?_
+  #adaptation_note /-- 2024-11-01 `le_div_iff₀` is synthesizing wrong `GroupWithZero` without `@` -/
+  rw [← mul_div_right_comm, ← mul_assoc,
+    @le_div_iff₀ _ (_) _ _ _ _ _ _ _ (cast_pos.2 hU.1.card_pos)]
   exact mod_cast pluennecke_petridis_inequality_mul C (mul_aux hU.1 hU.2 hUA)
 
 /-- **Ruzsa's triangle inequality**. Mul-div-div version. -/

Mathlib/Data/NNReal/Defs.lean

@@ -128,7 +128,8 @@ noncomputable example : Inv ℝ≥0 := by infer_instance
 
 noncomputable example : Div ℝ≥0 := by infer_instance
 
-example : LE ℝ≥0 := by infer_instance
+-- Note(kmill): instance contains `NNReal.instCanonicallyLinearOrderedSemifield`
+noncomputable example : LE ℝ≥0 := by infer_instance
 
 example : Bot ℝ≥0 := by infer_instance
 
@@ -330,7 +331,8 @@ noncomputable def gi : GaloisInsertion Real.toNNReal (↑) :=
 -- will be noncomputable, everything else should not be.
 example : OrderBot ℝ≥0 := by infer_instance
 
-example : PartialOrder ℝ≥0 := by infer_instance
+-- Note(kmill): instance contains `NNReal.instCanonicallyLinearOrderedSemifield`
+noncomputable example : PartialOrder ℝ≥0 := by infer_instance
 
 noncomputable example : CanonicallyLinearOrderedAddCommMonoid ℝ≥0 := by infer_instance
 

Mathlib/Order/Hom/Lattice.lean

@@ -1095,7 +1095,7 @@ def subtypeVal {P : β → Prop}
     letI := Subtype.lattice Psup Pinf
     LatticeHom {x : β // P x} β :=
   letI := Subtype.lattice Psup Pinf
-  .mk (SupHom.subtypeVal Psup) (by simp)
+  .mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_inf Pinf])
 
 @[simp]
 lemma subtypeVal_apply {P : β → Prop}

Mathlib/Order/Interval/Finset/Box.lean

@@ -93,11 +93,6 @@ lemma card_box : ∀ {n}, n ≠ 0 → #(box n : Finset (ℤ × ℤ)) = 8 * n
   | 0 => by simp [Prod.ext_iff]
   | n + 1 => by
     simp [box_succ_eq_sdiff, Prod.le_def]
-    #adaptation_note /-- v4.7.0-rc1: `omega` no longer identifies atoms up to defeq.
-    (This had become a performance bottleneck.)
-    We need a tactic for normalising instances, to avoid the `have`/`simp` dance below: -/
-    have : @Nat.cast ℤ instNatCastInt n = @Nat.cast ℤ AddMonoidWithOne.toNatCast n := rfl
-    simp only [this]
     omega
 
 -- TODO: Can this be generalised to locally finite archimedean ordered rings?

Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

@@ -64,29 +64,35 @@ noncomputable def rTensor :
     MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
   TensorProduct.finsuppLeft' _ _ _ _ _
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 lemma rTensor_apply_tmul (p : MvPolynomial σ S) (n : N) :
-    rTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) :=
+    rTensor.toFun (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) :=
   TensorProduct.finsuppLeft_apply_tmul p n
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 lemma rTensor_apply_tmul_apply (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) :
-    rTensor (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n :=
+    rTensor.toFun (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n :=
   TensorProduct.finsuppLeft_apply_tmul_apply p n d
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 lemma rTensor_apply_monomial_tmul (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) :
-    rTensor (monomial e s ⊗ₜ[R] n) d = if e = d then s ⊗ₜ[R] n else 0 := by
+    rTensor.toFun (monomial e s ⊗ₜ[R] n) d = if e = d then s ⊗ₜ[R] n else 0 := by
   simp only [rTensor_apply_tmul_apply, coeff_monomial, ite_tmul]
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 lemma rTensor_apply_X_tmul (s : σ) (n : N) (d : σ →₀ ℕ) :
-    rTensor (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then (1 : S) ⊗ₜ[R] n else 0 := by
+    rTensor.toFun (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then (1 : S) ⊗ₜ[R] n else 0 := by
   rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 lemma rTensor_apply (t : MvPolynomial σ S ⊗[R] N) (d : σ →₀ ℕ) :
-    rTensor t d = ((lcoeff S d).restrictScalars R).rTensor N t :=
+    rTensor.toFun t d = ((lcoeff S d).restrictScalars R).rTensor N t :=
   TensorProduct.finsuppLeft_apply t d
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 @[simp]
 lemma rTensor_symm_apply_single (d : σ →₀ ℕ) (s : S) (n : N) :
-    rTensor.symm (Finsupp.single d (s ⊗ₜ n)) =
+    rTensor.symm.toFun (Finsupp.single d (s ⊗ₜ n)) =
       (monomial d s) ⊗ₜ[R] n :=
   TensorProduct.finsuppLeft_symm_apply_single (R := R) d s n
 
@@ -163,8 +169,9 @@ lemma rTensorAlgHom_toLinearMap :
   simp only [coeff]
   erw [finsuppLeft_apply_tmul_apply]
 
+#adaptation_note /-- 2024-11-10 added `.toFun` -/
 lemma rTensorAlgHom_apply_eq (p : MvPolynomial σ S ⊗[R] N) :
-    rTensorAlgHom (S := S) p = rTensor p := by
+    rTensorAlgHom (S := S) p = rTensor.toFun p := by
   rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
   rfl
 
@@ -178,6 +185,8 @@ noncomputable def rTensorAlgEquiv :
     rw [← LinearEquiv.symm_apply_eq]
     exact finsuppLeft_symm_apply_single (R := R) (0 : σ →₀ ℕ) (1 : S) (1 : N)
   · intro x y
+    #adaptation_note /-- 2024-11-10 added `change` -/
+    change rTensor.toFun (x * y) = _
     erw [← rTensorAlgHom_apply_eq (S := S)]
     simp only [_root_.map_mul, rTensorAlgHom_apply_eq]
     rfl