Axiomatic-AI · winstonyin-ax · May 11, 2026 · May 11, 2026 · May 11, 2026 · May 11, 2026
diff --git a/Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean b/Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean
@@ -98,7 +98,6 @@ section map
 variable {S₁ S₂ : ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact)
   (f : S₁ ⟶ S₂)
 
-set_option backward.isDefEq.respectTransparency false in
 /--
 The morphism `triangleOfSES h₁ ⟶ triangleOfSES h₂` that is induced by a morphism of short
 exact sequences of cochain complexes.

diff --git a/Mathlib/Algebra/Module/Submodule/Basic.lean b/Mathlib/Algebra/Module/Submodule/Basic.lean
@@ -131,7 +131,7 @@ theorem toAddSubgroup_strictMono : StrictMono (toAddSubgroup : Submodule R M →
 theorem toAddSubgroup_le : p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p' :=
   Iff.rfl
 
-@[gcongr, mono]
+@[mono]
 theorem toAddSubgroup_mono : Monotone (toAddSubgroup : Submodule R M → AddSubgroup M) :=
   toAddSubgroup_strictMono.monotone
 

diff --git a/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean b/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
@@ -82,11 +82,13 @@ instance restrictScalars.isScalarTower (p : Submodule R M) :
   smul_assoc r s x := Subtype.ext <| smul_assoc r s (x : M)
 
 variable {R M} in
+@[gcongr]
 lemma restrictScalars_le {s t : Submodule R M} :
     s.restrictScalars S ≤ t.restrictScalars S ↔ s ≤ t :=
   Iff.rfl
 
 variable {R M} in
+@[gcongr]
 lemma restrictScalars_lt {s t : Submodule R M} :
     s.restrictScalars S < t.restrictScalars S ↔ s < t :=
   Iff.rfl
@@ -99,7 +101,7 @@ def restrictScalarsEmbedding : Submodule R M ↪o Submodule S M where
   inj' := restrictScalars_injective S R M
   map_rel_iff' := restrictScalars_le S
 
-@[gcongr, mono]
+@[mono]
 lemma restrictScalars_monotone : Monotone (restrictScalars S : Submodule R M → Submodule S M) :=
   (restrictScalarsEmbedding S R M).monotone
 

diff --git a/Mathlib/Algebra/Order/Ring/Ordering/Basic.lean b/Mathlib/Algebra/Order/Ring/Ordering/Basic.lean
@@ -41,11 +41,11 @@ theorem toSubsemiring_le_toSubsemiring {P₁ P₂ : RingPreordering R} :
 theorem toSubsemiring_lt_toSubsemiring {P₁ P₂ : RingPreordering R} :
     P₁.toSubsemiring < P₂.toSubsemiring ↔ P₁ < P₂ := .rfl
 
-@[gcongr, mono]
+@[mono]
 theorem toSubsemiring_mono : Monotone (toSubsemiring : RingPreordering R → _) :=
   fun _ _ => id
 
-@[gcongr, mono]
+@[mono]
 theorem toSubsemiring_strictMono : StrictMono (toSubsemiring : RingPreordering R → _) :=
   fun _ _ => id
 

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean b/Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean
@@ -90,7 +90,6 @@ def Scheme.Hom.finrank {X S : Scheme.{u}} (f : X ⟶ S) (s : S) : ℕ :=
   IsAffine.finrank (pullback.snd f (S.affineOpenCover.f <| S.affineOpenCover.idx s))
     (S.affineOpenCover.covers s).choose
 
-set_option backward.isDefEq.respectTransparency false in
 private lemma Scheme.Hom.finrank_eq_finrank_snd_of_isAffine (g : T ⟶ S) [IsAffine T] (t : T)
     [Flat f] [IsFinite f] :
     f.finrank (g t) = IsAffine.finrank (pullback.snd f g) t := by

diff --git a/Mathlib/Analysis/Convex/Cone/Basic.lean b/Mathlib/Analysis/Convex/Cone/Basic.lean
@@ -104,7 +104,6 @@ lemma mem_bot : x ∈ (⊥ : ProperCone R E) ↔ x = 0 := .rfl
 
 end T1Space
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The closure of image of a proper cone under an `R`-linear map is a proper cone. We
 use continuous maps here so that the comap of f is also a map between proper cones. -/
 abbrev comap (f : E →L[R] F) (C : ProperCone R F) : ProperCone R E :=
@@ -121,14 +120,12 @@ lemma mem_comap {C : ProperCone R F} {f : E →L[R] F} : x ∈ C.comap f ↔ f x
 
 variable [ContinuousAdd F] [ContinuousConstSMul R F]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The closure of image of a proper cone under a linear map is a proper cone.
 
 We use continuous maps here to match `ProperCone.comap`. -/
 abbrev map (f : E →L[R] F) (C : ProperCone R E) : ProperCone R F :=
   ClosedSubmodule.map (f.restrictScalars R≥0) C
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma map_id (C : ProperCone R F) : C.map (.id _ _) = C := ClosedSubmodule.map_id _
 
 @[simp, norm_cast]

diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -784,7 +784,6 @@ lemma pow_mul_norm_iteratedFDeriv_fourier_le
 @[deprecated (since := "2025-11-16")]
 alias pow_mul_norm_iteratedFDeriv_fourierIntegral_le := pow_mul_norm_iteratedFDeriv_fourier_le
 
-set_option backward.isDefEq.respectTransparency false in
 lemma hasDerivAt_fourier
     {f : ℝ → E} (hf : Integrable f) (hf' : Integrable (fun x : ℝ ↦ x • f x)) (w : ℝ) :
     HasDerivAt (𝓕 f) (𝓕 (fun x : ℝ ↦ (-2 * π * I * x) • f x) w) w := by

diff --git a/Mathlib/Analysis/SpecialFunctions/Sigmoid.lean b/Mathlib/Analysis/SpecialFunctions/Sigmoid.lean
@@ -97,7 +97,7 @@ lemma sigmoid_lt_iff {a b : ℝ} : sigmoid a < sigmoid b ↔ a < b := sigmoid_st
 @[gcongr]
 lemma sigmoid_lt {a b : ℝ} : a < b → sigmoid a < sigmoid b := sigmoid_lt_iff.mpr
 
-@[gcongr, mono]
+@[mono]
 lemma sigmoid_monotone : Monotone sigmoid := sigmoid_strictMono.monotone
 
 lemma sigmoid_injective : Function.Injective sigmoid := sigmoid_strictMono.injective
@@ -237,7 +237,7 @@ lemma sigmoid_lt_iff {a b : ℝ} : sigmoid a < sigmoid b ↔ a < b := Real.sigmo
 @[gcongr]
 lemma sigmoid_lt {a b : ℝ} : a < b → sigmoid a < sigmoid b := sigmoid_lt_iff.mpr
 
-@[gcongr, mono]
+@[mono]
 lemma sigmoid_monotone : Monotone sigmoid := sigmoid_strictMono.monotone
 
 lemma sigmoid_injective : Function.Injective sigmoid := sigmoid_strictMono.injective

diff --git a/Mathlib/CategoryTheory/Triangulated/Functor.lean b/Mathlib/CategoryTheory/Triangulated/Functor.lean
@@ -310,7 +310,6 @@ variable {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
   (h : Octahedron comm h₁₂ h₂₃ h₁₃)
   (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The image of an octahedron by a triangulated functor. -/
 @[simps]
 def map : Octahedron (by dsimp; rw [← F.map_comp, comm])

diff --git a/Mathlib/Data/Finset/Density.lean b/Mathlib/Data/Finset/Density.lean
@@ -98,8 +98,8 @@ lemma dens_lt_dens (h : s ⊂ t) : dens s < dens t :=
     _ < #t := by gcongr
     _ ≤ Fintype.card α := card_le_univ t
 
-@[gcongr, mono] lemma dens_mono : Monotone (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_le_dens
-@[gcongr, mono] lemma dens_strictMono : StrictMono (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_lt_dens
+@[mono] lemma dens_mono : Monotone (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_le_dens
+@[mono] lemma dens_strictMono : StrictMono (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_lt_dens
 
 lemma dens_map_le [Fintype β] (f : α ↪ β) : dens (s.map f) ≤ dens s := by
   cases isEmpty_or_nonempty α

diff --git a/Mathlib/Geometry/Convex/Cone/Dual.lean b/Mathlib/Geometry/Convex/Cone/Dual.lean
@@ -44,7 +44,6 @@ variable {p : M →ₗ[R] N →ₗ[R] R} {s t : Set M} {y : N}
 
 local notation3 "R≥0" => {c : R // 0 ≤ c}
 
-set_option backward.isDefEq.respectTransparency false in
 variable (p) in
 /-- The dual cone of a set `s` with respect to a bilinear pairing `p` is the cone consisting of all
 points `y` such that for all points `x ∈ s` we have `0 ≤ p x y`. -/
@@ -100,7 +99,6 @@ variable (s) in
 @[simp] lemma dual_flip_dual_dual_flip (s : Set N) :
     dual p.flip (dual p (dual p.flip s)) = dual p.flip s := dual_dual_flip_dual _
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma dual_hull (s : Set M) : dual p (hull R s) = dual p s := by
   refine le_antisymm (dual_anti Submodule.subset_span) (fun x hx y hy => ?_)

diff --git a/Mathlib/Geometry/Convex/Cone/Pointed.lean b/Mathlib/Geometry/Convex/Cone/Pointed.lean
@@ -44,7 +44,6 @@ section Submodule
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E]
 variable {C : PointedCone R E}
 
-set_option backward.isDefEq.respectTransparency false in
 /-- A submodule is a pointed cone. -/
 @[coe] abbrev ofSubmodule (S : Submodule R E) : PointedCone R E := S.restrictScalars _
 
@@ -54,25 +53,20 @@ instance : Coe (Submodule R E) (PointedCone R E) := ⟨ofSubmodule⟩
 
 lemma mem_ofSubmodule_iff {S : Submodule R E} {x : E} : x ∈ (S : PointedCone R E) ↔ x ∈ S := by rfl
 
-set_option backward.isDefEq.respectTransparency false in
 lemma ofSubmodule_inj {S T : Submodule R E} : ofSubmodule S = ofSubmodule T ↔ S = T :=
   restrictScalars_inj ..
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Coercion from submodules to pointed cones as an order embedding. -/
 abbrev ofSubmoduleEmbedding : Submodule R E ↪o PointedCone R E :=
   restrictScalarsEmbedding ..
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Coercion from submodules to pointed cones as a lattice homomorphism. -/
 abbrev ofSubmoduleLatticeHom : CompleteLatticeHom (Submodule R E) (PointedCone R E) :=
   restrictScalarsLatticeHom ..
 
-set_option backward.isDefEq.respectTransparency false in
 lemma ofSubmodule_inf (S T : Submodule R E) : S ⊓ T = (S ⊓ T : PointedCone R E) :=
   restrictScalars_inf _ _ _
 
-set_option backward.isDefEq.respectTransparency false in
 lemma ofSubmodule_sup (S T : Submodule R E) : S ⊔ T = (S ⊔ T : PointedCone R E) :=
   restrictScalars_sup _ _ _
 
@@ -91,7 +85,6 @@ lemma ofSubmodule_iSup (s : Set (Submodule R E)) : ⨆ S ∈ s, S = ⨆ S ∈ s,
 variable {R E : Type*}
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup E] [Module R E]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma neg_ofSubmodule (S : Submodule R E) :  -(ofSubmodule S) = ofSubmodule (-S) :=
   neg_restrictScalars S
 
@@ -129,7 +122,6 @@ lemma convex (C : PointedCone R E) : Convex R (C : Set E) := C.toConvexCone.conv
 nonrec lemma smul_mem (C : PointedCone R E) (hr : 0 ≤ r) (hx : x ∈ C) : r • x ∈ C :=
   C.smul_mem ⟨r, hr⟩ hx
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The `PointedCone` constructed from a pointed `ConvexCone`. -/
 def _root_.ConvexCone.toPointedCone (C : ConvexCone R E) (hC : C.Pointed) : PointedCone R E where
   carrier := C
@@ -222,7 +214,6 @@ between pointed cones induced from linear maps between the ambient modules that
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The image of a pointed cone under an `R`-linear map is a pointed cone. -/
 def map (f : E →ₗ[R] F) (C : PointedCone R E) : PointedCone R F :=
   Submodule.map (f : E →ₗ[R≥0] F) C
@@ -248,7 +239,6 @@ theorem map_map (g : F →ₗ[R] G) (f : E →ₗ[R] F) (C : PointedCone R E) :
 theorem map_id (C : PointedCone R E) : C.map LinearMap.id = C :=
   SetLike.coe_injective <| Set.image_id _
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The preimage of a pointed cone under an `R`-linear map is a pointed cone. -/
 def comap (f : E →ₗ[R] F) (C : PointedCone R F) : PointedCone R E :=
   Submodule.comap (f : E →ₗ[R≥0] F) C

diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
@@ -3,6 +3,7 @@ module  -- shake: keep-all, shake: keep-downstream
 public import Lean.Linter.Sets -- for the definition of linter sets
 public import Lean.LibrarySuggestions.Default -- for `+suggestions` modes in tactics
 public import Mathlib.Lean.Linter -- linter utilities; will be transitively imported in #31134
+public import Mathlib.Tactic.AdaptationNote -- make #adaptation_note available everywhere
 public import Mathlib.Tactic.Lemma
 public import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
 public import Mathlib.Tactic.Linter.DirectoryDependency

diff --git a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
@@ -138,6 +138,12 @@ theorem LinearMap.lTensor_range :
   apply lTensor_surjective
   rw [← range_eq_top, range_rangeRestrict]
 
+/-- If `g` is surjective, then `g.baseChange A` is surjective. -/
+theorem LinearMap.baseChange_surjective (A : Type*) [Semiring A] [Algebra R A]
+    (hg : Function.Surjective g) : Function.Surjective (g.baseChange A) := by
+  rw [LinearMap.baseChange_eq_ltensor]
+  exact lTensor_surjective _ hg
+
 /-- If `g` is surjective, then `rTensor Q g` is surjective -/
 theorem LinearMap.rTensor_surjective (hg : Function.Surjective g) :
     Function.Surjective (rTensor Q g) := by

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@@ -468,6 +468,20 @@ theorem distribBaseChange_symm_tmul
   rw [tmul_eq_smul_one_tmul b, ← smul_tmul, smul_tmul', mul_comm]
   simp
 
+lemma cancelBaseChange_self_eq_lid :
+    cancelBaseChange R A A A N = TensorProduct.lid A (A ⊗[R] N) := by
+  ext x
+  induction x using TensorProduct.induction_on with
+  | zero => simp only [map_zero]
+  | tmul b y =>
+    induction y using TensorProduct.induction_on with
+    | zero => simp
+    | tmul a m =>
+      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
+    | add x y hx hy =>
+      simp only [tmul_add, map_add, lid_tmul, hx, hy]
+  | add x y hx hy => simp [hx, hy]
+
 end cancelBaseChange
 
 section leftComm
@@ -866,3 +880,21 @@ lemma toBaseChange_surjective' {y : A ⊗[R] M} (hy : y ∈ p.baseChange A) :
   exact ⟨x, congr($hx)⟩
 
 end Submodule
+
+namespace TensorProduct.AlgebraTensorModule
+
+variable {R A M N : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
+variable [AddCommGroup M] [Module R M] [AddCommGroup N] [Module A N]
+
+lemma baseChange_comp_cancelBaseChange_symm_self (f : (A ⊗[R] M) →ₗ[A] N) :
+    f.baseChange A ∘ₗ (cancelBaseChange R A A A M).symm = (TensorProduct.lid A N).symm ∘ₗ f := by
+  rw [cancelBaseChange_self_eq_lid]
+  ext x
+  simp
+
+lemma ker_baseChange_comp_cancelBaseChange_symm (f : (A ⊗[R] M) →ₗ[A] N) :
+    (f.baseChange A ∘ₗ (cancelBaseChange R A A A M).symm).ker = f.ker := by
+  rw [baseChange_comp_cancelBaseChange_symm_self, LinearMap.ker_comp,
+    LinearEquiv.ker, Submodule.comap_bot]
+
+end TensorProduct.AlgebraTensorModule
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
@@ -5,11 +5,10 @@ Authors: Jeremy Avigad, Leonardo de Moura
 -/
 module
 
-public import Mathlib.Tactic.AdaptationNote
 public import Batteries.Logic
 public import Batteries.Util.LibraryNote
 
-import Mathlib.Tactic.Attr.Register
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # Basic logic properties

diff --git a/Mathlib/RingTheory/Finiteness/Basic.lean b/Mathlib/RingTheory/Finiteness/Basic.lean
@@ -510,7 +510,6 @@ variable {R E : Type*} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommMonoid
 
 local notation3 "R≥0" => {c : R // 0 ≤ c}
 
-set_option backward.isDefEq.respectTransparency false in
 private instance instModuleFiniteAux : Module.Finite R≥0 R := by
   simp_rw [Module.finite_def, Submodule.fg_def, Submodule.eq_top_iff']
   refine ⟨{1, -1}, by simp, fun x ↦ ?_⟩
@@ -520,7 +519,6 @@ private instance instModuleFiniteAux : Module.Finite R≥0 R := by
   · simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨-x, neg_nonneg.mpr hx⟩ (x := -1)
       (Submodule.subset_span <| by simp)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If a module is finite over a linearly ordered ring, then it is also finite over the non-negative
 scalars. -/
 instance instModuleFinite [Module.Finite R E] : Module.Finite R≥0 E := .trans R E