Sync upstream mathlib4 (2026-08-05, +12 commits)

Counterexamples/DirectSumIsInternal.lean

@@ -60,8 +60,7 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
     · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
     · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
 
-set_option linter.defProp false in
-def withSign.independent : iSupIndep withSign := by
+theorem withSign.independent : iSupIndep withSign := by
   apply
     (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
   intro i

Mathlib.lean

@@ -6483,6 +6483,7 @@ public import Mathlib.RingTheory.AlgebraTower
 public import Mathlib.RingTheory.Algebraic.Basic
 public import Mathlib.RingTheory.Algebraic.Cardinality
 public import Mathlib.RingTheory.Algebraic.Defs
+public import Mathlib.RingTheory.Algebraic.Denominator
 public import Mathlib.RingTheory.Algebraic.Integral
 public import Mathlib.RingTheory.Algebraic.LinearIndependent
 public import Mathlib.RingTheory.Algebraic.MvPolynomial

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -509,12 +509,14 @@ theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) :
     (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x :=
   rfl
 
-@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `ofLinear_toLinearMap`"
+@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `toLinearMap_ofLinearMap`"
   (since := "2026-06-23")]
 theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl
 
 @[simp]
-theorem ofLinear_toLinearMap (h₁ h₂) : (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl
+theorem toLinearMap_ofLinearMap (h₁ h₂) : (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl
+
+@[deprecated (since := "2026-08-04")] alias ofLinear_toLinearMap := toLinearMap_ofLinearMap
 
 end
 

Mathlib/Analysis/Calculus/FDeriv/Extend.lean

@@ -84,7 +84,7 @@ theorem hasFDerivWithinAt_closure_of_tendsto_fderiv {f : E → F} {s : Set E} {x
   refine ContinuousWithinAt.closure_le uv_in ?_ ?_ key
   all_goals
     -- common start for both continuity proofs
-    have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by gcongr <;> exact inter_subset_right
+    have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by grw [inter_subset_right]
     obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by
       simpa [closure_prod_eq] using closure_mono this uv_in
     apply ContinuousWithinAt.mono _ this

Mathlib/Analysis/Complex/HalfPlane.lean

@@ -12,7 +12,7 @@ public import Mathlib.Topology.Instances.EReal.Lemmas
 # Half-planes in ℂ are open
 
 We state that open left, right, upper and lower half-planes in the complex numbers are open sets,
-where the bounding value of the real or imaginary part is given by an `EReal` `x`.
+where the bounding value of the real or imaginary part is given by a real or `EReal` `x`.
 So this includes the full plane and the empty set for `x = ⊤`/`x = ⊥`.
 -/
 
@@ -40,4 +40,20 @@ in the complex plane. -/
 lemma isOpen_im_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < z.im} :=
   isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_im
 
+/-- An open left half-plane is an open set in the complex plane. -/
+lemma isOpen_re_lt (x : ℝ) : IsOpen {z : ℂ | z.re < x} := by
+  simpa using isOpen_re_lt_EReal x
+
+/-- An open right half-plane is an open set in the complex plane. -/
+lemma isOpen_re_gt (x : ℝ) : IsOpen {z : ℂ | x < z.re} := by
+  simpa using isOpen_re_gt_EReal x
+
+/-- An open lower half-plane is an open set in the complex plane. -/
+lemma isOpen_im_lt (x : ℝ) : IsOpen {z : ℂ | z.im < x} := by
+  simpa using isOpen_im_lt_EReal x
+
+/-- An open upper half-plane is an open set in the complex plane. -/
+lemma isOpen_im_gt (x : ℝ) : IsOpen {z : ℂ | x < z.im} := by
+  simpa using isOpen_im_gt_EReal x
+
 end Complex

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

@@ -5,12 +5,10 @@ Authors: Anatole Dedecker, Luigi Massacci
 -/
 module
 
-public import Mathlib.Analysis.Calculus.ContDiff.Operations
-public import Mathlib.MeasureTheory.Function.LocallyIntegrable
+public import Mathlib.Analysis.Calculus.ContDiff.Bounds
+public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.MeasureTheory.Function.Holder
 public import Mathlib.MeasureTheory.Integral.Bochner.Set
-public import Mathlib.Topology.ContinuousMap.Bounded.Normed
-public import Mathlib.Topology.Sets.Compacts
 
 /-!
 # Continuously differentiable functions supported in a given compact set
@@ -715,6 +713,45 @@ theorem norm_toBoundedContinuousFunction (f : 𝓓^{n}_{K}(E, F)) :
   simp [BoundedContinuousFunction.norm_eq_iSup_norm,
     ContDiffMapSupportedIn.seminorm_apply, structureMapCLM_apply]
 
+/-- Define a continuous `𝕜`-linear map from `𝓓^{n₁}_{K₁}(E, F)` to `𝓓^{n₂}_{K₂}(E, F')`. -/
+protected noncomputable def mkCLM (A : 𝓓^{n₁}_{K₁}(E, F) → E → F')
+    (hadd : ∀ f g x, A (f + g) x = A f x + A g x)
+    (hsmul : ∀ (c : 𝕜) f x, A (c • f) x = c • A f x)
+    (hsmooth : ∀ f, ContDiff ℝ n₂ (A f))
+    (hsupp : ∀ f, EqOn (A f) 0 K₂ᶜ)
+    (hbound : ∀ i : ℕ, i ≤ n₂ → ∃ (s : Finset ℕ) (C : ℝ), 0 ≤ C ∧ ∀ f, ∀ x ∈ K₂,
+      ‖iteratedFDeriv ℝ i (A f) x‖ ≤ C * (s.sup fun j ↦ N[𝕜]_{K₁, n₁, j}) f) :
+    𝓓^{n₁}_{K₁}(E, F) →L[𝕜] 𝓓^{n₂}_{K₂}(E, F') :=
+  letI Φ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F') :=
+    { toFun f := ⟨A f, hsmooth f, hsupp f⟩
+      map_add' f g := ext (hadd f g)
+      map_smul' c f := ext (hsmul c f) }
+  { toLinearMap := Φ
+    cont := show Continuous Φ by
+      refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
+        (ContDiffMapSupportedIn.withSeminorms ..) _ (.of_real fun i ↦ ?_)
+      by_cases hi : i ≤ n₂
+      · obtain ⟨s, C, hC, h⟩ := hbound i hi
+        exact ⟨s, C, fun f ↦ ((Φ f).seminorm_le_iff 𝕜 (mul_nonneg hC (apply_nonneg _ _)) i).2
+          fun _ x hx ↦ h f x hx⟩
+      · exact ⟨∅, 0, fun f ↦ by
+          simp [ContDiffMapSupportedIn.seminorm_eq_bot_of_gt 𝕜 (not_le.1 hi)]⟩ }
+
+/-- Define a continous `𝕜`-linear map fom `𝓓^{n}_{K}(E, F)` to a normed space. -/
+protected noncomputable def mkCLMtoNormedSpace {G : Type*} [NormedAddCommGroup G]
+    [NormedSpace 𝕜 G] (A : 𝓓^{n}_{K}(E, F) → G)
+    (hadd : ∀ f g, A (f + g) = A f + A g)
+    (hsmul : ∀ (c : 𝕜) f, A (c • f) = c • A f)
+    (hbound : ∃ (s : Finset ℕ) (C : ℝ), 0 ≤ C ∧ ∀ f,
+      ‖A f‖ ≤ C * (s.sup fun i ↦ N[𝕜]_{K, n, i}) f) :
+    𝓓^{n}_{K}(E, F) →L[𝕜] G :=
+  letI Φ : 𝓓^{n}_{K}(E, F) →ₗ[𝕜] G := ⟨⟨A, hadd⟩, hsmul⟩
+  { toLinearMap := Φ
+    cont := show Continuous Φ by
+      obtain ⟨s, C, hC, h⟩ := hbound
+      exact continuous_normedSpace_rng G (ContDiffMapSupportedIn.withSeminorms 𝕜 E F n K)
+        Φ ⟨s, ⟨C, hC⟩, h⟩ }
+
 /-- The inclusion of the space `𝓓^{n}_{K}(E, F)` into the space `E →ᵇ F` of bounded continuous
 functions as a continuous `𝕜`-linear map. -/
 noncomputable def toBoundedContinuousFunctionCLM : 𝓓^{n}_{K}(E, F) →L[𝕜] E →ᵇ F where
@@ -974,13 +1011,11 @@ lemma norm_integralAgainstBilinLM_le {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃}
 and a function `φ : E → F₂` which is integrable on `K`, this is the *continuous* `𝕜`-linear map
 `f ↦ ∫ x, B (f x) (φ x) ∂μ` from `𝓓^{n}_{K}(E, F₁)` to `F₃`. Otherwise, this is the zero map. -/
 noncomputable def integralAgainstBilinCLM (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (μ : Measure E) (φ : E → F₂) :
-    𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃ where
-  toLinearMap := integralAgainstBilinLM B μ φ
-  cont := show Continuous (integralAgainstBilinLM B μ φ) by
-    refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
-      (norm_withSeminorms 𝕜 _) _
-      (.of_real fun _ ↦ ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, fun f ↦ ?_⟩)
-    simpa using! norm_integralAgainstBilinLM_le
+    𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃ :=
+  ContDiffMapSupportedIn.mkCLMtoNormedSpace 𝕜 (integralAgainstBilinLM B μ φ)
+    (integralAgainstBilinLM B μ φ).map_add (integralAgainstBilinLM B μ φ).map_smul
+    ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, by positivity,
+      fun f ↦ by simpa using! norm_integralAgainstBilinLM_le⟩
 
 @[simp]
 lemma integralAgainstBilinCLM_apply {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : Measure E} {φ : E → F₂}
@@ -1001,4 +1036,68 @@ lemma integralAgainstBilinCLM_eq_setIntegral {B : F₁ →L[𝕜] F₂ →L[𝕜
 
 end Integral
 
+section Multiplication
+
+section bilin
+
+open ContDiffMapSupportedIn
+
+variable {F₁ F₂ F₃ G : Type*} [NormedAlgebra ℝ 𝕜]
+  [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [NormedSpace ℝ F₁]
+  [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [NormedSpace ℝ F₂]
+  [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [NormedSpace ℝ F₃]
+
+open ContinuousLinearMap Finset
+
+variable {𝕜}
+/-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on 𝓓^{n}_{K}(E, F₁),
+where `B` is a continuous `𝕜`-linear map and `g` is a C^n function.
+
+TODO: Introduce a type of bundled C^k functions. -/
+noncomputable def bilinLeftCLM (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {g : E → F₂} (hg : ContDiff ℝ n g) :
+    𝓓^{n}_{K}(E, F₁) →L[𝕜] 𝓓^{n}_{K}(E, F₃) :=
+  ContDiffMapSupportedIn.mkCLM 𝕜 (fun φ x ↦ B (φ x) (g x)) ?hadd ?hsmul (fun φ ↦ ?hsmooth)
+    (fun φ x hx ↦ ?hsupp) (fun k hk ↦ ?hbound)
+where finally
+  case hadd | hsmul => intros; simp
+  case hsmooth =>
+    exact (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp (φ.contDiff.prodMk hg)
+  case hsupp => simp only [φ.zero_on_compl hx, Pi.zero_apply, map_zero, zero_apply]
+  case hbound =>
+    have hcont : Continuous fun x ↦ (Finset.range (k + 1)).sup' Finset.nonempty_range_add_one
+        (fun i ↦ ‖iteratedFDeriv ℝ i g x‖) :=
+      Continuous.finset_sup'_apply Finset.nonempty_range_add_one fun i hi ↦
+        (hg.continuous_iteratedFDeriv (WithTop.coe_le_coe.2
+          (le_trans (WithTop.coe_le_coe.2 (mem_range_succ_iff.mp hi)) hk))).norm
+    obtain ⟨C₀, hC₀⟩ := K.isCompact.exists_bound_of_continuousOn hcont.continuousOn
+    have hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖ := fun i hi x hx ↦
+      (Finset.le_sup' _ (Finset.mem_range_succ_iff.2 hi)).trans
+        ((Real.le_norm_self _).trans ((hC₀ x hx).trans (Real.le_norm_self C₀)))
+    refine ⟨Finset.Iic k, ‖B‖ * 2 ^ k * ‖C₀‖, by positivity, fun φ x hx ↦ ?_⟩
+    calc
+      ‖iteratedFDeriv ℝ k (fun y ↦ B (φ y) (g y)) x‖
+        ≤ ‖B‖ * ∑ i ∈ Finset.range (k + 1), (k.choose i : ℝ) * ‖iteratedFDeriv ℝ i φ x‖ *
+            ‖iteratedFDeriv ℝ (k - i) g x‖ := by
+          simpa using (B.bilinearRestrictScalars ℝ).norm_iteratedFDeriv_le_of_bilinear
+            φ.contDiff hg x (mod_cast hk)
+      _ ≤ ‖B‖ * ∑ i ∈ Finset.range (k + 1), (k.choose i : ℝ) *
+            ((Finset.Iic k).sup fun m ↦ N[𝕜]_{K, n, m}) φ * ‖C₀‖ := by
+          gcongr with i hi
+          · exact (norm_iteratedFDeriv_apply_le_seminorm 𝕜
+              ((WithTop.coe_le_coe.2 (mem_range_succ_iff.mp hi)).trans hk)).trans
+              (Seminorm.le_finset_sup_apply (Finset.mem_Iic.2 (mem_range_succ_iff.mp hi)))
+          · exact hgC₀ (k - i) (Nat.sub_le k i) x hx
+      _ = ‖B‖ * 2 ^ k * ‖C₀‖ * ((Finset.Iic k).sup fun m ↦ N[𝕜]_{K, n, m}) φ := by
+          simp_rw [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose]
+          push_cast
+          ring
+
+@[simp]
+theorem bilinLeftCLM_apply (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {g : E → F₂} (hg : ContDiff ℝ n g)
+    (φ : 𝓓^{n}_{K}(E, F₁)) : bilinLeftCLM B hg φ = fun x => B (φ x) (g x) := rfl
+
+end bilin
+
+end Multiplication
+
 end ContDiffMapSupportedIn

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

@@ -545,8 +545,7 @@ lemma Subalgebra.frontier_subset_frontier :
     (spectrum.isClosed (x : A)).closure_eq]
   apply subset_inter (frontier_spectrum S x)
   rw [frontier_eq_closure_inter_closure]
-  exact inter_subset_right |>.trans <|
-    closure_mono <| compl_subset_compl.mpr <| spectrum.subset_subalgebra x
+  grw [inter_subset_right, spectrum.subset_subalgebra]
 
 open Set Notation
 
@@ -568,12 +567,8 @@ lemma Subalgebra.spectrum_sUnion_connectedComponentIn :
   suffices h_frontier : frontier (σ 𝕜 x \ σ 𝕜 (x : A)) ⊆ frontier (σ 𝕜 (x : A)) from
     disjoint_of_subset_left h_frontier <| disjoint_compl_right.frontier_left
       (spectrum.isClosed _).isOpen_compl
-  rw [sdiff_eq_compl_inter]
-  apply (frontier_inter_subset _ _).trans
-  rw [frontier_compl]
-  apply union_subset <| inter_subset_left
-  refine inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right
-  exact frontier_subset_frontier S x
+  grw [sdiff_eq_compl_inter, frontier_inter_subset, inter_subset_left, inter_subset_right,
+    frontier_compl, frontier_subset_frontier, union_self]
 
 /-- Let `S` be a closed subalgebra of a Banach algebra `A`, and let `x : S`. If `z` is in the
 spectrum of `x`, then the connected component of `z` in the complement of the spectrum of `↑x : A`

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -377,6 +377,7 @@ theorem mapDart_apply (d : G.Dart) : f.mapDart d = ⟨d.1.map f f, f.map_adj d.2
   rfl
 
 /-- The graph homomorphism from a smaller graph to a bigger one. -/
+@[implicit_reducible]
 def ofLE (h : G₁ ≤ G₂) : G₁ →g G₂ := ⟨id, @h⟩
 
 @[simp, norm_cast] lemma coe_ofLE (h : G₁ ≤ G₂) : ⇑(ofLE h) = id := rfl

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -373,7 +373,7 @@ theorem IsCycle.isPath_drop {u n} {p : G.Walk u u} (h : p.IsCycle) (hn : 0 < n)
     (p.drop n).IsPath := by
   replace h : (p.drop 1).IsPath := h.isPath_tail
   rw [← Nat.add_sub_of_le hn, drop_add_eq]
-  simp [h.drop (n - 1)]
+  simp [h.drop (n - 1), -drop_drop]
 
 theorem IsCycle.isPath_take {u n} {p : G.Walk u u} (h : p.IsCycle) (hn : n < p.length) :
     (p.take n).IsPath := by

Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

@@ -117,7 +117,7 @@ lemma dropUntil_eq_drop (p : G.Walk u v) (h : w ∈ p.support) :
   | @cons a _ _ _ p ih =>
     by_cases! h' : w = a
     · subst h'
-      simp [dropUntil_first, drop_support_eq_support_drop_min]
+      simp [dropUntil_first]
     · rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
       grind
 

Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean

@@ -86,6 +86,7 @@ theorem map_eq_nil_iff {p : G.Walk u u} : p.map f = nil ↔ p = nil := by cases
 @[simp]
 theorem length_map : (p.map f).length = p.length := by induction p <;> simp [*]
 
+@[simp]
 theorem map_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
     (p.append q).map f = (p.map f).append (q.map f) := by induction p <;> simp [*]
 
@@ -129,14 +130,24 @@ variable {G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v)
 abbrev mapLe : G'.Walk u v :=
   p.map (.ofLE h)
 
-set_option backward.isDefEq.respectTransparency false in
-lemma support_mapLe_eq_support : (p.mapLe h).support = p.support := by simp
+theorem length_mapLe : (p.mapLe h).length = p.length := by
+  simp
+
+lemma support_mapLe_eq_support : (p.mapLe h).support = p.support := by
+  simp
+
+lemma edges_mapLe_eq_edges : (p.mapLe h).edges = p.edges := by
+  simp
+
+lemma edgeSet_mapLe_eq_edgeSet : (p.mapLe h).edgeSet = p.edgeSet := by
+  simp
 
-set_option backward.isDefEq.respectTransparency false in
-lemma edges_mapLe_eq_edges : (p.mapLe h).edges = p.edges := by simp
+theorem reverse_mapLe : (p.mapLe h).reverse = p.reverse.mapLe h := by
+  simp
 
-set_option backward.isDefEq.respectTransparency false in
-lemma edgeSet_mapLe_eq_edgeSet : (p.mapLe h).edgeSet = p.edgeSet := by simp
+theorem mapLe_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
+    (p.append q).mapLe h = (p.mapLe h).append (q.mapLe h) := by
+  simp
 
 end mapLe