R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type ?u.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ (∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x) ↔
    ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ x ∈ localizationLocalizationSubmodule M N ↔ ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z
rw [localizationLocalizationSubmodule, Submonoid.mem_comap, Submonoid.mem_sup]
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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ (∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x) →
    ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ (∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z) →
    ∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type ?u.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ (∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x) ↔
    ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z
constructor
case mp.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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ ↑M
e : y * ↑(algebraMap R S) z = ↑(algebraMap R S) x
⊢ ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ (∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x) →
    ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z
rintro ⟨y, hy, _, ⟨z, hz, rfl⟩, e⟩
no goals
case mp.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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ ↑M
e : y * ↑(algebraMap R S) z = ↑(algebraMap R S) x
⊢ ∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z
exact ⟨⟨y, hy⟩, ⟨z, hz⟩, e.symm⟩
case mpr.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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : { x // x ∈ N }
z : { x // x ∈ M }
e : ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z
⊢ ∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x
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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
⊢ (∃ y z, ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z) →
    ∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x
rintro ⟨y, z, e⟩
no goals
case mpr.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.8605
inst✝⁴ : CommRing P
N : Submonoid S
T : Type ?u.8769
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : { x // x ∈ N }
z : { x // x ∈ M }
e : ↑(algebraMap R S) x = ↑y * ↑(algebraMap R S) ↑z
⊢ ∃ y, y ∈ N ∧ ∃ z, z ∈ Submonoid.map (algebraMap R S) M ∧ y * z = ↑(algebraMap R S) x
exact ⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.symm⟩