Merge remote-tracking branch 'upstream/master' into bump/v4.27.0

mathlib4-bot · mathlib4-bot · commit 461e6eaf7513 · 2025-12-09T11:38:25.000Z
diff --git a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@@ -576,11 +576,7 @@ noncomputable def rightHomologyData [HasZeroObject C] (s : S.Splitting) :
     (fun x hx => by simp only [s.g_s_assoc, sub_comp, id_comp, sub_eq_self, assoc, hx, comp_zero])
     (fun x _ b hb => by simp only [← hb, s.s_g_assoc])
   let g' := hp.desc (CokernelCofork.ofπ S.g S.zero)
-  have hg' : g' = 𝟙 _ := by
-    apply Cofork.IsColimit.hom_ext hp
-    dsimp
-    erw [Cofork.IsColimit.π_desc hp]
-    simp only [Cofork.π_ofπ, comp_id]
+  have hg' : g' = 𝟙 _ := by simp [g']
   have wι : (0 : 0 ⟶ S.X₃) ≫ g' = 0 := zero_comp
   have hι : IsLimit (KernelFork.ofι 0 wι) := KernelFork.IsLimit.ofMonoOfIsZero _
       (by rw [hg']; dsimp; infer_instance) (isZero_zero _)
diff --git a/Mathlib/Algebra/Polynomial/AlgebraMap.lean b/Mathlib/Algebra/Polynomial/AlgebraMap.lean
@@ -476,12 +476,12 @@ theorem map_aeval_eq_aeval_map {S T U : Type*} [Semiring S] [CommSemiring T] [Se
     [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U}
     (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : R[X]) (a : S) :
     ψ (aeval a p) = aeval (ψ a) (p.map φ) := by
-  conv_rhs => rw [aeval_def, ← eval_map]
+  conv_rhs => rw [← eval_map_algebraMap]
   rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
 
 theorem aeval_eq_zero_of_dvd_aeval_eq_zero [CommSemiring S] [CommSemiring T] [Algebra S T]
     {p q : S[X]} (h₁ : p ∣ q) {a : T} (h₂ : aeval a p = 0) : aeval a q = 0 := by
-  rw [aeval_def, ← eval_map] at h₂ ⊢
+  rw [← eval_map_algebraMap] at h₂ ⊢
   exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂
 
 section Semiring
diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean
@@ -453,7 +453,7 @@ theorem ι_glueMorphisms (𝒰 : OpenCover.{v} X) {Y : Scheme} (f : ∀ x, 𝒰.
     PreZeroHypercover.pullback₁_X, ulift_X, ulift_f, PreZeroHypercover.pullback₁_f]
   simp_rw [pullback.condition_assoc, ← ulift_f, ← ι_fromGlued, Category.assoc, glueMorphisms,
     IsIso.hom_inv_id_assoc, ulift_f, hf]
-  erw [Multicoequalizer.π_desc]
+  simp [CategoryTheory.GlueData.ι]
 
 end Cover
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
@@ -78,10 +78,8 @@ def N₁Γ₀ : Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ) :=
 theorem N₁Γ₀_app (K : ChainComplex C ℕ) :
     N₁Γ₀.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
       (toKaroubi _).mapIso (Γ₀NondegComplexIso K) := by
-  ext1
-  dsimp [N₁Γ₀]
-  erw [id_comp, comp_id, comp_id]
-  rfl
+  ext
+  simp [N₁Γ₀, Γ₀'CompNondegComplexFunctor]
 
 theorem N₁Γ₀_hom_app (K : ChainComplex C ℕ) :
     N₁Γ₀.hom.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫
diff --git a/Mathlib/Analysis/Complex/Polynomial/UnitTrinomial.lean b/Mathlib/Analysis/Complex/Polynomial/UnitTrinomial.lean
@@ -37,7 +37,7 @@ theorem irreducible_of_coprime' (hp : IsUnitTrinomial p)
   rw [natDegree_pos_iff_degree_pos] at hq''
   rw [← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int] at hq''
   obtain ⟨z, hz⟩ := Complex.exists_root hq''
-  rw [IsRoot, eval_map, ← aeval_def] at hz
+  rw [IsRoot, eval_map_algebraMap] at hz
   refine h z ⟨?_, ?_⟩
   · obtain ⟨g', hg'⟩ := hq
     rw [hg', aeval_mul, hz, zero_mul]
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
@@ -486,7 +486,7 @@ theorem adjoin_minpoly_coeff_of_exists_primitive_element
     apply minpoly.dvd
     rw [aeval_def, eval₂_eq_eval_map]
     erw [g.map_toSubring K'.toSubring]
-    rw [eval_map, ← aeval_def]
+    rw [eval_map_algebraMap]
     exact minpoly.aeval K α
   have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) := by
     intro K
diff --git a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
@@ -91,7 +91,7 @@ theorem isIntegrallyClosed_dvd_iff {s : S} (hs : IsIntegral R s) (p : R[X]) :
     Polynomial.aeval s p = 0 ↔ minpoly R s ∣ p :=
   ⟨fun hp => isIntegrallyClosed_dvd hs hp, fun hp => by
     simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom,
-      Function.comp_apply, eval_map, ← aeval_def] using
+      Function.comp_apply, eval_map_algebraMap] using
       aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)⟩
 
 theorem ker_eval {s : S} (hs : IsIntegral R s) :
diff --git a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
@@ -35,7 +35,7 @@ noncomputable def minpolyDiv : S[X] := (minpoly R x).map (algebraMap R S) /ₘ (
 lemma minpolyDiv_spec :
     minpolyDiv R x * (X - C x) = (minpoly R x).map (algebraMap R S) := by
   delta minpolyDiv
-  rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map, ← aeval_def, minpoly.aeval]
+  rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map_algebraMap, minpoly.aeval]
 
 lemma coeff_minpolyDiv (i) : coeff (minpolyDiv R x) i =
     algebraMap R S (coeff (minpoly R x) (i + 1)) + coeff (minpolyDiv R x) (i + 1) * x := by
@@ -48,11 +48,11 @@ lemma minpolyDiv_eq_zero (hx : ¬IsIntegral R x) : minpolyDiv R x = 0 := by
   rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]
 
 lemma eval_minpolyDiv_self : (minpolyDiv R x).eval x = aeval x (derivative <| minpoly R x) := by
