R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type ?u.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type ?u.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
refine' (mem_span_iff M).trans _
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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

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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type ?u.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
constructor
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
rw [← coeSubmodule_span]
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
rintro ⟨_, ⟨y, hy, rfl⟩, z, hz⟩
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
refine' ⟨y, hy, z, _⟩
no goals
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
rintro ⟨y, hy, z, hz⟩
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
refine' ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, _⟩
no goals
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.194470
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type ?u.195302
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
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]