chore: bump to v4.30.0

Physlib/ClassicalMechanics/Mass/MassUnit.lean

@@ -63,29 +63,30 @@ lemma div_eq_val (x y : MassUnit) :
 lemma div_ne_zero (x y : MassUnit) : ¬ x / y = (0 : ℝ≥0) := by
   rw [div_eq_val]
   refine coe_ne_zero.mp ?_
-  simp
+  simp [toReal]
 
 @[simp]
 lemma div_pos (x y : MassUnit) : (0 : ℝ≥0) < x/ y := by
   apply lt_of_le_of_ne
-  · exact zero_le (x / y)
+  · exact zero_le
   · exact Ne.symm (div_ne_zero x y)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma div_self (x : MassUnit) :
     x / x = (1 : ℝ≥0) := by
   simp [div_eq_val, x.val_ne_zero]
+  rfl
 
 lemma div_symm (x y : MassUnit) :
     x / y = (y / x)⁻¹ := NNReal.eq <| by
   rw [div_eq_val, inv_eq_one_div, div_eq_val]
   simp
+  rw [toReal, inv_div]
 
 @[simp]
 lemma div_mul_div_coe (x y z : MassUnit) :
-    (x / y : ℝ) * (y /z : ℝ) = x /z := by
-  simp [div_eq_val]
+    (x / y : ℝ) * (y / z : ℝ) = x / z := by
+  simp [div_eq_val, toReal]
   field_simp
 
 /-!
@@ -107,8 +108,6 @@ lemma scale_div_self (x : MassUnit) (r : ℝ) (hr : 0 < r) :
 lemma self_div_scale (x : MassUnit) (r : ℝ) (hr : 0 < r) :
     x / scale r x hr = (⟨1/r, _root_.div_nonneg (by simp) (le_of_lt hr)⟩ : ℝ≥0) := by
   simp [scale, div_eq_val]
-  ext
-  simp only [coe_mk]
   field_simp
 
 @[simp]