-  rw [aeval_def, ← eval_map, ← derivative_map, ← minpolyDiv_spec R x]; simp
+  rw [← eval_map_algebraMap, ← derivative_map, ← minpolyDiv_spec R x]; simp
 
 lemma minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero [IsDomain S]
     {y} (hxy : y ≠ x) (hy : aeval y (minpoly R x) = 0) : (minpolyDiv R x).eval y = 0 := by
-  rw [aeval_def, ← eval_map, ← minpolyDiv_spec R x] at hy
+  rw [← eval_map_algebraMap, ← minpolyDiv_spec R x] at hy
   simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy
   exact hy.resolve_right (by rwa [sub_eq_zero])
 
@@ -72,7 +72,7 @@ lemma eval₂_minpolyDiv_self {T} [CommRing T] [Algebra R T] [IsDomain T] [Decid
       if σ₁ x = σ₂ x then σ₁ (aeval x (derivative <| minpoly R x)) else 0 := by
   apply eval₂_minpolyDiv_of_eval₂_eq_zero
   rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
-    eval_map, ← aeval_def, minpoly.aeval, map_zero]
+    eval_map_algebraMap, minpoly.aeval, map_zero]
 
 lemma eval_minpolyDiv_of_aeval_eq_zero [IsDomain S] [DecidableEq S]
     {y} (hy : aeval y (minpoly R x) = 0) :
diff --git a/Mathlib/FieldTheory/Normal/Basic.lean b/Mathlib/FieldTheory/Normal/Basic.lean
@@ -48,7 +48,7 @@ theorem Normal.exists_isSplittingField [h : Normal F K] [FiniteDimensional F K]
               mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
                 Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)
   · exact minpoly.ne_zero (h.isIntegral (s x))
-  rw [IsRoot.def, eval_map, ← aeval_def, map_prod]
+  rw [IsRoot.def, eval_map_algebraMap, map_prod]
   exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)
 
 section NormalTower
diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean
@@ -306,7 +306,7 @@ theorem splits_in_splittingField_of_comp (hq : q.natDegree ≠ 0) :
       Splits.exists_eval_eq_zero (SplittingField.splits (r.comp q)) fun h =>
         hr' ((mul_eq_zero.mp (natDegree_comp.symm.trans (natDegree_eq_of_degree_eq_some
           (by rwa [degree_map] at h)))).resolve_right hq)
