Theorem: Submodule.codisjoint_restrictScalars_iff (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
⊢ Codisjoint (restrictScalars A M₁) (restrictScalars A M₂) ↔ Codisjoint M₁ M₂
Tactic:
simp only [codisjoint_iff, ← Submodule.sup_restrictScalars, Submodule.restrictScalars_eq_top_iff]
State after:
no goals