[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
⊢ coeSubmodule S ⊥ = ⊥
[PROOFSTEP]
rw [coeSubmodule, Submodule.map_bot]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
⊢ coeSubmodule S ⊤ = 1
[PROOFSTEP]
rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (↑(algebraMap R S) '' s)
[PROOFSTEP]
rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
s : Set R
⊢ Submodule.span R (↑(Algebra.linearMap R S) '' s) = Submodule.span R (↑(algebraMap R S) '' s)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
x : R
⊢ coeSubmodule S (Ideal.span {x}) = Submodule.span R {↑(algebraMap R S) x}
[PROOFSTEP]
rw [coeSubmodule_span, Set.image_singleton]
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
h : IsNoetherianRing R
⊢ IsNoetherianRing S
[PROOFSTEP]
rw [isNoetherianRing_iff, isNoetherian_iff_wellFounded] at h ⊢
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ Submodule.IsPrincipal (coeSubmodule S I) ↔ Submodule.IsPrincipal I
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ Submodule.IsPrincipal (coeSubmodule S I) → Submodule.IsPrincipal I
[PROOFSTEP]
rintro ⟨⟨x, hx⟩⟩
[GOAL]
case mpr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ Submodule.IsPrincipal I → Submodule.IsPrincipal (coeSubmodule S I)
[PROOFSTEP]
rintro ⟨⟨x, hx⟩⟩
[GOAL]
case mp.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = Submodule.span R {x}
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x
[GOAL]
case mp.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = Submodule.span R {x}
x_mem : x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem
[GOAL]
case mp.mk.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = Submodule.span R {↑(algebraMap R S) x}
x_mem : ↑(algebraMap R S) x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
refine' ⟨⟨x, coeSubmodule_injective S h _⟩⟩
[GOAL]
case mp.mk.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = Submodule.span R {↑(algebraMap R S) x}
x_mem : ↑(algebraMap R S) x ∈ coeSubmodule S I
⊢ coeSubmodule S I = coeSubmodule S (Submodule.span R {x})
[PROOFSTEP]
rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]
[GOAL]
case mpr.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = Submodule.span R {x}
⊢ Submodule.IsPrincipal (coeSubmodule S I)
[PROOFSTEP]
refine' ⟨⟨algebraMap R S x, _⟩⟩
[GOAL]
case mpr.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = Submodule.span R {x}
⊢ coeSubmodule S I = Submodule.span R {↑(algebraMap R S) x}
[PROOFSTEP]
rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ x ∈ Submodule.span S a ↔ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ x ∈ Submodule.span S a → ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
case mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) → x ∈ Submodule.span S a
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
refine' Submodule.span_induction h _ _ _ _
[GOAL]
case mp.refine'_1
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (x : N), x ∈ a → ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
rintro x hx
[GOAL]
case mp.refine'_1
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ x = mk' S 1 1 • x
[PROOFSTEP]
rw [mk'_one, _root_.map_one, one_smul]
[GOAL]
case mp.refine'_2
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, 0 = mk' S 1 z • y
[PROOFSTEP]
exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ 0 = mk' S 1 1 • 0
[PROOFSTEP]
rw [mk'_one, _root_.map_one, one_smul]
[GOAL]
case mp.refine'_3
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (x y : N),
    (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) →
      (∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z, y = mk' S 1 z • y_1) →
        ∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z, x + y = mk' S 1 z • y_1
[PROOFSTEP]
rintro _ _ ⟨y, hy, z, rfl⟩ ⟨y', hy', z', rfl⟩
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ ∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z_1, mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 z_1 • y_1
[PROOFSTEP]
refine'
  ⟨(z' : R) • y + (z : R) • y', Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'), z * z', _⟩
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • (↑z' • y + ↑z • y')
[PROOFSTEP]
rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ← IsScalarTower.algebraMap_smul S (z' : R), smul_smul,
  smul_smul]
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z') • y + (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z) • y'
[PROOFSTEP]
congr 1
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro.e_a
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z • y = (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z') • y
[PROOFSTEP]
rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, _root_.map_one, mul_one, mul_one]
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro.e_a
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z' • y' = (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z) • y'
[PROOFSTEP]
rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, _root_.map_one, mul_one, one_mul]
[GOAL]
case mp.refine'_4
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (a_1 : S) (x : N),
    (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) → ∃ y, y ∈ Submodule.span R a ∧ ∃ z, a_1 • x = mk' S 1 z • y
[PROOFSTEP]
rintro a _ ⟨y, hy, z, rfl⟩
[GOAL]
case mp.refine'_4.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a✝ : Set N
h : x ∈ Submodule.span S a✝
a : S
y : N
hy : y ∈ Submodule.span R a✝
z : { x // x ∈ M }
⊢ ∃ y_1, y_1 ∈ Submodule.span R a✝ ∧ ∃ z_1, a • mk' S 1 z • y = mk' S 1 z_1 • y_1
[PROOFSTEP]
obtain ⟨y', z', rfl⟩ := mk'_surjective M a
[GOAL]
case mp.refine'_4.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : R
z' : { x // x ∈ M }
⊢ ∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z_1, mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1
[PROOFSTEP]
refine' ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, _⟩
[GOAL]
case mp.refine'_4.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : R
z' : { x // x ∈ M }
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul, mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul]
[GOAL]
case mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) → x ∈ Submodule.span S a
[PROOFSTEP]
rintro ⟨y, hy, z, rfl⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
a : Set N
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
⊢ mk' S 1 z • y ∈ Submodule.span S a
[PROOFSTEP]
exact Submodule.smul_mem _ _ (Submodule.span_subset_span R S _ hy)
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ x ∈ Ideal.span (↑(algebraMap R S) '' a) ↔ ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
refine' (mem_span_iff M).trans _
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y) ↔
    ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y) →
    ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
rw [← coeSubmodule_span]
[GOAL]
case mp
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ coeSubmodule S (Ideal.span a) ∧ ∃ z, x = mk' S 1 z • y) → ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
rintro ⟨_, ⟨y, hy, rfl⟩, z, hz⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : { x // x ∈ M }
hz : x = mk' S 1 z • ↑(Algebra.linearMap R S) y
⊢ ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
refine' ⟨y, hy, z, _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : { x // x ∈ M }
hz : x = mk' S 1 z • ↑(Algebra.linearMap R S) y
⊢ x = mk' S y z
[PROOFSTEP]
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
[GOAL]
case mpr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z) →
    ∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
rintro ⟨y, hy, z, hz⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : { x // x ∈ M }
hz : x = mk' S y z
⊢ ∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
refine' ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, _⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : { x // x ∈ M }
hz : x = mk' S y z
⊢ x = mk' S 1 z • ↑(algebraMap R S) y
[PROOFSTEP]
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