-    rw [eval_map, ← aeval_def, aeval_comp] at hx
+    rw [eval_map_algebraMap, aeval_comp] at hx
     have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)
     have qx_int := Normal.isIntegral h_normal (aeval x q)
     exact (h_normal.splits _).splits_of_dvd (map_ne_zero (minpoly.ne_zero (h_normal.isIntegral _)))
@@ -369,7 +369,7 @@ theorem prime_degree_dvd_card [CharZero F] (p_irr : Irreducible p) (p_deg : p.na
     · exact natDegree_le_of_dvd this p_irr.ne_zero
     · exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
   apply minpoly.dvd F α
-  rw [aeval_def, ← eval_map, eval_rootOfSplits]
+  rw [← eval_map_algebraMap, eval_rootOfSplits]
 
 end Gal
 
diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean
@@ -140,9 +140,9 @@ theorem primitive_element_inf_aux [Algebra.IsSeparable F E] : ∃ γ : E, F⟮α
   have h_sep : h.Separable := separable_gcd_right _ (.map (Algebra.IsSeparable.isSeparable F β))
   have h_root : h.eval β = 0 := by
     apply eval_gcd_eq_zero
-    · rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map, ← aeval_def, ←
+    · rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
         Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
-    · rw [eval_map, ← aeval_def, minpoly.aeval]
+    · rw [eval_map_algebraMap, minpoly.aeval]
   have h_splits : Splits (h.map ιEE') := by
     rw [← Polynomial.gcd_map]
     exact (SplittingField.splits _).splits_of_dvd (map_ne_zero map_g_ne_zero)
diff --git a/Mathlib/FieldTheory/SeparableDegree.lean b/Mathlib/FieldTheory/SeparableDegree.lean
@@ -336,7 +336,7 @@ theorem natSepDegree_ne_zero (h : f.natDegree ≠ 0) : f.natSepDegree ≠ 0 := b
   use rootOfSplits (SplittingField.splits f) (degree_ne_of_natDegree_ne (by rwa [natDegree_map]))
   classical
   rw [Multiset.mem_toFinset, mem_aroots]
-  exact ⟨ne_of_apply_ne _ h, by simp only [aeval_def, ← eval_map, eval_rootOfSplits]⟩
+  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩
 
 /-- A polynomial has zero separable degree if and only if it is constant. -/
 theorem natSepDegree_eq_zero_iff : f.natSepDegree = 0 ↔ f.natDegree = 0 :=
diff --git a/Mathlib/LinearAlgebra/Projectivization/Basic.lean b/Mathlib/LinearAlgebra/Projectivization/Basic.lean
@@ -195,7 +195,7 @@ def map {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective f) : 
       rintro ⟨u, hu⟩ ⟨v, hv⟩ ⟨a, ha⟩
       use Units.map σ.toMonoidHom a
       dsimp at ha ⊢
-      erw [← f.map_smulₛₗ, ha])
+      simp [f.map_smulₛₗ, ← ha, Units.smul_def])
 
 theorem map_mk {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective f) (v : V) (hv : v ≠ 0) :
     map f hf (mk K v hv) = mk L (f v) (map_zero f ▸ hf.ne hv) :=
diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
@@ -424,12 +424,12 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : 
     simp only [mem_setOf_eq]
     rw [isRoot_of_unity_iff (NeZero.pos n)]
     refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
-    rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def]
+    rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map_algebraMap]
     exact hx.2
   · simp only [mem_setOf_eq] at hx
     obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2
     refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)
-    rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot]
+    rw [mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, map_cyclotomic, ← IsRoot]
     exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos n)⟩
 
 theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ} [NeZero n] [IsDomain B] {ζ : B}
