Merge branch 'nightly-testing' of github.com:leanprover-community/mat…

…hlib4 into nightly-testing

Mathlib/Algebra/Order/Ring/Cast.lean

@@ -24,15 +24,17 @@ open Function Nat
 variable {R : Type*}
 
 namespace Int
-section OrderedRing
-variable [OrderedRing R]
+section OrderedAddCommGroupWithOne
+
+variable [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (· + ·) (· ≤ ·)]
+variable [ZeroLEOneClass R] [NeZero (1 : R)]
 
 lemma cast_mono : Monotone (Int.cast : ℤ → R) := by
   intro m n h
   rw [← sub_nonneg] at h
   lift n - m to ℕ using h with k hk
   rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]
-  exact k.cast_nonneg
+  exact k.cast_nonneg'
 
 variable [Nontrivial R] {m n : ℤ}
 
@@ -56,7 +58,7 @@ lemma cast_strictMono : StrictMono (fun x : ℤ => (x : R)) :=
 
 @[simp] lemma cast_lt_zero : (n : R) < 0 ↔ n < 0 := by rw [← cast_zero, cast_lt]
 
-end OrderedRing
+end OrderedAddCommGroupWithOne
 
 section LinearOrderedRing
 variable [LinearOrderedRing R] {a b n : ℤ} {x : R}

Mathlib/Analysis/CstarAlgebra/Multiplier.lean

@@ -447,7 +447,7 @@ maps `Lₐ Rₐ : A →L[𝕜] A` given by left- and right-multiplication by `a`
 Warning: if `A = 𝕜`, then this is a coercion which is not definitionally equal to the
 `algebraMap 𝕜 𝓜(𝕜, 𝕜)` coercion, but these are propositionally equal. See
 `DoubleCentralizer.coe_eq_algebraMap` below. -/
--- Porting note: added `noncomputable` because an IR check failed?
+-- Porting note: added `noncomputable`; IR check does not recognise `ContinuousLinearMap.mul`
 @[coe]
 protected noncomputable def coe (a : A) : 𝓜(𝕜, A) :=
   { fst := ContinuousLinearMap.mul 𝕜 A a

Mathlib/Analysis/Quaternion.lean

@@ -86,7 +86,6 @@ noncomputable instance : NormedDivisionRing ℍ where
     simp only [norm_eq_sqrt_real_inner, inner_self, normSq.map_mul]
     exact Real.sqrt_mul normSq_nonneg _
 
--- Porting note: added `noncomputable`
 noncomputable instance : NormedAlgebra ℝ ℍ where
   norm_smul_le := norm_smul_le
   toAlgebra := Quaternion.algebra

Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean

@@ -25,14 +25,7 @@ open Opposite
 
 open MonoidalCategory
 
--- Porting note: made it noncomputable.
--- `failed to compile definition, consider marking it as 'noncomputable' because it`
--- `depends on 'CategoryTheory.typesMonoidal', and it does not have executable code`
--- I don't know if that is a problem, might need to change it back in the future, but
--- if so it might be better to fix then instead of at the moment of porting.
-
 /-- `(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type`. -/
-noncomputable
 def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] :
     LaxMonoidalFunctor C (Type v) := .ofTensorHom
     (F := coyoneda.obj (op (𝟙_ C)))

Mathlib/Computability/PartrecCode.lean

@@ -79,7 +79,6 @@ inductive Code : Type
   | prec : Code → Code → Code
   | rfind' : Code → Code
 
--- Porting note: `Nat.Partrec.Code.recOn` is noncomputable in Lean4, so we make it computable.
 compile_inductive% Code
 
 end Nat.Partrec

Mathlib/Computability/TMToPartrec.lean

@@ -867,7 +867,6 @@ inductive Λ'
   | pred (q₁ q₂ : Λ')
   | ret (k : Cont')
 
--- Porting note: `Turing.PartrecToTM2.Λ'.rec` is noncomputable in Lean4, so we make it computable.
 compile_inductive% Code
 compile_inductive% Cont'
 compile_inductive% K'

Mathlib/Data/Analysis/Topology.lean

@@ -153,10 +153,8 @@ theorem ext [T : TopologicalSpace α] {σ : Type*} {F : Ctop α σ} (H₁ : ∀
 
 variable [TopologicalSpace α]
 
--- Porting note: add non-computable : because
--- > ... it depends on `Inter.inter`, and it does not have executable code.
 /-- The topological space realizer made of the open sets. -/
-protected noncomputable def id : Realizer α :=
+protected def id : Realizer α :=
   ⟨{ x : Set α // IsOpen x },
     { f := Subtype.val
       top := fun _ ↦ ⟨univ, isOpen_univ⟩

Mathlib/MeasureTheory/Measure/Haar/Basic.lean

@@ -83,10 +83,6 @@ variable {G : Type*} [Group G]
 
 namespace haar
 
--- Porting note: Even in `noncomputable section`, a definition with `to_additive` require
---               `noncomputable` to generate an additive definition.
---               Please refer to leanprover/lean4#2077.
-
 /-- The index or Haar covering number or ratio of `K` w.r.t. `V`, denoted `(K : V)`:
   it is the smallest number of (left) translates of `V` that is necessary to cover `K`.
   It is defined to be 0 if no finite number of translates cover `K`. -/
@@ -341,11 +337,6 @@ theorem nonempty_iInter_clPrehaar (K₀ : PositiveCompacts G) :
 ### Lemmas about `chaar`
 -/
 
-
--- Porting note: Even in `noncomputable section`, a definition with `to_additive` require
---               `noncomputable` to generate an additive definition.
---               Please refer to leanprover/lean4#2077.
-
 /-- This is the "limit" of `prehaar K₀ U K` as `U` becomes a smaller and smaller open
   neighborhood of `(1 : G)`. More precisely, it is defined to be an arbitrary element
   in the intersection of all the sets `clPrehaar K₀ V` in `haarProduct K₀`.
@@ -463,10 +454,6 @@ theorem is_left_invariant_chaar {K₀ : PositiveCompacts G} (g : G) (K : Compact
     apply is_left_invariant_prehaar; rw [h2U.interior_eq]; exact ⟨1, h3U⟩
   · apply continuous_iff_isClosed.mp this; exact isClosed_singleton
 
--- Porting note: Even in `noncomputable section`, a definition with `to_additive` require
---               `noncomputable` to generate an additive definition.
---               Please refer to leanprover/lean4#2077.
-
 /-- The function `chaar` interpreted in `ℝ≥0`, as a content -/
 @[to_additive "additive version of `MeasureTheory.Measure.haar.haarContent`"]
 noncomputable def haarContent (K₀ : PositiveCompacts G) : Content G where
@@ -518,13 +505,8 @@ open haar
 ### The Haar measure
 -/
 
-
 variable [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G]
 
--- Porting note: Even in `noncomputable section`, a definition with `to_additive` require
---               `noncomputable` to generate an additive definition.
---               Please refer to leanprover/lean4#2077.
-
 /-- The Haar measure on the locally compact group `G`, scaled so that `haarMeasure K₀ K₀ = 1`. -/
 @[to_additive
 "The Haar measure on the locally compact additive group `G`, scaled so that