@@ -120,6 +119,7 @@ lemma scale_div_scale (x1 x2 : MassUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 <
     scale r1 x1 hr1 / scale r2 x2 hr2 = (⟨r1, le_of_lt hr1⟩ / ⟨r2, le_of_lt hr2⟩) * (x1 / x2) := by
   refine NNReal.eq ?_
   simp [scale, div_eq_val]
+  rw [toReal]
   field_simp
 
 @[simp]
@@ -187,12 +187,12 @@ noncomputable def nominalSolarMasses : MassUnit := scale (1.988416e30) kilograms
 -/
 
 lemma pounds_div_ounces : pounds / ounces = (16 : ℝ≥0) := NNReal.eq <| by
-  simp [pounds, ounces]; norm_num
+  simp [pounds, ounces]; rw [toReal]; norm_num
 
 lemma shortTons_div_kilograms : shortTons / kilograms = (907.18474 : ℝ≥0) := NNReal.eq <| by
-  simp [shortTons, pounds]; norm_num
+  simp [shortTons, pounds]; rw [toReal]; norm_num
 
 lemma longTons_div_kilograms : longTons / kilograms = (1016.0469088 : ℝ≥0) := NNReal.eq <| by
-  simp [longTons, pounds]; norm_num
+  simp [longTons, pounds]; rw [toReal]; norm_num
 
 end MassUnit

Physlib/Electromagnetism/Charge/ChargeUnit.lean

@@ -68,29 +68,31 @@ lemma div_eq_val (x y : ChargeUnit) :
 lemma div_ne_zero (x y : ChargeUnit) : ¬ x / y = (0 : ℝ≥0) := by
   rw [div_eq_val]
   refine coe_ne_zero.mp ?_
-  simp
+  simp [toReal]
 
 @[simp]
 lemma div_pos (x y : ChargeUnit) : (0 : ℝ≥0) < x/ y := by
   apply lt_of_le_of_ne
-  · exact zero_le (x / y)
+  · exact zero_le
   · exact Ne.symm (div_ne_zero x y)
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma div_self (x : ChargeUnit) :
     x / x = (1 : ℝ≥0) := by
   simp [div_eq_val, x.val_ne_zero]
+  rfl
 
 lemma div_symm (x y : ChargeUnit) :
     x / y = (y / x)⁻¹ := NNReal.eq <| by
   rw [div_eq_val, inv_eq_one_div, div_eq_val]
   simp
+  rw [toReal, inv_div]
 
 @[simp]
 lemma div_mul_div_coe (x y z : ChargeUnit) :
-    (x / y : ℝ) * (y /z : ℝ) = x /z := by
-  simp [div_eq_val]
+    (x / y : ℝ) * (y / z : ℝ) = x / z := by
+  simp [div_eq_val, toReal]
   field_simp
 
 /-!
@@ -112,8 +114,6 @@ lemma scale_div_self (x : ChargeUnit) (r : ℝ) (hr : 0 < r) :
 lemma self_div_scale (x : ChargeUnit) (r : ℝ) (hr : 0 < r) :
     x / scale r x hr = (⟨1/r, _root_.div_nonneg (by simp) (le_of_lt hr)⟩ : ℝ≥0) := by
   simp [scale, div_eq_val]
-  ext
-  simp only [coe_mk]
   field_simp
 
 @[simp]
@@ -125,6 +125,7 @@ lemma scale_div_scale (x1 x2 : ChargeUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0
     scale r1 x1 hr1 / scale r2 x2 hr2 = (⟨r1, le_of_lt hr1⟩ / ⟨r2, le_of_lt hr2⟩) * (x1 / x2) := by
   refine NNReal.eq ?_
   simp [scale, div_eq_val]
+  rw [toReal]
   field_simp
 
 @[simp]

Physlib/Mathematics/DataStructures/Matrix/LieTrace.lean

@@ -253,7 +253,7 @@ lemma exp_map_algebraMap {n : Type*} [Fintype n] [DecidableEq n]
   erw [Matrix.map_tsum (algebraMap ℝ ℂ).toAddMonoidHom RCLike.continuous_ofReal hs]
   apply tsum_congr
   intro k
-  erw [Matrix.map_smul, Matrix.map_pow]
+  erw [Matrix.map_smul, Matrix.map_pow A (algebraMap ℝ ℂ) k]
   simp
 
 end NormedSpace

Physlib/Mathematics/Distribution/Basic.lean

@@ -7,7 +7,7 @@ module
 
 public import Physlib.Meta.TODO.Basic
 public import Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
-public import Mathlib.Topology.Algebra.Module.PointwiseConvergence
+public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
 /-!
 
 # Distributions

Physlib/Mathematics/Distribution/PowMul.lean

@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
+public import Mathlib.Analysis.Calculus.ContDiff.Bounds
 /-!
 
 ## The multiple of a Schwartz map by `x`
@@ -37,19 +38,17 @@ lemma norm_iteratedFDeriv_ofRealCLM {x} (i : ℕ) :
     induction i with
     | zero =>
       simp [iteratedFDeriv_succ_eq_comp_right]
-      rw [@ContinuousLinearMap.norm_def]
-      apply ContinuousLinearMap.opNorm_eq_of_bounds
-      · simp
-      · intro x
-        simp only [fderiv_eq_smul_deriv, Real.norm_eq_abs, one_mul]
-        rw [← @RCLike.ofRealCLM_apply]
-        simp [- RCLike.ofRealCLM_apply, norm_smul]
-        simp
-      · intro N hN h
-        have h1 := h 1
-        rw [← RCLike.ofRealCLM_apply] at h1
-        simp [- RCLike.ofRealCLM_apply] at h1
-        simpa using h1
+      rw [ContinuousMultilinearMap.norm_def]
+      rw [← RCLike.ofRealCLM_apply]
+      simp [-RCLike.ofRealCLM_apply, Real.norm_eq_abs]
+      simp
+      apply le_antisymm
+      · apply csInf_le ⟨0, fun c hc => hc.1⟩
+        exact ⟨le_of_lt one_pos, fun m => by rw [one_mul]⟩
+      · apply le_csInf
+        · exact ⟨1, le_of_lt one_pos, fun m => by rw [one_mul]⟩
+        · intro c ⟨_, hc⟩
+          simpa using hc (fun _ => 1)
     | succ i ih =>
       rw [iteratedFDeriv_succ_eq_comp_right]
       simp only [Nat.succ_eq_add_one, ContinuousLinearMap.fderiv, Function.comp_apply,

Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean

@@ -201,9 +201,9 @@ def pseudoRiemannianMetricValToQuadraticForm
   exists_companion' :=
       ⟨LinearMap.mk₂ ℝ (fun v y => val x v y + val x y v)
         (fun v₁ v₂ y => by simp only [map_add, add_apply]; ring)
-        (fun a v y => by simp only [map_smul, smul_apply]; ring_nf; exact Eq.symm (smul_add ..))
+        (fun a v y => by simp only [map_smul, smul_apply]; ring)
         (fun v y₁ y₂ => by simp only [map_add, add_apply]; ring)
-        (fun a v y => by simp only [map_smul, smul_apply]; ring_nf; exact Eq.symm (smul_add ..)),
+        (fun a v y => by simp only [map_smul, smul_apply]; ring),
             by
               intro v y
               simp only [LinearMap.mk₂_apply, ContinuousLinearMap.map_add,
@@ -383,6 +383,7 @@ lemma flatL_surj
         fun f => f.toLinearMap
       let from_dual : Module.Dual ℝ (TangentSpace I x) → (TangentSpace I x →L[ℝ] ℝ) := fun f =>
         ContinuousLinearMap.mk f (by
+          have : T2Space (TangentSpace I x) := inferInstanceAs (T2Space E)
           apply LinearMap.continuous_of_finiteDimensional)
       let equiv : (TangentSpace I x →L[ℝ] ℝ) ≃ₗ[ℝ] Module.Dual ℝ (TangentSpace I x) :=
       { toFun := to_dual,
@@ -406,6 +407,7 @@ def flatEquiv
     (g : PseudoRiemannianMetric E H M n I)
     (x : M) :
     TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
+  have : T2Space (TangentSpace I x) := inferInstanceAs (T2Space E)
   LinearEquiv.toContinuousLinearEquiv
     (LinearEquiv.ofBijective
       ((g.flatL x).toLinearMap)
@@ -567,13 +569,11 @@ noncomputable def cotangentToQuadraticForm (g : PseudoRiemannianMetric E H M n I
           cotangentMetricVal g x ω₁ ω₂ + cotangentMetricVal g x ω₂ ω₁)
         (fun ω₁ ω₂ ω₃ => by simp only [cotangentMetricVal, map_add, add_apply]; ring)
         (fun a ω₁ ω₂ => by
-          simp only [cotangentMetricVal, map_smul, smul_apply];
-          ring_nf; exact Eq.symm (smul_add ..))
+          simp only [cotangentMetricVal, map_smul, smul_apply]; ring)
         (fun ω₁ ω₂ ω₃ => by
           simp only [cotangentMetricVal, map_add, add_apply]; ring)
         (fun a ω₁ ω₂ => by
-          simp only [cotangentMetricVal, map_smul, smul_apply]; ring_nf;
-          exact Eq.symm (smul_add ..)),
+          simp only [cotangentMetricVal, map_smul, smul_apply]; ring),
           by
             intro ω₁ ω₂
             simp only [LinearMap.mk₂_apply, cotangentMetricVal]

Physlib/Mathematics/List.lean

@@ -42,7 +42,7 @@ lemma takeWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
     simp only [List.takeWhile, List.eraseIdx_zero]
     by_cases hPb : P b
     · have hPa : P a := by
-        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
+        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp) (by simpa using hPb)
       simp [hPb, hPa]
     · simp only [hPb, decide_false]
       simp_all only [List.length_cons, List.get_eq_getElem, List.tail_cons, decide_false,
@@ -98,7 +98,7 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
       Nat.sub_eq_zero_of_le, List.eraseIdx_zero]
     by_cases hPb : P b
     · have hPa : P a := by
-        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
+        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp) (by simpa using hPb)
       simp [hPb, hPa]
     · simp only [List.tail_cons, hPb, decide_false, Bool.false_eq_true, not_false_eq_true,
       List.dropWhile_cons_of_neg]
@@ -111,7 +111,7 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
     simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ]
     by_cases hPb : P b
     · have hPa : P a := by
-        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
+        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp) (by simpa using hPb)
       simp only [List.dropWhile, hPa, decide_true, List.takeWhile, hPb, List.length_cons,
         add_le_add_iff_right, Nat.reduceSubDiff]
       rw [dropWile_eraseIdx]

