Theorem: LinearMap.isCompl_baseChange (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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (range (baseChange R M₁.subtype)) (range (baseChange R M₂.subtype))
Tactic:
rw [← isCompl_restrictScalars_iff A]
State after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Submodule.restrictScalars A (range (baseChange R M₁.subtype)))
    (Submodule.restrictScalars A (range (baseChange R M₂.subtype)))

State before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Submodule.restrictScalars A (range (baseChange R M₁.subtype)))
    (Submodule.restrictScalars A (range (baseChange R M₂.subtype)))
Tactic:
exact isCompl_lTensor hM R
State after:
no goals