R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
⊢ z = 0 ∨ w = 0
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
⊢ ∀ {a b : S}, a * b = 0 → a = 0 ∨ b = 0
intro z w h
case intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
⊢ z = 0 ∨ w = 0
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
⊢ z = 0 ∨ w = 0
cases' surj M z with x hx
case intro.intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
⊢ z = 0 ∨ w = 0
case intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
⊢ z = 0 ∨ w = 0
cases' surj M w with y hy
case intro.intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : z * w * ↑(algebraMap A S) ↑y.snd * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst * ↑(algebraMap A S) y.fst
⊢ z = 0 ∨ w = 0
case intro.intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
⊢ z = 0 ∨ w = 0
have :
  z * w * algebraMap A S y.2 * algebraMap A S x.2 = algebraMap A S x.1 * algebraMap A S y.1 :=
  by rw [mul_assoc z, hy, ← hx]; ring
case intro.intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : 0 = ↑(algebraMap A S) (x.fst * y.fst)
⊢ z = 0 ∨ w = 0
case intro.intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : z * w * ↑(algebraMap A S) ↑y.snd * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst * ↑(algebraMap A S) y.fst
⊢ z = 0 ∨ w = 0
rw [h, zero_mul, zero_mul, ← (algebraMap A S).map_mul] at this
case intro.intro.inl
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : 0 = ↑(algebraMap A S) (x.fst * y.fst)
H : x.fst = 0
⊢ z = 0 ∨ w = 0

case intro.intro.inr
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : 0 = ↑(algebraMap A S) (x.fst * y.fst)
H : y.fst = 0
⊢ z = 0 ∨ w = 0
case intro.intro
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : 0 = ↑(algebraMap A S) (x.fst * y.fst)
⊢ z = 0 ∨ w = 0
cases' eq_zero_or_eq_zero_of_mul_eq_zero ((to_map_eq_zero_iff S hM).mp this.symm) with H H
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
⊢ z * ↑(algebraMap A S) y.fst * ↑(algebraMap A S) ↑x.snd = z * ↑(algebraMap A S) ↑x.snd * ↑(algebraMap A S) y.fst
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
⊢ z * w * ↑(algebraMap A S) ↑y.snd * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst * ↑(algebraMap A S) y.fst
rw [mul_assoc z, hy, ← hx]
no goals
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
⊢ z * ↑(algebraMap A S) y.fst * ↑(algebraMap A S) ↑x.snd = z * ↑(algebraMap A S) ↑x.snd * ↑(algebraMap A S) y.fst
ring
no goals
case intro.intro.inl
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : 0 = ↑(algebraMap A S) (x.fst * y.fst)
H : x.fst = 0
⊢ z = 0 ∨ w = 0
exact Or.inl (eq_zero_of_fst_eq_zero hx H)
no goals
case intro.intro.inr
R : Type ?u.3107598
inst✝¹⁰ : CommRing R
M✝ : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type ?u.3108027
inst✝⁷ : CommRing P
K : Type ?u.3108033
inst✝⁶ : IsLocalization M✝ S
Q : Type ?u.3108214
inst✝⁵ : CommRing Q
g : R →+* P
inst✝⁴ : Algebra P Q
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra A S
M : Submonoid A
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors A
z w : S
h : z * w = 0
x : A × { x // x ∈ M }
hx : z * ↑(algebraMap A S) ↑x.snd = ↑(algebraMap A S) x.fst
y : A × { x // x ∈ M }
hy : w * ↑(algebraMap A S) ↑y.snd = ↑(algebraMap A S) y.fst
this : 0 = ↑(algebraMap A S) (x.fst * y.fst)
H : y.fst = 0
⊢ z = 0 ∨ w = 0
exact Or.inr (eq_zero_of_fst_eq_zero hy H)