Physlib/Mathematics/SpecialFunctions/PhysHermite.lean

@@ -136,7 +136,7 @@ lemma iterate_derivative_physHermite_self {n : ℕ} :
       Nat.cast_inj, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, false_and, or_false]
     rw [Nat.descFactorial_self]
   | m + 1 =>
-    rw [coeff_physHermite_of_lt (by omega), Polynomial.coeff_C_ne_zero (by omega)]
+    rw [coeff_physHermite_of_lt (by omega), Polynomial.coeff_C_of_ne_zero (by omega)]
     rfl
 
 @[simp]
@@ -291,7 +291,7 @@ lemma guassian_integrable_polynomial {b : ℝ} (hb : 0 < b) (P : Polynomial ℤ)
   conv =>
     enter [1, x]
     rw [Polynomial.aeval_eq_sum_range, Finset.sum_mul]
-  apply MeasureTheory.integrable_finset_sum
+  apply MeasureTheory.integrable_finsetSum
   intro i hi
   have h2 : (fun a => P.coeff i • a ^ i * Real.exp (-b * a ^ 2)) =
       (P.coeff i : ℝ) • (fun x => (x ^ (i : ℝ) * Real.exp (-b * x ^ 2))) := by
@@ -309,7 +309,7 @@ lemma guassian_integrable_polynomial_cons {b c : ℝ} (hb : 0 < b) (P : Polynomi
   conv =>
     enter [1, x]
     rw [Polynomial.aeval_eq_sum_range, Finset.sum_mul]
-  apply MeasureTheory.integrable_finset_sum
+  apply MeasureTheory.integrable_finsetSum
   intro i hi
   have h2 : (fun a => P.coeff i • (c * a) ^ i * Real.exp (-b * a ^ 2)) =
       (c ^ i * P.coeff i : ℝ) • (fun x => (x ^ (i : ℝ) * Real.exp (-b * x ^ 2))) := by

Physlib/Particles/FlavorPhysics/CKMMatrix/Invariants.lean

@@ -28,7 +28,6 @@ noncomputable section
 namespace Invariant
 
 /-- The complex jarlskog invariant for a CKM matrix. -/
-@[simps!]
 def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
   [V]us * [V]cb * conj [V]ub * conj [V]cs
 

Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean

@@ -155,7 +155,8 @@ lemma le_schwartzSubmodule (d : ℕ) (a : ℕ∞) : polyBddSchwartzSubmodule d a
 
 lemma antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
     polyBddSchwartzSubmodule d b ≤ polyBddSchwartzSubmodule d a := by
-  simp only [polyBddSchwartzSubmodule, polyBddSchwartzIncl, LinearMap.range_domRestrict]
+  simp only [polyBddSchwartzSubmodule, polyBddSchwartzIncl,
+    ContinuousLinearMap.toLinearMap_domRestrict, LinearMap.range_domRestrict]
   exact Submodule.map_mono (polyBddSchwartzMap_antitone d h)
 
 /-!
@@ -264,7 +265,7 @@ lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDH
             rw [← mul_zero (C * 2 ^ d), ← zero_pow (M₀ := ℝ) hd.ne']
             refine ENNReal.tendsto_ofReal <| Tendsto.const_mul (C * 2 ^ d) ?_
             exact tendsto_one_div_add_atTop_nhds_zero_nat.pow d
-        refine Tendsto.squeeze tendsto_const_nhds hξB (zero_le _) (fun n ↦ ?_)
+        refine Tendsto.squeeze tendsto_const_nhds hξB (zero_le) (fun n ↦ ?_)
         suffices ∫⁻ x, ‖σ n x‖ₑ ^ 2 = ∫⁻ x in B n, ‖σ n x‖ₑ ^ 2 by
           rw [this]
           refine setLIntegral_mono_ae' measurableSet_ball ?_
@@ -280,7 +281,7 @@ lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDH
         apply tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq.mpr
         have hψξ : Tendsto (fun n ↦ ∫⁻ x, ‖(ψ n - ξ) x‖ₑ ^ 2) atTop (nhds 0) :=
           tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq.mp (sub_self ξ ▸ hψξ.sub_const ξ)
-        refine Tendsto.squeeze tendsto_const_nhds hψξ (zero_le _) (fun n ↦ ?_)
+        refine Tendsto.squeeze tendsto_const_nhds hψξ (zero_le) (fun n ↦ ?_)
         refine lintegral_mono_ae ?_
         filter_upwards [hφσ_ae n, hψξ_ae n] with x h h'
         simp_rw [h, h', Pi.sub_apply, hg, s, ← mul_sub]

Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean

@@ -100,7 +100,7 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial
     rw [Finsupp.sum]
     simp
   rw [h2]
-  apply MeasureTheory.integrable_finset_sum
+  apply MeasureTheory.integrable_finsetSum
   intro i hi
   simp only [mul_assoc]
   have hf' : (fun x => ↑(a i) * (physHermite i (x/Q.ξ) *
@@ -199,7 +199,7 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     funext x
     rw [← ha]
     simp [← Finset.sum_mul, Finsupp.sum]
-  rw [h2, MeasureTheory.integral_finset_sum]
+  rw [h2, MeasureTheory.integral_finsetSum]
   · apply Finset.sum_eq_zero
     intro x hx
     simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow,
@@ -394,7 +394,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       (Complex.I * ↑c * ↑y) ^ r / r ! *
       (f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) = fun (n : ℕ) => 0 := by
     funext n
-    rw [MeasureTheory.integral_finset_sum]
+    rw [MeasureTheory.integral_finsetSum]
     · apply Finset.sum_eq_zero
       intro r hr
       have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! *

Physlib/QuantumMechanics/OneDimension/Operators/Parity.lean

@@ -8,6 +8,7 @@ module
 public import Physlib.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
 public import Physlib.QuantumMechanics.OneDimension.Operators.Unbounded
 public import Mathlib.MeasureTheory.Measure.Haar.Unique
+public import Mathlib.Analysis.Calculus.ContDiff.Operations
 /-!
 
 # Parity operator
@@ -47,7 +48,6 @@ def parityOperator : (ℝ → ℂ) →ₗ[ℂ] (ℝ → ℂ) where
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The parity operator on the Schwartz maps is defined as the linear map from
   `𝓢(ℝ, ℂ)` to itself, such that `ψ` is taken to `fun x => ψ (-x)`. -/
 def parityOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by
@@ -67,7 +67,7 @@ def parityOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by
       simp [ContinuousLinearMap.norm_id]
     | .succ (.succ n) =>
       rw [iteratedFDeriv_succ_eq_comp_right]
-      simp only [Nat.succ_eq_add_one, fderiv_id', Function.comp_apply,
+      simp only [Nat.succ_eq_add_one, fderiv_fun_id, Function.comp_apply,
         LinearIsometryEquiv.norm_map, ge_iff_le]
       rw [iteratedFDeriv_const_of_ne]
       simp only [Pi.zero_apply, norm_zero]
@@ -80,7 +80,6 @@ def parityOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by
     intro x
     simp
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The unbounded parity operator, whose domain is Schwartz maps. -/
 def parityOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective :=
   UnboundedOperator.ofSelfCLM parityOperatorSchwartz
@@ -99,7 +98,6 @@ lemma parityOperatorSchwartz_parityOperatorSchwartz (ψ : 𝓢(ℝ, ℂ)) :
 
 open InnerProductSpace
 
-set_option backward.isDefEq.respectTransparency false in
 lemma parityOperatorUnbounded_isSelfAdjoint :
     parityOperatorUnbounded.IsSelfAdjoint := by
   intro ψ1 ψ2
@@ -113,8 +111,6 @@ lemma parityOperatorUnbounded_isSelfAdjoint :
   · simp only [neg_neg, f]
     rfl
 
-open InnerProductSpace
-
 end HilbertSpace
 end
 end OneDimension