Sync upstream mathlib4 (2026-08-04, +16 commits)

Counterexamples.lean

@@ -10,6 +10,7 @@ public import Counterexamples.DirectSumIsInternal
 public import Counterexamples.DiscreteTopologyNonDiscreteUniformity
 public import Counterexamples.EulerSumOfPowers
 public import Counterexamples.Girard
+public import Counterexamples.GrothendieckPower
 public import Counterexamples.HeawoodUnitDistance
 public import Counterexamples.HomogeneousPrimeNotPrime
 public import Counterexamples.InvertibleModuleNotIdeal

Mathlib/Algebra/BigOperators/Associated.lean

@@ -73,7 +73,7 @@ theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι)
 theorem exists_associated_mem_of_dvd_prod [CommMonoidWithZero M₀] [IsCancelMulZero M₀]
     {p : M₀} (hp : Prime p)
     {s : Multiset M₀} : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
-  Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_unit]) fun a s ih hs hps => by
+  Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_isUnit]) fun a s ih hs hps => by
     rw [Multiset.prod_cons] at hps
     rcases hp.dvd_or_dvd hps with h | h
     · have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -256,8 +256,8 @@ theorem finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1)
   split_ifs
   exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]
 
-theorem finprod_nonneg {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R]
-    {f : α → R} (hf : ∀ x, 0 ≤ f x) :
+theorem finprod_nonneg {R : Type*} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R]
+    [PosMulMono R] {f : α → R} (hf : ∀ x, 0 ≤ f x) :
     0 ≤ ∏ᶠ x, f x :=
   finprod_induction (fun x => 0 ≤ x) zero_le_one (fun _ _ => mul_nonneg) hf
 

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -287,7 +287,7 @@ variable {X Y : ModuleCat R}
 
 /-- Build a `LinearEquiv` from an isomorphism in the category `ModuleCat R`. -/
 def toLinearEquiv (i : X ≅ Y) : X ≃ₗ[R] Y :=
