-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma restrictScalars_localized'_smul (I : Submodule R R) (N' : Submodule S N) :
    (I.localized' S p (Algebra.linearMap R S) • N').restrictScalars R =
      I • N'.restrictScalars R

Proof state:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
⊢ ∀ r ∈ localized' S p (Algebra.linearMap R S) I, ∀ n ∈ N', r • n ∈ I • restrictScalars R N'

Tactic:
rintro _ ⟨r, hr, s, rfl⟩ n hn

Result:
case refine_1.intro.intro.intro
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r s • n ∈ I • restrictScalars R N'

Proof state:
case refine_1.intro.intro.intro
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ r • IsLocalization.mk' S 1 s • n ∈ I • restrictScalars R N'

Tactic:
exact smul_mem_smul hr ((Submodule.restrictScalars_mem _ _ _).mpr <| smul_mem _ _ hn)

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r s • n ∈ I • restrictScalars R N'

Tactic:
rw [← IsLocalization.mk'_eq_mk', IsLocalization.mk'_eq_mul_mk'_one, mul_smul, algebraMap_smul]

Result:
case refine_1.intro.intro.intro
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ r • IsLocalization.mk' S 1 s • n ∈ I • restrictScalars R N'

Proof state:
case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ (algebraMap R S) r • n ∈ localized' S p (Algebra.linearMap R S) I • N'

Tactic:
exact Submodule.smul_mem_smul ⟨_, hr, 1, by simp⟩ hn

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
⊢ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N') = I • restrictScalars R N'

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (Submodule.smul_le.mpr fun r hr n hn ↦ ?_)

Result:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
⊢ x ∈ I • restrictScalars R N'

case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ r • n ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')

Proof state:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r 1 = (algebraMap R S) r

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
⊢ x ∈ I • restrictScalars R N'

Tactic:
refine smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ fun _ _ ↦ add_mem

Result:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
⊢ ∀ r ∈ localized' S p (Algebra.linearMap R S) I, ∀ n ∈ N', r • n ∈ I • restrictScalars R N'

Proof state:
case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ r • n ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')

Tactic:
rw [← algebraMap_smul S, Submodule.restrictScalars_mem]

Result:
case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ (algebraMap R S) r • n ∈ localized' S p (Algebra.linearMap R S) I • N'