feat: port MeasureTheory.Measure.OuterMeasure (#3674)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -1521,6 +1521,7 @@ import Mathlib.Mathport.Syntax
 import Mathlib.MeasureTheory.CardMeasurableSpace
 import Mathlib.MeasureTheory.MeasurableSpace
 import Mathlib.MeasureTheory.MeasurableSpaceDef
+import Mathlib.MeasureTheory.Measure.OuterMeasure
 import Mathlib.MeasureTheory.PiSystem
 import Mathlib.ModelTheory.Basic
 import Mathlib.ModelTheory.Encoding

Mathlib/Algebra/Algebra/Tower.lean

@@ -156,8 +156,8 @@ instance (priority := 999) subsemiring (U : Subsemiring S) : IsScalarTower U S A
 #align is_scalar_tower.subsemiring IsScalarTower.subsemiring
 
 -- Porting note: @[nolint instance_priority]
-instance of_ring_hom {R A B : Type _} [CommSemiring R] [CommSemiring A] [CommSemiring B]
-    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
+instance (priority := 999) of_ring_hom {R A B : Type _} [CommSemiring R] [CommSemiring A]
+    [CommSemiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
     @IsScalarTower R A B _ f.toRingHom.toAlgebra.toSMul _ :=
   letI := (f : A →+* B).toAlgebra
   of_algebraMap_eq fun x => (f.commutes x).symm