Merge master into nightly-testing

Mathlib.lean

@@ -4172,6 +4172,7 @@ import Mathlib.NumberTheory.PrimesCongruentOne
 import Mathlib.NumberTheory.Primorial
 import Mathlib.NumberTheory.PythagoreanTriples
 import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.NumberTheory.RamificationInertia.Galois
 import Mathlib.NumberTheory.Rayleigh
 import Mathlib.NumberTheory.SiegelsLemma
 import Mathlib.NumberTheory.SmoothNumbers
@@ -4610,6 +4611,7 @@ import Mathlib.RingTheory.Finiteness.Nakayama
 import Mathlib.RingTheory.Finiteness.Nilpotent
 import Mathlib.RingTheory.Finiteness.Prod
 import Mathlib.RingTheory.Finiteness.Projective
+import Mathlib.RingTheory.Finiteness.Quotient
 import Mathlib.RingTheory.Finiteness.Subalgebra
 import Mathlib.RingTheory.Finiteness.TensorProduct
 import Mathlib.RingTheory.Fintype
@@ -4751,6 +4753,7 @@ import Mathlib.RingTheory.Localization.NumDen
 import Mathlib.RingTheory.Localization.Pi
 import Mathlib.RingTheory.Localization.Submodule
 import Mathlib.RingTheory.MatrixAlgebra
+import Mathlib.RingTheory.Morita.Basic
 import Mathlib.RingTheory.Multiplicity
 import Mathlib.RingTheory.MvPolynomial
 import Mathlib.RingTheory.MvPolynomial.Basic
@@ -5009,6 +5012,7 @@ import Mathlib.SetTheory.Ordinal.Notation
 import Mathlib.SetTheory.Ordinal.Principal
 import Mathlib.SetTheory.Ordinal.Rank
 import Mathlib.SetTheory.Ordinal.Topology
+import Mathlib.SetTheory.Ordinal.Veblen
 import Mathlib.SetTheory.Surreal.Basic
 import Mathlib.SetTheory.Surreal.Dyadic
 import Mathlib.SetTheory.Surreal.Multiplication

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -423,11 +423,40 @@ end Module
 
 section
 
-variable {S : Type u} [CommRing S]
+universe u₀
+
+namespace Algebra
+
+variable {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S]
 
 variable {M N : ModuleCat.{v} S}
 
-instance : Linear S (ModuleCat.{v} S) where
+/--
+Let `S` be an `S₀`-algebra. Then `S`-modules are modules over `S₀`.
+-/
+scoped instance : Module S₀ M := Module.compHom _ (algebraMap S₀ S)
+
+scoped instance : IsScalarTower S₀ S M where
+  smul_assoc _ _ _ := by rw [Algebra.smul_def, mul_smul]; rfl
+
+scoped instance : SMulCommClass S S₀ M where
+  smul_comm s s₀ n :=
+    show s • algebraMap S₀ S s₀ • n = algebraMap S₀ S s₀ • s • n by
+    rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
+
+/--
+Let `S` be an `S₀`-algebra. Then the category of `S`-modules is `S₀`-linear.
+-/
+scoped instance instLinear : Linear S₀ (ModuleCat.{v} S) where
+  smul_comp _ M N s₀ f g := by ext; simp
+
+end Algebra
+
+section
+
+variable {S : Type u} [CommRing S]
+
+instance : Linear S (ModuleCat.{v} S) := ModuleCat.Algebra.instLinear
 
 variable {X Y X' Y' : ModuleCat.{v} S}
 
@@ -441,6 +470,8 @@ theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) :
 
 end
 
+end
+
 variable (M N : ModuleCat.{v} R)
 
 /-- `ModuleCat.Hom.hom` as an isomorphism of rings. -/

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Limits
 import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.CategoryTheory.Adjunction.Mates
+import Mathlib.CategoryTheory.Linear.LinearFunctor
 
 /-!
 # Change Of Rings
