Also add domRestrict_comp_codRestrict to RingHom and FirstOrder.Language.Hom

Author: wwylele

Mathlib/Algebra/Module/Submodule/LinearMap.lean

@@ -175,7 +175,7 @@ theorem subtype_comp_codRestrict (p : Submodule R₂ M₂) (h : ∀ b, f b ∈ p
   ext fun _ => rfl
 
 @[simp]
-theorem domRestrict_comp_codRestrict (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₂ M₂)
+theorem domRestrict_comp_codRestrict (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂)
     (h : ∀ c, f c ∈ p) :
     g.domRestrict p ∘ₛₗ f.codRestrict p h = g ∘ₛₗ f :=
   rfl

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -736,6 +736,12 @@ theorem comp_restrict (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f
     (SubsemiringClass.subtype s).comp (f.restrict s' s h) = f.comp (SubsemiringClass.subtype s') :=
   rfl
 
+@[simp]
+theorem domRestrict_comp_codRestrict (g : S →+* T) (f : R →+* S) (p : Subsemiring S)
+    (h : ∀ c, f c ∈ p) :
+    (g.domRestrict p).comp (f.codRestrict p h) = g.comp f :=
+  rfl
+
 /-- Restriction of a ring homomorphism to its range interpreted as a subsemiring.
 
 This is the bundled version of `Set.rangeFactorization`. -/

Mathlib/ModelTheory/Substructures.lean

@@ -783,6 +783,12 @@ theorem subtype_comp_codRestrict (f : M →[L] N) (p : L.Substructure N) (h : 
     p.subtype.toHom.comp (codRestrict p f h) = f :=
   ext fun _ => rfl
 
+@[simp]
+theorem domRestrict_comp_codRestrict (g : N →[L] P) (f : M →[L] N) (p : L.Substructure N)
+    (h : ∀ b, f b ∈ p) :
+    (g.domRestrict p).comp (f.codRestrict p h) = g.comp f :=
+  rfl
+
 /-- The range of a first-order hom `f : M → N` is a submodule of `N`.
 See Note [range copy pattern]. -/
 def range (f : M →[L] N) : L.Substructure N :=