R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
have := isLocalization_of_submonoid_le S T M (nonZeroDivisors R) hM
case refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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

case refine_2
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_
no goals
case refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
exact map_nonZeroDivisors_le M S
case refine_2.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
case refine_2
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
rintro ⟨x, hx⟩
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
case refine_2.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M x
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
use algebraMap R S s
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
rw [mul_comm, Subtype.coe_mk, e]
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
refine' Set.mem_image_of_mem (algebraMap R S) _
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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)
intro z hz
case refine_2.mk.intro.mk.a
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
case refine_2.mk.intro.mk
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
apply IsLocalization.injective S hM
case refine_2.mk.intro.mk.a
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
case refine_2.mk.intro.mk.a
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
rw [map_zero]
case refine_2.mk.intro.mk.a.a
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
case refine_2.mk.intro.mk.a
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
apply hx
no goals
case refine_2.mk.intro.mk.a.a
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S✝ : Type ?u.661559
inst✝¹⁰ : CommRing S✝
inst✝⁹ : Algebra R S✝
P : Type ?u.661815
inst✝⁸ : CommRing P
S : Type u_1
T : Type u_2
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
rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
  MulZeroClass.zero_mul]