[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
N : Submonoid S
T : Type u_4
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
[PROOFSTEP]
rw [localizationLocalizationSubmodule, Submonoid.mem_comap, Submonoid.mem_sup]
[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
N : Submonoid S
T : Type u_4
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
[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
N : Submonoid S
T : Type u_4
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
[PROOFSTEP]
rintro ⟨y, hy, _, ⟨z, hz, rfl⟩, e⟩
[GOAL]
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_3
inst✝⁴ : CommRing P
N : Submonoid S
T : Type u_4
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
[PROOFSTEP]
exact ⟨⟨y, hy⟩, ⟨z, hz⟩, e.symm⟩
[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
N : Submonoid S
T : Type u_4
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
[PROOFSTEP]
rintro ⟨y, z, e⟩
[GOAL]
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_3
inst✝⁴ : CommRing P
N : Submonoid S
T : Type u_4
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
[PROOFSTEP]
exact ⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.symm⟩
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
⊢ IsUnit (↑(algebraMap R T) ↑y)
[PROOFSTEP]
obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop
[GOAL]
case 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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
y' : { x // x ∈ N }
z : { x // x ∈ M }
eq : ↑(algebraMap R S) ↑y = ↑y' * ↑(algebraMap R S) ↑z
⊢ IsUnit (↑(algebraMap R T) ↑y)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply R S T, eq, RingHom.map_mul, IsUnit.mul_iff]
[GOAL]
case 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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
y' : { x // x ∈ N }
z : { x // x ∈ M }
eq : ↑(algebraMap R S) ↑y = ↑y' * ↑(algebraMap R S) ↑z
⊢ IsUnit (↑(algebraMap S T) ↑y') ∧ IsUnit (↑(algebraMap S T) (↑(algebraMap R S) ↑z))
[PROOFSTEP]
exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
⊢ ∃ y, x * ↑(algebraMap R T) ↑y.snd = ↑(algebraMap R T) y.fst
[PROOFSTEP]
rcases IsLocalization.surj N x with
  ⟨⟨y, s⟩, eq₁⟩
    -- x = y / s
[GOAL]
case intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑(y, s).snd = ↑(algebraMap S T) (y, s).fst
⊢ ∃ y, x * ↑(algebraMap R T) ↑y.snd = ↑(algebraMap R T) y.fst
[PROOFSTEP]
rcases IsLocalization.surj M y with
  ⟨⟨z, t⟩, eq₂⟩
    -- y = z / t
[GOAL]
case intro.mk.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑(y, s).snd = ↑(algebraMap S T) (y, s).fst
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑(z, t).snd = ↑(algebraMap R S) (z, t).fst
⊢ ∃ y, x * ↑(algebraMap R T) ↑y.snd = ↑(algebraMap R T) y.fst
[PROOFSTEP]
rcases IsLocalization.surj M (s : S) with
  ⟨⟨z', t'⟩, eq₃⟩
    -- s = z' / t'
[GOAL]
case intro.mk.intro.mk.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑(y, s).snd = ↑(algebraMap S T) (y, s).fst
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑(z, t).snd = ↑(algebraMap R S) (z, t).fst
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑(z', t').snd = ↑(algebraMap R S) (z', t').fst
⊢ ∃ y, x * ↑(algebraMap R T) ↑y.snd = ↑(algebraMap R T) y.fst
[PROOFSTEP]
dsimp only at eq₁ eq₂ eq₃
[GOAL]
case intro.mk.intro.mk.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑s = ↑(algebraMap S T) y
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑t = ↑(algebraMap R S) z
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑t' = ↑(algebraMap R S) z'
⊢ ∃ y, x * ↑(algebraMap R T) ↑y.snd = ↑(algebraMap R T) y.fst
[PROOFSTEP]
refine
  ⟨⟨z * t', z' * t, ?_⟩, ?_⟩
    -- x = y / s = (z * t') / (z' * t)
[GOAL]
case intro.mk.intro.mk.intro.mk.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑s = ↑(algebraMap S T) y
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑t = ↑(algebraMap R S) z
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑t' = ↑(algebraMap R S) z'
⊢ z' * ↑t ∈ localizationLocalizationSubmodule M N
[PROOFSTEP]
rw [mem_localizationLocalizationSubmodule]
[GOAL]
case intro.mk.intro.mk.intro.mk.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑s = ↑(algebraMap S T) y
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑t = ↑(algebraMap R S) z
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑t' = ↑(algebraMap R S) z'
⊢ ∃ y z, ↑(algebraMap R S) (z' * ↑t) = ↑y * ↑(algebraMap R S) ↑z
[PROOFSTEP]
refine' ⟨s, t * t', _⟩
[GOAL]
case intro.mk.intro.mk.intro.mk.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑s = ↑(algebraMap S T) y
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑t = ↑(algebraMap R S) z
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑t' = ↑(algebraMap R S) z'
⊢ ↑(algebraMap R S) (z' * ↑t) = ↑s * ↑(algebraMap R S) ↑(t * t')
[PROOFSTEP]
rw [RingHom.map_mul, ← eq₃, mul_assoc, ← RingHom.map_mul, mul_comm t, Submonoid.coe_mul]
[GOAL]
case intro.mk.intro.mk.intro.mk.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑s = ↑(algebraMap S T) y
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑t = ↑(algebraMap R S) z
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑t' = ↑(algebraMap R S) z'
⊢ x *
      ↑(algebraMap R T)
        ↑(z * ↑t', { val := z' * ↑t, property := (_ : z' * ↑t ∈ localizationLocalizationSubmodule M N) }).snd =
    ↑(algebraMap R T)
      (z * ↑t', { val := z' * ↑t, property := (_ : z' * ↑t ∈ localizationLocalizationSubmodule M N) }).fst
[PROOFSTEP]
simp only [Subtype.coe_mk, RingHom.map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]
[GOAL]
case intro.mk.intro.mk.intro.mk.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : { x // x ∈ N }
eq₁ : x * ↑(algebraMap S T) ↑s = ↑(algebraMap S T) y
z : R
t : { x // x ∈ M }
eq₂ : y * ↑(algebraMap R S) ↑t = ↑(algebraMap R S) z
z' : R
t' : { x // x ∈ M }
eq₃ : ↑s * ↑(algebraMap R S) ↑t' = ↑(algebraMap R S) z'
⊢ x * (↑(algebraMap S T) ↑s * ↑(algebraMap S T) (↑(algebraMap R S) ↑t') * ↑(algebraMap S T) (↑(algebraMap R S) ↑t)) =
    x * ↑(algebraMap S T) ↑s * ↑(algebraMap S T) (↑(algebraMap R S) ↑t) * ↑(algebraMap S T) (↑(algebraMap R S) ↑t')
[PROOFSTEP]
ring
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ ↑(algebraMap R T) x = ↑(algebraMap R T) y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply R S T, IsScalarTower.algebraMap_apply R S T, IsLocalization.eq_iff_exists N T]
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y) ↔ ∃ c, ↑c * x = ↑c * 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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y) → ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rintro ⟨z, eq₁⟩
[GOAL]
case mp.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
⊢ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rcases IsLocalization.surj M (z : S) with ⟨⟨z', s⟩, eq₂⟩
[GOAL]
case mp.intro.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑(z', s).snd = ↑(algebraMap R S) (z', s).fst
⊢ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
dsimp only at eq₂
[GOAL]
case mp.intro.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
⊢ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
suffices : (algebraMap R S) (x * z' : R) = (algebraMap R S) (y * z')
[GOAL]
case mp.intro.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
⊢ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
obtain ⟨c, eq₃ : ↑c * (x * z') = ↑c * (y * z')⟩ := (IsLocalization.eq_iff_exists M S).mp this
[GOAL]
case mp.intro.intro.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
refine ⟨⟨c * z', ?_⟩, ?_⟩
[GOAL]
case mp.intro.intro.mk.intro.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑c * z' ∈ localizationLocalizationSubmodule M N
[PROOFSTEP]
rw [mem_localizationLocalizationSubmodule]
[GOAL]
case mp.intro.intro.mk.intro.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ y z, ↑(algebraMap R S) (↑c * z') = ↑y * ↑(algebraMap R S) ↑z
[PROOFSTEP]
refine ⟨z, c * s, ?_⟩
[GOAL]
case mp.intro.intro.mk.intro.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑(algebraMap R S) (↑c * z') = ↑z * ↑(algebraMap R S) ↑(c * s)
[PROOFSTEP]
rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
[GOAL]
case mp.intro.intro.mk.intro.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑{ val := ↑c * z', property := (_ : ↑c * z' ∈ localizationLocalizationSubmodule M N) } * x =
    ↑{ val := ↑c * z', property := (_ : ↑c * z' ∈ localizationLocalizationSubmodule M N) } * y
[PROOFSTEP]
rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
[GOAL]
case this
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
⊢ ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
[PROOFSTEP]
rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁, mul_comm _ (z : S)]
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
[PROOFSTEP]
rintro ⟨⟨c, hc⟩, eq₁ : c * x = c * y⟩
[GOAL]
case mpr.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
hc : c ∈ localizationLocalizationSubmodule M N
eq₁ : c * x = c * y
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
[PROOFSTEP]
rw [mem_localizationLocalizationSubmodule] at hc
[GOAL]
case mpr.intro.mk
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
hc : ∃ y z, ↑(algebraMap R S) c = ↑y * ↑(algebraMap R S) ↑z
eq₁ : c * x = c * y
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
[PROOFSTEP]
rcases hc with ⟨z₁, z, eq₂⟩
[GOAL]
case mpr.intro.mk.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
[PROOFSTEP]
use z₁
[GOAL]
case h
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ↑z₁ * ↑(algebraMap R S) x = ↑z₁ * ↑(algebraMap R S) y
[PROOFSTEP]
refine (IsLocalization.map_units S z).mul_right_inj.mp ?_
[GOAL]
case h
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ↑(algebraMap R S) ↑z * (↑z₁ * ↑(algebraMap R S) x) = ↑(algebraMap R S) ↑z * (↑z₁ * ↑(algebraMap R S) y)
[PROOFSTEP]
rw [← mul_assoc, mul_comm _ (z₁ : S), ← eq₂, ← map_mul, eq₁, map_mul, eq₂, ← mul_assoc, mul_comm _ (z₁ : S)]
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ IsLocalization (Submonoid.comap (algebraMap R S) N) T
[PROOFSTEP]
convert localization_localization_isLocalization M N T using 1
[GOAL]
case h.e'_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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = localizationLocalizationSubmodule M N
[PROOFSTEP]
dsimp [localizationLocalizationSubmodule]
[GOAL]
case h.e'_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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e_S
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N = N ⊔ Submonoid.map (algebraMap R S) M
[PROOFSTEP]
symm
[GOAL]
case h.e'_3.e_S
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N ⊔ Submonoid.map (algebraMap R S) M = N
[PROOFSTEP]
rw [sup_eq_left]
[GOAL]
case h.e'_3.e_S
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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.map (algebraMap R S) M ≤ N
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case h.e'_3.e_S.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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
x : R
hx : x ∈ ↑M
⊢ ↑(algebraMap R S) x ∈ N
[PROOFSTEP]
exact H _ (IsLocalization.map_units _ ⟨x, hx⟩)
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
⊢ IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)
[PROOFSTEP]
apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ Ideal.primeCompl p
[PROOFSTEP]
intro x hx hx'
[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
N : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ ↑p
⊢ False
[PROOFSTEP]
exact (Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)
[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
N : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
x : Ideal R
H : Ideal.IsPrime x
inst✝ : IsDomain R
⊢ Ideal.primeCompl x ≤ nonZeroDivisors R
[PROOFSTEP]
intro a ha
[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
N : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
x : Ideal R
H : Ideal.IsPrime x
inst✝ : IsDomain R
a : R
ha : a ∈ Ideal.primeCompl x
⊢ a ∈ nonZeroDivisors R
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff_ne_zero]
[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
N : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
x : Ideal R
H : Ideal.IsPrime x
inst✝ : IsDomain R
a : R
ha : a ∈ Ideal.primeCompl x
⊢ a ≠ 0
[PROOFSTEP]
exact fun h => ha (h.symm ▸ x.zero_mem)
[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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
⊢ ∀ (y : { x // x ∈ Submonoid.map (algebraMap R S) N }), IsUnit (↑(algebraMap S T) ↑y)
[PROOFSTEP]
rintro ⟨_, ⟨y, hy, rfl⟩⟩
[GOAL]
case mk.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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ IsUnit
    (↑(algebraMap S T)
      ↑{ val := ↑(algebraMap R S) y, property := (_ : ∃ a, a ∈ ↑N ∧ ↑(algebraMap R S) a = ↑(algebraMap R S) y) })
[PROOFSTEP]
convert IsLocalization.map_units T ⟨y, hy⟩
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ ↑(algebraMap S T)
      ↑{ val := ↑(algebraMap R S) y, property := (_ : ∃ a, a ∈ ↑N ∧ ↑(algebraMap R S) a = ↑(algebraMap R S) y) } =
    ↑(algebraMap R T) ↑{ val := y, property := hy }
[PROOFSTEP]
exact (IsScalarTower.algebraMap_apply _ _ _ _).symm
[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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : T
⊢ ∃ x, y * ↑(algebraMap S T) ↑x.snd = ↑(algebraMap S T) x.fst
[PROOFSTEP]
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj N y
[GOAL]
case intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : T
x : R
s : { x // x ∈ N }
e : y * ↑(algebraMap R T) ↑(x, s).snd = ↑(algebraMap R T) (x, s).fst
⊢ ∃ x, y * ↑(algebraMap S T) ↑x.snd = ↑(algebraMap S T) x.fst
[PROOFSTEP]
refine ⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩
[GOAL]
case intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : T
x : R
s : { x // x ∈ N }
e : y * ↑(algebraMap R T) ↑(x, s).snd = ↑(algebraMap R T) (x, s).fst
⊢ y *
      ↑(algebraMap S T)
        ↑(↑(algebraMap R S) x,
              { val := ↑(algebraMap R S) ↑s,
                property := (_ : ∃ a, a ∈ ↑N ∧ ↑(algebraMap R S) a = ↑(algebraMap R S) ↑s) }).snd =
    ↑(algebraMap S T)
      (↑(algebraMap R S) x,
          { val := ↑(algebraMap R S) ↑s,
            property := (_ : ∃ a, a ∈ ↑N ∧ ↑(algebraMap R S) a = ↑(algebraMap R S) ↑s) }).fst
[PROOFSTEP]
simpa [← IsScalarTower.algebraMap_apply] using e
[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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ c, ↑c * x₁ = ↑c * x₂
[PROOFSTEP]
obtain ⟨⟨y₁, s₁⟩, e₁⟩ := IsLocalization.surj M x₁
[GOAL]
case intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑(y₁, s₁).snd = ↑(algebraMap R S) (y₁, s₁).fst
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ c, ↑c * x₁ = ↑c * x₂
[PROOFSTEP]
obtain ⟨⟨y₂, s₂⟩, e₂⟩ := IsLocalization.surj M x₂
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑(y₁, s₁).snd = ↑(algebraMap R S) (y₁, s₁).fst
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑(y₂, s₂).snd = ↑(algebraMap R S) (y₂, s₂).fst
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ c, ↑c * x₁ = ↑c * x₂
[PROOFSTEP]
refine' Iff.trans _ (Set.exists_image_iff (algebraMap R S) N fun c => c * x₁ = c * x₂).symm
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑(y₁, s₁).snd = ↑(algebraMap R S) (y₁, s₁).fst
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑(y₂, s₂).snd = ↑(algebraMap R S) (y₂, s₂).fst
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
dsimp only at e₁ e₂ ⊢
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
suffices :
  algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) ↔
    ∃ a : N, algebraMap R S (a * (y₁ * s₂)) = algebraMap R S (a * (y₂ * s₁))
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
this :
  ↑(algebraMap R T) (y₁ * ↑s₂) = ↑(algebraMap R T) (y₂ * ↑s₁) ↔
    ∃ a, ↑(algebraMap R S) (↑a * (y₁ * ↑s₂)) = ↑(algebraMap R S) (↑a * (y₂ * ↑s₁))
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
have h₁ :=
  @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂) (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
this :
  ↑(algebraMap R T) (y₁ * ↑s₂) = ↑(algebraMap R T) (y₂ * ↑s₁) ↔
    ∃ a, ↑(algebraMap R S) (↑a * (y₁ * ↑s₂)) = ↑(algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap R T) ↑{ val := ↑s₁, property := (_ : ↑s₁ ∈ N) } =
      ↑(algebraMap S T) x₂ * ↑(algebraMap R T) ↑{ val := ↑s₁, property := (_ : ↑s₁ ∈ N) } ↔
    ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
have h₂ :=
  @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁)) ((algebraMap S T x₂) * (algebraMap R T s₁))
    (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
this :
  ↑(algebraMap R T) (y₁ * ↑s₂) = ↑(algebraMap R T) (y₂ * ↑s₁) ↔
    ∃ a, ↑(algebraMap R S) (↑a * (y₁ * ↑s₂)) = ↑(algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap R T) ↑{ val := ↑s₁, property := (_ : ↑s₁ ∈ N) } =
      ↑(algebraMap S T) x₂ * ↑(algebraMap R T) ↑{ val := ↑s₁, property := (_ : ↑s₁ ∈ N) } ↔
    ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂
h₂ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap R T) ↑s₁ * ↑(algebraMap R T) ↑{ val := ↑s₂, property := (_ : ↑s₂ ∈ N) } =
      ↑(algebraMap S T) x₂ * ↑(algebraMap R T) ↑s₁ * ↑(algebraMap R T) ↑{ val := ↑s₂, property := (_ : ↑s₂ ∈ N) } ↔
    ↑(algebraMap S T) x₁ * ↑(algebraMap R T) ↑s₁ = ↑(algebraMap S T) x₂ * ↑(algebraMap R T) ↑s₁
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
simp only [IsScalarTower.algebraMap_apply R S T, Subtype.coe_mk] at h₁ h₂
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
this :
  ↑(algebraMap R T) (y₁ * ↑s₂) = ↑(algebraMap R T) (y₂ * ↑s₁) ↔
    ∃ a, ↑(algebraMap R S) (↑a * (y₁ * ↑s₂)) = ↑(algebraMap R S) (↑a * (y₂ * ↑s₁))
h₁ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) ↔
    ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂
h₂ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) ↔
    ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁)
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc, mul_right_comm _ (algebraMap R S s₂),
  mul_right_comm _ (algebraMap S T (algebraMap R S s₂)), (IsLocalization.map_units S s₁).mul_left_inj,
  (IsLocalization.map_units S s₂).mul_left_inj] at this
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
h₁ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) ↔
    ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂
h₂ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) ↔
    ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁)
this :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) ↔
    ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
rw [h₂, h₁] at this
[GOAL]
case intro.mk.intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
h₁ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) ↔
    ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂
h₂ :
  ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₂) ↔
    ↑(algebraMap S T) x₁ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁) =
      ↑(algebraMap S T) x₂ * ↑(algebraMap S T) (↑(algebraMap R S) ↑s₁)
this : ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
⊢ ↑(algebraMap S T) x₁ = ↑(algebraMap S T) x₂ ↔ ∃ a, ↑(algebraMap R S) ↑a * x₁ = ↑(algebraMap R S) ↑a * x₂
[PROOFSTEP]
simpa only [mul_comm] using this
[GOAL]
case this
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
⊢ ↑(algebraMap R T) (y₁ * ↑s₂) = ↑(algebraMap R T) (y₂ * ↑s₁) ↔
    ∃ a, ↑(algebraMap R S) (↑a * (y₁ * ↑s₂)) = ↑(algebraMap R S) (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
simp_rw [IsLocalization.eq_iff_exists N T, IsLocalization.eq_iff_exists M S]
[GOAL]
case this
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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
⊢ (∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)) ↔ ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
constructor
[GOAL]
case this.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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
⊢ (∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)) → ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
rintro ⟨a, e⟩
[GOAL]
case this.mp.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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
exact ⟨a, 1, by convert e using 1 <;> simp⟩
[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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑1 * (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
convert e using 1
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑a * (y₁ * ↑s₂)
[PROOFSTEP]
simp
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₂ * ↑s₁)) = ↑a * (y₂ * ↑s₁)
[PROOFSTEP]
simp
[GOAL]
case this.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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
⊢ (∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))) → ∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)
[PROOFSTEP]
rintro ⟨a, b, e⟩
[GOAL]
case this.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_3
inst✝⁶ : CommRing P
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
b : { x // x ∈ M }
e : ↑b * (↑a * (y₁ * ↑s₂)) = ↑b * (↑a * (y₂ * ↑s₁))
⊢ ∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)
[PROOFSTEP]
exact ⟨a * (⟨_, h b.prop⟩ : N), by convert e using 1 <;> simp <;> ring⟩
[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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
b : { x // x ∈ M }
e : ↑b * (↑a * (y₁ * ↑s₂)) = ↑b * (↑a * (y₂ * ↑s₁))
⊢ ↑(a * { val := ↑b, property := (_ : ↑b ∈ N) }) * (y₁ * ↑s₂) =
    ↑(a * { val := ↑b, property := (_ : ↑b ∈ N) }) * (y₂ * ↑s₁)
[PROOFSTEP]
convert e using 1
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
b : { x // x ∈ M }
e : ↑b * (↑a * (y₁ * ↑s₂)) = ↑b * (↑a * (y₂ * ↑s₁))
⊢ ↑(a * { val := ↑b, property := (_ : ↑b ∈ N) }) * (y₁ * ↑s₂) = ↑b * (↑a * (y₁ * ↑s₂))
[PROOFSTEP]
simp
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
b : { x // x ∈ M }
e : ↑b * (↑a * (y₁ * ↑s₂)) = ↑b * (↑a * (y₂ * ↑s₁))
⊢ ↑(a * { val := ↑b, property := (_ : ↑b ∈ N) }) * (y₂ * ↑s₁) = ↑b * (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
simp
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
b : { x // x ∈ M }
e : ↑b * (↑a * (y₁ * ↑s₂)) = ↑b * (↑a * (y₂ * ↑s₁))
⊢ ↑a * ↑b * (y₁ * ↑s₂) = ↑b * (↑a * (y₁ * ↑s₂))
[PROOFSTEP]
ring
[GOAL]
case h.e'_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
N✝ : Submonoid S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : { x // x ∈ M }
e₁ : x₁ * ↑(algebraMap R S) ↑s₁ = ↑(algebraMap R S) y₁
y₂ : R
s₂ : { x // x ∈ M }
e₂ : x₂ * ↑(algebraMap R S) ↑s₂ = ↑(algebraMap R S) y₂
a : { x // x ∈ N }
b : { x // x ∈ M }
e : ↑b * (↑a * (y₁ * ↑s₂)) = ↑b * (↑a * (y₂ * ↑s₁))
⊢ ↑a * ↑b * (y₂ * ↑s₁) = ↑b * (↑a * (y₂ * ↑s₁))
[PROOFSTEP]
ring
[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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
⊢ IsUnit (↑(algebraMap R S) ↑y)
[PROOFSTEP]
obtain ⟨m, hm⟩ := h' y
[GOAL]
case 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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
⊢ IsUnit (↑(algebraMap R S) ↑y)
[PROOFSTEP]
have := IsLocalization.map_units S ⟨_, hm⟩
[GOAL]
case 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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
this : IsUnit (↑(algebraMap R S) ↑{ val := m * ↑y, property := hm })
⊢ IsUnit (↑(algebraMap R S) ↑y)
[PROOFSTEP]
erw [map_mul] at this
[GOAL]
case 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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
y : { x // x ∈ N }
m : R
hm : m * ↑y ∈ M
this : IsUnit (↑(algebraMap R S) m * ↑(algebraMap R S) ↑y)
⊢ IsUnit (↑(algebraMap R S) ↑y)
[PROOFSTEP]
exact (IsUnit.mul_iff.mp this).2
[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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
z : S
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
[PROOFSTEP]
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M z
[GOAL]
case intro.mk
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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
z : S
y : R
s : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ ∃ x, z * ↑(algebraMap R S) ↑x.snd = ↑(algebraMap R S) x.fst
[PROOFSTEP]
exact ⟨⟨y, _, h s.prop⟩, e⟩
[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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ ↑(algebraMap R S) x✝¹ = ↑(algebraMap R S) x✝ ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝
[PROOFSTEP]
rw [IsLocalization.eq_iff_exists M]
[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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) ↔ ∃ c, ↑c * x✝¹ = ↑c * x✝
[PROOFSTEP]
refine ⟨fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩, ?_⟩
[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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝
[PROOFSTEP]
rintro ⟨x, h⟩
[GOAL]
case 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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
⊢ ∃ c, ↑c * x✝¹ = ↑c * x✝
[PROOFSTEP]
obtain ⟨m, hm⟩ := h' x
[GOAL]
case 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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
m : R
hm : m * ↑x ∈ M
⊢ ∃ c, ↑c * x✝¹ = ↑c * x✝
[PROOFSTEP]
refine ⟨⟨_, hm⟩, ?_⟩
[GOAL]
case 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
N✝ : Submonoid S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
M N : Submonoid R
inst✝ : IsLocalization M S
h✝ : M ≤ N
h' : ∀ (x : { x // x ∈ N }), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
x : { x // x ∈ N }
h : ↑x * x✝¹ = ↑x * x✝
m : R
hm : m * ↑x ∈ M
⊢ ↑{ val := m * ↑x, property := hm } * x✝¹ = ↑{ val := m * ↑x, property := hm } * x✝
[PROOFSTEP]
simp [h, mul_assoc]
[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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
⊢ IsFractionRing S T
[PROOFSTEP]
have := isLocalization_of_submonoid_le S T M (nonZeroDivisors R) hM
[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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ IsFractionRing S T
[PROOFSTEP]
refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_
[GOAL]
case 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
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S
[PROOFSTEP]
exact map_nonZeroDivisors_le M S
[GOAL]
case 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
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ ∀ (x : { x // x ∈ nonZeroDivisors S }), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case refine_2.mk
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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
⊢ ∃ m, m * ↑{ val := x, property := hx } ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
[PROOFSTEP]
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M x
[GOAL]
case refine_2.mk.intro.mk
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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ ∃ m, m * ↑{ val := x, property := hx } ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
[PROOFSTEP]
use algebraMap R S s
[GOAL]
case h
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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ ↑(algebraMap R S) ↑s * ↑{ val := x, property := hx } ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
[PROOFSTEP]
rw [mul_comm, Subtype.coe_mk, e]
[GOAL]
case h
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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ ↑(algebraMap R S) (y, s).fst ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
[PROOFSTEP]
refine' Set.mem_image_of_mem (algebraMap R S) _
[GOAL]
case h
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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
⊢ (y, s).fst ∈ ↑(nonZeroDivisors R)
[PROOFSTEP]
intro z hz
[GOAL]
case h
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 : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
z : R
hz : z * (y, s).fst = 0
⊢ z = 0
[PROOFSTEP]
apply IsLocalization.injective S hM
[GOAL]
case h.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
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
z : R
hz : z * (y, s).fst = 0
⊢ ↑(algebraMap R S) z = ↑(algebraMap R S) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case h.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
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
z : R
hz : z * (y, s).fst = 0
⊢ ↑(algebraMap R S) z = 0
[PROOFSTEP]
apply hx
[GOAL]
case h.a.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
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : { x // x ∈ M }
e : x * ↑(algebraMap R S) ↑(y, s).snd = ↑(algebraMap R S) (y, s).fst
z : R
hz : z * (y, s).fst = 0
⊢ ↑(algebraMap R S) z * x = 0
[PROOFSTEP]
rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero, zero_mul]
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
⊢ IsFractionRing S T
[PROOFSTEP]
haveI := IsFractionRing.nontrivial R T
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this : Nontrivial T
⊢ IsFractionRing S T
[PROOFSTEP]
haveI := (algebraMap S T).domain_nontrivial
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
⊢ IsFractionRing S T
[PROOFSTEP]
apply isFractionRing_of_isLocalization M S T
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
⊢ M ≤ nonZeroDivisors R
[PROOFSTEP]
intro x hx
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ∈ nonZeroDivisors R
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff_ne_zero]
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ≠ 0
[PROOFSTEP]
intro hx'
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ False
[PROOFSTEP]
apply @zero_ne_one S
[GOAL]
case 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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ 0 = 1
[PROOFSTEP]
rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]
[GOAL]
case 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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ∃ m, ↑m * 1 = 0
[PROOFSTEP]
exact ⟨⟨x, hx⟩, by simp [hx']⟩
[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
inst✝⁸ : IsDomain R
S : Type u_4
T : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ↑{ val := x, property := hx } * 1 = 0
[PROOFSTEP]
simp [hx']