-  .ofLinear i.hom.hom i.inv.hom (by aesop) (by aesop)
+  .ofLinearMap i.hom.hom i.inv.hom (by aesop) (by aesop)
 
 @[simp] lemma toLinearEquiv_apply (i : X ≅ Y) (x : X) : i.toLinearEquiv x = i.hom x := rfl
 @[simp] lemma toLinearEquiv_symm (i : X ≅ Y) : i.toLinearEquiv.symm = i.symm.toLinearEquiv := rfl

Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -263,7 +263,7 @@ namespace CategoryTheory.Iso
 
 /-- Build a `LinearEquiv` from an isomorphism in the category `SemimoduleCat R`. -/
 def toLinearEquivₛ {X Y : SemimoduleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y :=
-  LinearEquiv.ofLinear i.hom.hom i.inv.hom (by aesop) (by aesop)
+  LinearEquiv.ofLinearMap i.hom.hom i.inv.hom (by aesop) (by aesop)
 
 end CategoryTheory.Iso
 

Mathlib/Algebra/Colimit/Module.lean

@@ -211,7 +211,7 @@ family of equivalences `eᵢ : Gᵢ ≅ G'ᵢ` such that `e ∘ f = f' ∘ e` in
 -/
 def congr (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ i j h, e j ∘ₗ f i j h = f' i j h ∘ₗ e i) :
     DirectLimit G f ≃ₗ[R] DirectLimit G' f' :=
-  LinearEquiv.ofLinear (map (e ·) he)
+  LinearEquiv.ofLinearMap (map (e ·) he)
     (map (fun i ↦ (e i).symm) fun i j h ↦ by
       rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
         refl_toLinearMap, comp_id])
@@ -242,7 +242,7 @@ open _root_.DirectLimit
 /-- The direct limit constructed as a quotient of the direct sum is isomorphic to
 the direct limit constructed as a quotient of the disjoint union. -/
 def linearEquiv : DirectLimit G f ≃ₗ[R] _root_.DirectLimit G f :=
-  .ofLinear
+  .ofLinearMap
     (lift _ _ _ _ (Module.of _ _ _ _) fun _ _ _ _ ↦ .symm <| eq_of_le ..)
     (Module.lift _ _ _ _ (of _ _ _ _) fun _ _ _ _ ↦ of_f ..)
     (by ext; simp)

Mathlib/Algebra/GroupWithZero/Associated.lean

@@ -234,7 +234,7 @@ protected theorem Associated.prime [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ
     Prime q :=
   ⟨h.ne_zero_iff.1 hp.ne_zero,
     let ⟨u, hu⟩ := h
-    ⟨fun ⟨v, hv⟩ => hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩, by
+    ⟨fun ⟨v, hv⟩ => hp.not_isUnit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩, by
       rw [← hu]
       simp only [Units.isUnit, IsUnit.mul_right_dvd]
       intro a b

Mathlib/Algebra/IsPrimePow.lean

@@ -43,11 +43,14 @@ theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R) := by
   rw [eq_zero_of_pow_eq_zero hx]
   simp
 
-theorem IsPrimePow.not_unit {n : R} (h : IsPrimePow n) : ¬IsUnit n :=
+theorem IsPrimePow.not_isUnit {n : R} (h : IsPrimePow n) : ¬IsUnit n :=
   let ⟨_p, _k, hp, hk, hn⟩ := h
-  hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_unit
+  hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_isUnit
 
-theorem IsUnit.not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_unit h
+@[deprecated (since := "2026-08-02")]
+alias IsPrimePow.not_unit := IsPrimePow.not_isUnit
+
+theorem IsUnit.not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_isUnit h
 
 theorem not_isPrimePow_one : ¬IsPrimePow (1 : R) :=
   isUnit_one.not_isPrimePow

Mathlib/Algebra/Module/CharacterModule.lean

@@ -108,7 +108,7 @@ lemma dual_surjective_of_injective (f : A →ₗ[R] B) (hf : Function.Injective
 Two isomorphic modules have isomorphic character modules.
 -/
 def congr (e : A ≃ₗ[R] B) : CharacterModule A ≃ₗ[R] CharacterModule B :=
-  .ofLinear (dual e.symm) (dual e)
+  .ofLinearMap (dual e.symm) (dual e)
     (by ext c _; exact congr(c $(e.right_inv _)))
     (by ext c _; exact congr(c $(e.left_inv _)))
 
@@ -144,7 +144,7 @@ Linear maps into a character module are exactly characters of the tensor product
 -/
 @[simps!] noncomputable def homEquiv :
     (A →ₗ[R] CharacterModule B) ≃ₗ[R] CharacterModule (A ⊗[R] B) :=
-  .ofLinear uncurry curry (by ext _ z; refine z.induction_on ?_ ?_ ?_ <;> aesop) (by aesop)
+  .ofLinearMap uncurry curry (by ext _ z; refine z.induction_on ?_ ?_ ?_ <;> aesop) (by aesop)
 
 theorem dual_rTensor_conj_homEquiv (f : A →ₗ[R] A') :
     homEquiv.symm.toLinearMap ∘ₗ dual (f.rTensor B) ∘ₗ homEquiv.toLinearMap = f.lcomp R _ := rfl

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -481,25 +481,40 @@ variable (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M)
 
 
 /-- If a linear map has an inverse, it is a linear equivalence. -/
-def ofLinear (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂ :=
-  { f with
-    invFun := g
-    left_inv := LinearMap.ext_iff.1 h₂
-    right_inv := LinearMap.ext_iff.1 h₁ }
+def ofLinearMap (h₁ : f.comp g = .id) (h₂ : g.comp f = .id) : M ≃ₛₗ[σ₁₂] M₂ where
+  __ := f
+  invFun := g
+  left_inv := LinearMap.ext_iff.1 h₂
+  right_inv := LinearMap.ext_iff.1 h₁
 
-@[simp]
+@[simp low]
+theorem coe_ofLinearMap (h₁ h₂) : ⇑(ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl
+
+@[simp low]
+theorem symm_ofLinearMap (h₁ h₂) :
+    (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = (ofLinearMap g f h₂ h₁) :=
+  rfl
+
+/-- If a linear map has an inverse, it is a linear equivalence. -/
+@[deprecated ofLinearMap (since := "2026-06-23")]
+abbrev ofLinear (h₁ : f.comp g = .id) (h₂ : g.comp f = .id) : M ≃ₛₗ[σ₁₂] M₂ := ofLinearMap f g h₁ h₂
+
+@[deprecated coe_ofLinearMap (since := "2026-06-23")]
 theorem ofLinear_apply {h₁ h₂} (x : M) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) x = f x :=
   rfl
 
-@[simp]
-theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x :=
+@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `coe_ofLinearMap`"
+  (since := "2026-06-23")]
+theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) :
+    (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x :=
   rfl
 
-@[simp]
-theorem ofLinear_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl
+@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `ofLinear_toLinearMap`"
+  (since := "2026-06-23")]
+theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl
 
 @[simp]
-theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl
+theorem ofLinear_toLinearMap (h₁ h₂) : (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl
 
 end
 
@@ -833,7 +848,7 @@ open LinearMap
 /-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types,
 construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)` -/
 def funCongrLeft (e : m ≃ n) : (n → M) ≃ₗ[R] m → M :=
-  LinearEquiv.ofLinear (funLeft R M e) (funLeft R M e.symm)
+  LinearEquiv.ofLinearMap (funLeft R M e) (funLeft R M e.symm)
     (LinearMap.ext fun x ↦
       funext fun i ↦ by rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id])
     (LinearMap.ext fun x ↦

Mathlib/Algebra/Module/Presentation/Basic.lean

@@ -364,7 +364,7 @@ variable {solution' : relations.Solution N} (h' : solution'.IsPresentation)
 
 /-- Uniqueness (up to a unique linear equivalence) of the module defined
 by generators and relations. -/
-def uniq : M ≃ₗ[A] N := LinearEquiv.ofLinear
+def uniq : M ≃ₗ[A] N := LinearEquiv.ofLinearMap
   (h.desc solution') (h'.desc solution)
     (h'.postcomp_injective (by simp))
     (h.postcomp_injective (by simp))
@@ -459,7 +459,7 @@ lemma isPresentation {solution : relations.Solution M}
     solution.IsPresentation where
   bijective := by
     let e : relations.Quotient ≃ₗ[A] M :=
-      LinearEquiv.ofLinear solution.fromQuotient
+      LinearEquiv.ofLinearMap solution.fromQuotient
       ((down.{v} h).desc (ofQuotient relations))
       ((down.{max u w₀} h).postcomp_injective (by aesop)) (by aesop)
     exact e.bijective

Mathlib/Algebra/Prime/Defs.lean

@@ -51,11 +51,14 @@ include hp
 theorem ne_zero : p ≠ 0 :=
   hp.1
 
-theorem not_unit : ¬IsUnit p :=
+theorem not_isUnit : ¬IsUnit p :=
   hp.2.1
 
+@[deprecated (since := "2026-08-02")]
+alias not_unit := not_isUnit
+
 theorem not_dvd_one : ¬p ∣ 1 :=
-  mt (isUnit_of_dvd_one ·) hp.not_unit
+  mt (isUnit_of_dvd_one ·) hp.not_isUnit
 
 theorem ne_one : p ≠ 1 := fun h => hp.2.1 (h.symm ▸ isUnit_one)
 
@@ -76,7 +79,7 @@ theorem dvd_of_dvd_pow {a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a := by
   | zero =>
     rw [pow_zero] at h
     have := isUnit_of_dvd_one h
-    have := not_unit hp
+    have := not_isUnit hp
     contradiction
   | succ n ih =>
     rw [pow_succ'] at h
@@ -93,7 +96,7 @@ end Prime
 theorem not_prime_zero : ¬Prime (0 : M) := fun h => h.ne_zero rfl
 
 @[simp]
-theorem not_prime_one : ¬Prime (1 : M) := fun h => h.not_unit isUnit_one
+theorem not_prime_one : ¬Prime (1 : M) := fun h => h.not_isUnit isUnit_one
 
 end Prime
 
@@ -147,7 +150,7 @@ section CancelCommMonoidWithZero
 variable [CommMonoidWithZero M] [IsCancelMulZero M] {p : M}
 
 protected theorem Prime.irreducible (hp : Prime p) : Irreducible p :=
-  ⟨hp.not_unit, fun a b ↦ by
+  ⟨hp.not_isUnit, fun a b ↦ by
     rintro rfl
     exact (hp.dvd_or_dvd dvd_rfl).symm.imp
       (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

@@ -71,6 +71,10 @@ theorem omega_mul_omega_eq_add :
     (ω : QuadraticAlgebra R a b) * ω = a • 1 + b • ω := by
   ext <;> simp
 
+theorem omega_mul_omega_eq_algebraMap :
+    (ω : QuadraticAlgebra R a b) * ω = algebraMap R _ a + algebraMap R _ b * ω := by
+  simp [omega_mul_omega_eq_add, Algebra.algebraMap_eq_smul_one]
+
 @[simp]
 theorem omega_mul_mk (x y : R) : (ω : QuadraticAlgebra R a b) * ⟨x, y⟩ = ⟨a * y, x + b * y⟩ := by
   ext <;> simp

Mathlib/Algebra/Squarefree/Basic.lean

@@ -185,7 +185,7 @@ theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {k : ℕ}
     p ^ k ∣ y := by
   by_cases hxp : p ∣ x
   · obtain ⟨x', rfl⟩ := hxp
-    have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_unit <| hx p (mul_dvd_mul_left p contra)
+    have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_isUnit <| hx p (mul_dvd_mul_left p contra)
     replace h : p ^ k ∣ x' * y := by
       rw [pow_succ', mul_assoc] at h
       exact (mul_dvd_mul_iff_left hp.ne_zero).mp h

Mathlib/Algebra/Star/Module.lean

@@ -221,7 +221,7 @@ set_option backward.isDefEq.respectTransparency false in
 as a linear equivalence. -/
 @[simps!]
 def StarModule.decomposeProdAdjoint : A ≃ₗ[R] selfAdjoint A × skewAdjoint A := by
-  refine LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R))
+  refine LinearEquiv.ofLinearMap ((selfAdjointPart R).prod (skewAdjointPart R))
     (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype)
     ?_ (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R)
   -- Note: with https://github.com/leanprover-community/mathlib4/pull/6965 `Submodule.coe_subtype` doesn't fire in `dsimp` or `simp`

Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

@@ -476,9 +476,6 @@ set_option backward.isDefEq.respectTransparency.types false in
 set_option backward.defeqAttrib.useBackward true in
 /-- Restriction along the composition is isomorphic to the composition of restrictions. -/
 def restrictFunctorComp : restrictFunctor (f ≫ g) ≅ restrictFunctor g ⋙ restrictFunctor f :=
-  have : (f.opensFunctor ⋙ g.opensFunctor).IsContinuous
-      (Opens.grothendieckTopology X) (Opens.grothendieckTopology Z) :=
-    Functor.isContinuous_comp _ _ _ (Opens.grothendieckTopology _) _
   SheafOfModules.pushforwardNatIso _ (NatIso.ofComponents fun _ ↦ eqToIso (by simp)) ≪≫
     SheafOfModules.pushforwardCongr (by ext : 3; simp [← Functor.map_comp, SheafedSpace.sheaf]) ≪≫
     (SheafOfModules.pushforwardComp _ _).symm

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -263,8 +263,8 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi
   /- First rewrite things in a simplified form, without any real change. -/
   suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
     rw [fourierIntegral_continuousLinearMap_apply' hf']
-    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
-      neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
+    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
+      fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
       smul_neg, ← smul_smul, coe_smul, neg_neg]
   -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
   have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -962,7 +962,7 @@ theorem coe_ofSurjective (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Sur
 def ofLinearIsometry (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E)
     (h₁ : f.toLinearMap.comp g = LinearMap.id) (h₂ : g.comp f.toLinearMap = LinearMap.id) :
     E ≃ₛₗᵢ[σ₁₂] E₂ :=
-  { toLinearEquiv := LinearEquiv.ofLinear f.toLinearMap g h₁ h₂
+  { toLinearEquiv := LinearEquiv.ofLinearMap f.toLinearMap g h₁ h₂
     norm_map' := fun x => f.norm_map x }
 
 @[simp]

Mathlib/CategoryTheory/Limits/Types/Products.lean

@@ -229,7 +229,6 @@ noncomputable def productLimitCone :
       π := Discrete.natTrans (fun ⟨j⟩ =>
         ↾fun f => (equivShrink (∀ j, F j)).symm f j) }
   isLimit :=
-    have : Small.{u} (∀ j, F j) := inferInstance
     { lift := fun s => ↾fun x => (equivShrink _) (fun j => s.π.app ⟨j⟩ x)
       uniq := fun s m w => ConcreteCategory.hom_ext _ _ fun x => Shrink.ext (funext fun j => by
         simpa using! ConcreteCategory.congr_hom (w ⟨j⟩) x) }

Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean

@@ -45,9 +45,6 @@ def PreZeroHypercover.isLimitSigmaOfIsColimitEquiv (E : PreZeroHypercover.{w} S)
     [PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F] :
     IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
       IsLimit (E.toPreOneHypercover.multifork F) := by
-  have : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f) :=
-    inferInstanceAs <| HasPullback
-      ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
   let c' : Cofan E.toPreOneHypercover.Y' :=
     Cofan.mk
       ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := ⟨⟩) (i₂ := ⟨⟩) ⟨⟩)

Mathlib/CategoryTheory/Sites/LeftExact.lean

@@ -135,7 +135,6 @@ def liftToPlusObjLimitObj {K : Type s} [SmallCategory K] [FinCategory K]
     [ReflectsLimitsOfShape K (forget D)] (F : K ⥤ Cᵒᵖ ⥤ D) (X : C)
     (S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))) :
     S.pt ⟶ (J.plusObj (limit F)).obj (op X) :=
-  let x := (J.Cover X)ᵒᵖ
   let F' := F ⋙ J.diagramFunctor D X
   let e := colimitLimitIso (F ⋙ J.diagramFunctor D X)
   let t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) :=

Mathlib/Data/Fin/VecNotation.lean

@@ -197,7 +197,6 @@ dsimproc cons_val (Matrix.vecCons _ _ _) := fun e => do
     if let Expr.lit (.natVal length) := etailn_whnf then
       pure (length, false, q(OfNat.ofNat $etailn_whnf))
     else if let some ((base : Q(ℕ)), offset) ← (Meta.isOffset? etailn_whnf).run then
-      let offset_e : Q(ℕ) := mkNatLit offset
       pure (offset, true, q($base + $offset))
     else
       pure (0, true, etailn)

Mathlib/Data/Nat/Multiplicity.lean

@@ -79,7 +79,7 @@ theorem emultiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n)
 namespace Prime
 
 theorem emultiplicity_one {p : ℕ} (hp : p.Prime) : emultiplicity p 1 = 0 :=
-  emultiplicity_of_one_right hp.prime.not_unit
+  emultiplicity_of_one_right hp.prime.not_isUnit
 
 theorem emultiplicity_mul {p m n : ℕ} (hp : p.Prime) :
     emultiplicity p (m * n) = emultiplicity p m + emultiplicity p n :=
@@ -93,7 +93,7 @@ theorem emultiplicity_self {p : ℕ} (hp : p.Prime) : emultiplicity p p = 1 :=
   (Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, hp.pos⟩).emultiplicity_self
 
 theorem emultiplicity_pow_self {p n : ℕ} (hp : p.Prime) : emultiplicity p (p ^ n) = n :=
-  _root_.emultiplicity_pow_self hp.ne_zero hp.prime.not_unit n
+  _root_.emultiplicity_pow_self hp.ne_zero hp.prime.not_isUnit n
 
 /-- **Legendre's Theorem**
 

Mathlib/LinearAlgebra/Contraction.lean

@@ -168,7 +168,7 @@ attribute [-ext] AlgebraTensorModule.curry_injective in
 provides this equivalence in return for a basis of `M`. -/
 -- We manually create simp-lemmas because `@[simps]` generates a malformed lemma
 noncomputable def dualTensorHomEquivOfBasis : Module.Dual R M ⊗[R] N ≃ₗ[R] M →ₗ[R] N :=
-  LinearEquiv.ofLinear (dualTensorHom R M N)
+  LinearEquiv.ofLinearMap (dualTensorHom R M N)
     (∑ i, TensorProduct.mk R _ N (b.dualBasis i) ∘ₗ (LinearMap.applyₗ (R := R) (b i)))
     (by
       ext f m
@@ -446,7 +446,7 @@ isomorphism `R ⊗ R ≃ R`.
 @[simps!]
 noncomputable def dualDistribEquivOfBasis (b : Basis ι R M) (c : Basis κ R N) :
     Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N) := by
-  refine LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_
+  refine LinearEquiv.ofLinearMap (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_
   · exact dualDistrib_dualDistribInvOfBasis_left_inverse _ _
   · exact dualDistrib_dualDistribInvOfBasis_right_inverse _ _
 

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

@@ -49,7 +49,7 @@ variable [Module S M₁'] [IsScalarTower R S M₁']
 "tensor product distributes over direct sum". -/
 protected def directSum :
     ((⨁ i₁, M₁ i₁) ⊗[R] ⨁ i₂, M₂ i₂) ≃ₗ[S] ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2 := by
-  refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right
+  refine LinearEquiv.ofLinearMap ?toFun ?invFun ?left ?right
   · exact AlgebraTensorModule.lift <|
       toModule S _ _ fun i₁ => flip <| toModule R _ _ fun i₂ => flip <| AlgebraTensorModule.curry <|
       DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)

Mathlib/LinearAlgebra/Dual/Lemmas.lean

@@ -620,7 +620,7 @@ vanish on `W`.
 The inverse of this is `Submodule.dualCopairing`. -/
 def dualQuotEquivDualAnnihilator (W : Submodule R M) :
     Module.Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator :=
-  LinearEquiv.ofLinear
+  LinearEquiv.ofLinearMap
     (W.mkQ.dualMap.codRestrict W.dualAnnihilator fun φ =>
       W.range_dualMap_mkQ_eq ▸ LinearMap.mem_range_self W.mkQ.dualMap φ)
     W.dualCopairing (by ext; rfl) (by ext; rfl)