@@ -264,6 +265,24 @@ instance restrictScalars_isEquivalence_of_ringEquiv {R S} [Ring R] [Ring S] (e :
     (ModuleCat.restrictScalars e.toRingHom).IsEquivalence :=
   (restrictScalarsEquivalenceOfRingEquiv e).isEquivalence_functor
 
+instance {R S} [Ring R] [Ring S] (f : R →+* S) : (restrictScalars f).Additive where
+
+instance restrictScalarsEquivalenceOfRingEquiv_additive {R S} [Ring R] [Ring S] (e : R ≃+* S) :
+    (restrictScalarsEquivalenceOfRingEquiv e).functor.Additive where
+
+namespace Algebra
+
+instance {R₀ R S} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S]
+    (f : R →ₐ[R₀] S) : (restrictScalars f.toRingHom).Linear R₀ where
+  map_smul {M N} g r₀ := by ext m; exact congr_arg (· • g.hom m) (f.commutes r₀).symm
+
+instance restrictScalarsEquivalenceOfRingEquiv_linear
+    {R₀ R S} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] (e : R ≃ₐ[R₀] S) :
+    (restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor.Linear R₀ :=
+  inferInstanceAs ((restrictScalars e.toAlgHom.toRingHom).Linear R₀)
+
+end Algebra
+
 open TensorProduct
 
 variable {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S)

Mathlib/CategoryTheory/Action/Limits.lean

@@ -328,6 +328,6 @@ instance mapAction_preadditive [F.Additive] : (F.mapAction G).Additive where
 
 variable {R : Type*} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.Linear R W]
 
-instance mapAction_linear [F.Additive] [F.Linear R] : (F.mapAction G).Linear R where
+instance mapAction_linear [F.Linear R] : (F.mapAction G).Linear R where
 
 end CategoryTheory.Functor

Mathlib/CategoryTheory/Linear/LinearFunctor.lean

@@ -28,7 +28,7 @@ variable (R : Type*) [Semiring R]
 
 /-- An additive functor `F` is `R`-linear provided `F.map` is an `R`-module morphism. -/
 class Functor.Linear {C D : Type*} [Category C] [Category D] [Preadditive C] [Preadditive D]
-  [Linear R C] [Linear R D] (F : C ⥤ D) [F.Additive] : Prop where
+  [Linear R C] [Linear R D] (F : C ⥤ D) : Prop where
   /-- the functor induces a linear map on morphisms -/
   map_smul : ∀ {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f := by aesop_cat
 
@@ -40,7 +40,7 @@ section
 
 variable {R}
 variable {C D : Type*} [Category C] [Category D] [Preadditive C] [Preadditive D]
-  [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : C ⥤ D) [Additive F] [Linear R F]
+  [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : C ⥤ D) [Linear R F]
 
 @[simp]
 theorem map_smul {X Y : C} (r : R) (f : X ⟶ Y) : F.map (r • f) = r • F.map f :=
@@ -53,9 +53,9 @@ theorem map_units_smul {X Y : C} (r : Rˣ) (f : X ⟶ Y) : F.map (r • f) = r 
 instance : Linear R (𝟭 C) where
 
 instance {E : Type*} [Category E] [Preadditive E] [CategoryTheory.Linear R E] (G : D ⥤ E)
-    [Additive G] [Linear R G] : Linear R (F ⋙ G) where
+    [Linear R G] : Linear R (F ⋙ G) where
 
-variable (R)
+variable (R) [F.Additive]
 
 /-- `F.mapLinearMap` is an `R`-linear map whose underlying function is `F.map`. -/
 @[simps]
@@ -103,7 +103,7 @@ namespace Equivalence
 variable {C D : Type*} [Category C] [Category D] [Preadditive C] [Linear R C] [Preadditive D]
   [Linear R D]
 
-instance inverseLinear (e : C ≌ D) [e.functor.Additive] [e.functor.Linear R] :
+instance inverseLinear (e : C ≌ D) [e.functor.Linear R] :
   e.inverse.Linear R where
     map_smul r f := by
       apply e.functor.map_injective

Mathlib/CategoryTheory/Monoidal/Linear.lean

@@ -50,7 +50,7 @@ instance tensoringRight_linear (X : C) : ((tensoringRight C).obj X).Linear R whe
 ensures that the domain is linear monoidal. -/
 theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
     [MonoidalCategory D] [MonoidalPreadditive D] (F : D ⥤ C) [F.Monoidal] [F.Faithful]
-    [F.Additive] [F.Linear R] : MonoidalLinear R D :=
+    [F.Linear R] : MonoidalLinear R D :=
   { whiskerLeft_smul := by
       intros X Y Z r f
       apply F.map_injective

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -205,8 +205,6 @@ theorem pi_caratheodory :
 protected irreducible_def pi : Measure (∀ i, α i) :=
   toMeasure (OuterMeasure.pi fun i => (μ i).toOuterMeasure) (pi_caratheodory μ)
 
--- Porting note: moved from below so that instances about `Measure.pi` and `MeasureSpace.pi`
--- go together
 instance _root_.MeasureTheory.MeasureSpace.pi {α : ι → Type*} [∀ i, MeasureSpace (α i)] :
     MeasureSpace (∀ i, α i) :=
   ⟨Measure.pi fun _ => volume⟩

Mathlib/MeasureTheory/Covering/VitaliFamily.lean

@@ -116,7 +116,6 @@ covering of almost every `s`. -/
 protected def index : Set (X × Set X) :=
   h.exists_disjoint_covering_ae.choose
 
--- Porting note: Needed to add `(_h : FineSubfamilyOn v f s)`
 /-- Given `h : v.FineSubfamilyOn f s`, then `h.covering p` is a set in the family,
 for `p ∈ h.index`, such that these sets form a disjoint covering of almost every `s`. -/
 @[nolint unusedArguments]

Mathlib/MeasureTheory/Decomposition/Jordan.lean

@@ -114,7 +114,6 @@ theorem real_smul_def (r : ℝ) (j : JordanDecomposition α) :
 
 @[simp]
 theorem coe_smul (r : ℝ≥0) : (r : ℝ) • j = r • j := by
-  -- Porting note: replaced `show`
   rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]
 
 theorem real_smul_nonneg (r : ℝ) (hr : 0 ≤ r) : r • j = r.toNNReal • j :=
@@ -145,13 +144,11 @@ def toSignedMeasure : SignedMeasure α :=
 
 theorem toSignedMeasure_zero : (0 : JordanDecomposition α).toSignedMeasure = 0 := by
   ext1 i hi
-  -- Porting note: replaced `erw` by adding further lemmas
   rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
     VectorMeasure.coe_zero, Pi.zero_apply]
 
 theorem toSignedMeasure_neg : (-j).toSignedMeasure = -j.toSignedMeasure := by
   ext1 i hi
