Theorem: Submodule.sup_restrictScalars (DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean)

State before:
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ restrictScalars A (M₁ ⊔ M₂) = restrictScalars A M₁ ⊔ restrictScalars A M₂
Tactic:
apply Submodule.toAddSubmonoid_injective
State after:
case a
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ (restrictScalars A (M₁ ⊔ M₂)).toAddSubmonoid = (restrictScalars A M₁ ⊔ restrictScalars A M₂).toAddSubmonoid

State before:
case a
R✝ : Type u_1
inst✝⁹ : CommRing R✝
A✝ : Type u_2
inst✝⁸ : CommRing A✝
inst✝⁷ : Algebra R✝ A✝
J : Ideal A✝
A : Type u_3
inst✝⁶ : CommSemiring A
R : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Algebra A R
M : Type u_5
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower A R M
M₁ M₂ : Submodule R M
⊢ (restrictScalars A (M₁ ⊔ M₂)).toAddSubmonoid = (restrictScalars A M₁ ⊔ restrictScalars A M₂).toAddSubmonoid
Tactic:
simp only [Submodule.toAddSubmonoid_restrictScalars, Submodule.sup_toAddSubmonoid]
State after:
no goals