@@ -440,10 +440,10 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ} [NeZero n] [
       exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
     refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_
     refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
-    rw [mem_rootSet', aeval_def, ← eval_map, map_cyclotomic, ← IsRoot] at hx
+    rw [mem_rootSet', ← eval_map_algebraMap, map_cyclotomic, ← IsRoot] at hx
     exact hx.2
   · simp only [mem_singleton_iff] at hx
-    simpa only [hx, mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, IsRoot] using
+    simpa only [hx, mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, IsRoot] using
       And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic (NeZero.pos n))
 
 theorem adjoin_primitive_root_eq_top {n : ℕ} [NeZero n] [IsDomain B]
diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
@@ -95,7 +95,7 @@ theorem zeta_spec : IsPrimitiveRoot (zeta n A B) n :=
 
 theorem aeval_zeta [IsDomain B] [NeZero (n : B)] :
     aeval (zeta n A B) (cyclotomic n A) = 0 := by
-  rw [aeval_def, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff]
+  rw [← eval_map_algebraMap, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff]
   exact zeta_spec n A B
 
 theorem zeta_isRoot [IsDomain B] [NeZero (n : B)] : IsRoot (cyclotomic n B) (zeta n A B) := by
diff --git a/Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean b/Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean
@@ -181,7 +181,7 @@ protected theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental 
   rintro ⟨f : ℤ[X], f0, ef0⟩
   -- Change `aeval x f = 0` to `eval (map _ f) = 0`, who knew.
   replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0 := by
-    rwa [aeval_def, ← eval_map] at ef0
+    rwa [← eval_map_algebraMap] at ef0
   -- There is a "large" real number `A` such that `(b + 1) ^ (deg f) * |f (x - a / (b + 1))| * A`
   -- is at least one.  This is obtained from lemma `exists_pos_real_of_irrational_root`.
   obtain ⟨A, hA, h⟩ : ∃ A : ℝ, 0 < A ∧ ∀ (a : ℤ) (b : ℕ),
diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean
@@ -212,7 +212,7 @@ theorem discr_powerBasis_eq_norm [Algebra.IsSeparable K L] :
     nodup_roots (Separable.map (Algebra.IsSeparable.isSeparable K pb.gen))
   have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ (minpoly K pb.gen).aroots E := by
     intro σ
-    rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply]
+    rw [mem_roots, IsRoot.def, eval_map_algebraMap, aeval_algHom_apply]
     repeat' simp [minpoly.ne_zero pb.isIntegral_gen]
   apply (algebraMap K E).injective
   rw [map_mul, map_pow, map_neg, map_one, discr_powerBasis_eq_prod'' _ _ _ e]
diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
@@ -57,14 +57,14 @@ theorem cyclotomic_expand_eq_cyclotomic_mul {p n : ℕ} (hp : Nat.Prime p) (hdiv
       have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
       rw [cyclotomic_eq_minpoly_rat hprim hpos]
       refine minpoly.dvd ℚ _ ?_
-      rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
+      rw [← eval_map_algebraMap, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
         @isRoot_cyclotomic_iff]
       convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
       rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
     · have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
       rw [cyclotomic_eq_minpoly_rat hprim hnpos]
       refine minpoly.dvd ℚ _ ?_
-      rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.def, ←
+      rw [← eval_map_algebraMap, map_expand, expand_eval, ← IsRoot.def, ←
         cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, @isRoot_cyclotomic_iff]
       exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv
   · rw [natDegree_expand, natDegree_cyclotomic,
@@ -98,7 +98,7 @@ theorem cyclotomic_expand_eq_cyclotomic {p n : ℕ} (hp : Nat.Prime p) (hdiv : p
     have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm
     rw [cyclotomic_eq_minpoly hprim hpos]
     refine minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) ?_
-    rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
+    rw [← eval_map_algebraMap, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
       @isRoot_cyclotomic_iff]
     convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
     rw [Nat.mul_div_cancel _ hp.pos]
diff --git a/Mathlib/RingTheory/Polynomial/GaussLemma.lean b/Mathlib/RingTheory/Polynomial/GaussLemma.lean
@@ -191,7 +191,7 @@ theorem isIntegrallyClosed_iff' [IsDomain R] :
     rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]
     apply
       degree_eq_one_of_irreducible_of_root ((H _ <| minpoly.monic hx).mp (minpoly.irreducible hx))
-    rw [IsRoot, eval_map, ← aeval_def, minpoly.aeval R x]
+    rw [IsRoot, eval_map_algebraMap, minpoly.aeval R x]
 
 theorem Monic.dvd_of_fraction_map_dvd_fraction_map [IsIntegrallyClosed R] {p q : R[X]}
     (hp : p.Monic) (hq : q.Monic)