-  -- Porting note: removed `rfl` after the `rw` by adding further steps.
   rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
     toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
 
@@ -202,9 +199,8 @@ def toJordanDecomposition (s : SignedMeasure α) : JordanDecomposition α :=
     negPart_finite := inferInstance
     mutuallySingular := by
       refine ⟨iᶜ, hi.1.compl, ?_, ?_⟩
-      -- Porting note: added `NNReal.eq_iff`
-      · rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]; simp [NNReal.eq_iff]
-      · rw [toMeasureOfLEZero_apply _ _ hi.1.compl hi.1.compl.compl]; simp [NNReal.eq_iff] }
+      · rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]; simp
+      · rw [toMeasureOfLEZero_apply _ _ hi.1.compl hi.1.compl.compl]; simp }
 
 theorem toJordanDecomposition_spec (s : SignedMeasure α) :
     ∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
@@ -325,7 +321,6 @@ private theorem eq_of_posPart_eq_posPart {j₁ j₂ : JordanDecomposition α}
   ext1
   · exact hj
   · rw [← toSignedMeasure_eq_toSignedMeasure_iff]
-    -- Porting note: golfed
     unfold toSignedMeasure at hj'
     simp_rw [hj, sub_right_inj] at hj'
     exact hj'
@@ -469,9 +464,8 @@ theorem absolutelyContinuous_ennreal_iff (s : SignedMeasure α) (μ : VectorMeas
     rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hS₁,
       toMeasureOfLEZero_apply _ _ _ hS₁]
     rw [← VectorMeasure.AbsolutelyContinuous.ennrealToMeasure] at h
-    -- Porting note: added `NNReal.eq_iff`
     simp [h (measure_mono_null (i.inter_subset_right) hS₂),
-      h (measure_mono_null (iᶜ.inter_subset_right) hS₂), NNReal.eq_iff]
+      h (measure_mono_null (iᶜ.inter_subset_right) hS₂)]
   · refine VectorMeasure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_
     rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂
     exact null_of_totalVariation_zero s (h hS₂)
@@ -499,13 +493,11 @@ theorem mutuallySingular_iff (s t : SignedMeasure α) :
     refine ⟨u, hmeas, ?_, ?_⟩
     · rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
         toMeasureOfLEZero_apply _ _ _ hmeas]
-      -- Porting note: added `NNReal.eq_iff`
-      simp [hu₁ _ Set.inter_subset_right, NNReal.eq_iff]
+      simp [hu₁ _ Set.inter_subset_right]
     · rw [totalVariation, Measure.add_apply, hjpos, hjneg,
         toMeasureOfZeroLE_apply _ _ _ hmeas.compl,
         toMeasureOfLEZero_apply _ _ _ hmeas.compl]
-      -- Porting note: added `NNReal.eq_iff`
-      simp [hu₂ _ Set.inter_subset_right, NNReal.eq_iff]
+      simp [hu₂ _ Set.inter_subset_right]
   · rintro ⟨u, hmeas, hu₁, hu₂⟩
     exact
       ⟨u, hmeas, fun t htu => null_of_totalVariation_zero _ (measure_mono_null htu hu₁),
@@ -519,8 +511,7 @@ theorem mutuallySingular_ennreal_iff (s : SignedMeasure α) (μ : VectorMeasure
     refine ⟨u, hmeas, ?_, ?_⟩
     · rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hmeas,
         toMeasureOfLEZero_apply _ _ _ hmeas]
-      -- Porting note: added `NNReal.eq_iff`
-      simp [hu₁ _ Set.inter_subset_right, NNReal.eq_iff]
+      simp [hu₁ _ Set.inter_subset_right]
     · rw [VectorMeasure.ennrealToMeasure_apply hmeas.compl]
       exact hu₂ _ (Set.Subset.refl _)
   · rintro ⟨u, hmeas, hu₁, hu₂⟩

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -273,15 +273,13 @@ variable (F p μ)
 noncomputable def lpMeasSubgroupToLpTrim (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
     Lp F p (μ.trim hm) :=
   Memℒp.toLp (mem_lpMeasSubgroup_iff_aeStronglyMeasurable.mp f.mem).choose
-    -- Porting note: had to replace `f` with `f.1` here.
     (memℒp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem)
 
 variable (𝕜)
 
 /-- Map from `lpMeas` to `Lp F p (μ.trim hm)`. -/
 noncomputable def lpMeasToLpTrim (hm : m ≤ m0) (f : lpMeas F 𝕜 m p μ) : Lp F p (μ.trim hm) :=
   Memℒp.toLp (mem_lpMeas_iff_aeStronglyMeasurable.mp f.mem).choose
-    -- Porting note: had to replace `f` with `f.1` here.
     (memℒp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem)
 
 variable {𝕜}
@@ -302,24 +300,20 @@ variable {F 𝕜 p μ}
 
 theorem lpMeasSubgroupToLpTrim_ae_eq (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
     lpMeasSubgroupToLpTrim F p μ hm f =ᵐ[μ] f :=
-  -- Porting note: replaced `(↑f)` with `f.1` here.
   (ae_eq_of_ae_eq_trim (Memℒp.coeFn_toLp (memℒp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem))).trans
     (mem_lpMeasSubgroup_iff_aeStronglyMeasurable.mp f.mem).choose_spec.2.symm
 
 theorem lpTrimToLpMeasSubgroup_ae_eq (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) :
     lpTrimToLpMeasSubgroup F p μ hm f =ᵐ[μ] f :=
-  -- Porting note: filled in the argument
   Memℒp.coeFn_toLp (memℒp_of_memℒp_trim hm (Lp.memℒp f))
 
 theorem lpMeasToLpTrim_ae_eq (hm : m ≤ m0) (f : lpMeas F 𝕜 m p μ) :
     lpMeasToLpTrim F 𝕜 p μ hm f =ᵐ[μ] f :=
-  -- Porting note: replaced `(↑f)` with `f.1` here.
   (ae_eq_of_ae_eq_trim (Memℒp.coeFn_toLp (memℒp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem))).trans
     (mem_lpMeasSubgroup_iff_aeStronglyMeasurable.mp f.mem).choose_spec.2.symm
 
 theorem lpTrimToLpMeas_ae_eq (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) :
     lpTrimToLpMeas F 𝕜 p μ hm f =ᵐ[μ] f :=
-  -- Porting note: filled in the argument
   Memℒp.coeFn_toLp (memℒp_of_memℒp_trim hm (Lp.memℒp f))
 
 /-- `lpTrimToLpMeasSubgroup` is a right inverse of `lpMeasSubgroupToLpTrim`. -/
@@ -461,7 +455,6 @@ variable {m m0 : MeasurableSpace α} {μ : Measure α}
 `f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f`. -/
 theorem lpMeas.ae_fin_strongly_measurable' (hm : m ≤ m0) (f : lpMeas F 𝕜 m p μ) (hp_ne_zero : p ≠ 0)
     (hp_ne_top : p ≠ ∞) :
-    -- Porting note: changed `f` to `f.1` in the next line. Not certain this is okay.
     ∃ g, FinStronglyMeasurable g (μ.trim hm) ∧ f.1 =ᵐ[μ] g :=
   ⟨lpMeasSubgroupToLpTrim F p μ hm f, Lp.finStronglyMeasurable _ hp_ne_zero hp_ne_top,
     (lpMeasSubgroupToLpTrim_ae_eq hm f).symm⟩
@@ -519,9 +512,6 @@ theorem Lp.induction_stronglyMeasurable_aux (hm : m ≤ m0) (hp_ne_top : p ≠ 
     @Lp.induction α F m _ p (μ.trim hm) _ hp_ne_top
       (fun g => P ((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ?_ ?_ ?_ g
   · intro b t ht hμt
-    -- Porting note: needed to pass `m` to `Lp.simpleFunc.coe_indicatorConst` to avoid
-    -- synthesized type class instance is not definitionally equal to expression inferred by typing
-    -- rules, synthesized m0 inferred m
     rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator ht hμt.ne b]
     have hμt' : μ t < ∞ := (le_trim hm).trans_lt hμt
     specialize h_ind b ht hμt'

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -272,8 +272,6 @@ alias condexpIndL1_disjoint_union := condExpIndL1_disjoint_union
 
 end CondexpIndL1
 
--- Porting note: `G` is not automatically inferred in `condExpInd` in Lean 4;
--- to avoid repeatedly typing `(G := ...)` it is made explicit.
 variable (G)
 
 /-- Conditional expectation of the indicator of a set, as a linear map from `G` to L1. -/
@@ -405,8 +403,6 @@ section CondexpL1
 variable {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)]
   {f g : α → F'} {s : Set α}
 
--- Porting note: `F'` is not automatically inferred in `condExpL1CLM` in Lean 4;
--- to avoid repeatedly typing `(F' := ...)` it is made explicit.
 variable (F')
 
 /-- Conditional expectation of a function as a linear map from `α →₁[μ] F'` to itself. -/

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

@@ -61,8 +61,6 @@ local notation "⟪" x ", " y "⟫" => @inner 𝕜 E _ x y
 
 local notation "⟪" x ", " y "⟫₂" => @inner 𝕜 (α →₂[μ] E) _ x y
 
--- Porting note: the argument `E` of `condExpL2` is not automatically filled in Lean 4.
--- To avoid typing `(E := _)` every time it is made explicit.
 variable (E 𝕜)
 
 /-- Conditional expectation of a function in L2 with respect to a sigma-algebra -/

Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

@@ -238,10 +238,8 @@ theorem condExp_stronglyMeasurable_simpleFunc_mul (hm : m ≤ m0) (f : @SimpleFu
     · simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_mul]
   apply @SimpleFunc.induction _ _ m _ (fun f => _)
     (fun c s hs => ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ => ?_) f
-  · -- Porting note: if not classical, `DecidablePred fun x ↦ x ∈ s` cannot be synthesised
-    -- for `Set.piecewise_eq_indicator`
-    classical simp only [@SimpleFunc.const_zero _ _ m, @SimpleFunc.coe_piecewise _ _ m,
-      @SimpleFunc.coe_const _ _ m, @SimpleFunc.coe_zero _ _ m, Set.piecewise_eq_indicator]
+  · simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise,
+      SimpleFunc.coe_const, SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
     rw [this, this]
     refine (condExp_indicator (hg.smul c) hs).trans ?_
     filter_upwards [condExp_smul c g m] with x hx

Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean

@@ -45,14 +45,11 @@ section UniquenessOfConditionalExpectation
 
 theorem lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero (hm : m ≤ m0) (f : lpMeas E' 𝕜 m p μ)
     (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
-    -- Porting note: needed to add explicit casts in the next two hypotheses
     (hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (f : Lp E' p μ) s μ)
     (hf_zero : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, (f : Lp E' p μ) x ∂μ = 0) :
     f =ᵐ[μ] (0 : α → E') := by
   obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top
   refine hfg.trans ?_
-  -- Porting note: added
-  unfold Filter.EventuallyEq at hfg
   refine ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm
   · intro s hs hμs
     have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
@@ -72,8 +69,7 @@ theorem Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' (hm : m ≤ m0) (f : Lp E'
     (hf_zero : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = 0)
     (hf_meas : AEStronglyMeasurable[m] f μ) : f =ᵐ[μ] 0 := by
   let f_meas : lpMeas E' 𝕜 m p μ := ⟨f, hf_meas⟩
-  -- Porting note: `simp only` does not call `rfl` to try to close the goal. See https://github.com/leanprover-community/mathlib4/issues/5025
-  have hf_f_meas : f =ᵐ[μ] f_meas := by simp only [f_meas, Subtype.coe_mk]; rfl
+  have hf_f_meas : f =ᵐ[μ] f_meas := by simp [f_meas, Subtype.coe_mk]
   refine hf_f_meas.trans ?_
   refine lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero hm f_meas hp_ne_zero hp_ne_top ?_ ?_
   · intro s hs hμs