-- Mathlib/RingTheory/Localization/Defs.lean
theorem noZeroDivisors_of_le_nonZeroDivisors [Algebra A S] {M : Submonoid A} [IsLocalization M S]
    (hM : M ≤ nonZeroDivisors A) : NoZeroDivisors S :=
  { eq_zero_or_eq_zero_of_mul_eq_zero

Proof state:
case intro.intro.inl
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : 0 = (algebraMap A S) (x.1 * y.1)
H : x.1 = 0
⊢ z = 0 ∨ w = 0

Tactic:
exact Or.inl (eq_zero_of_fst_eq_zero hx H)

Result:
no goals

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
⊢ z * w * (algebraMap A S) ↑y.2 * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1 * (algebraMap A S) y.1

Tactic:
rw [mul_assoc z, hy, ← hx]

Result:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
⊢ z * (algebraMap A S) y.1 * (algebraMap A S) ↑x.2 = z * (algebraMap A S) ↑x.2 * (algebraMap A S) y.1

Proof state:
case intro.intro.inr
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : 0 = (algebraMap A S) (x.1 * y.1)
H : y.1 = 0
⊢ z = 0 ∨ w = 0

Tactic:
exact Or.inr (eq_zero_of_fst_eq_zero hy H)

Result:
no goals

Proof state:
case intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
⊢ z = 0 ∨ w = 0

Tactic:
obtain ⟨y, hy⟩ := surj M w

Result:
case intro.intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
⊢ z = 0 ∨ w = 0

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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

Tactic:
obtain ⟨x, hx⟩ := surj M z

Result:
case intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
⊢ z = 0 ∨ w = 0

Proof state:
case intro.intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : z * w * (algebraMap A S) ↑y.2 * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1 * (algebraMap A S) y.1
⊢ z = 0 ∨ w = 0

Tactic:
rw [h, zero_mul, zero_mul, ← (algebraMap A S).map_mul] at this

Result:
case intro.intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : 0 = (algebraMap A S) (x.1 * y.1)
⊢ z = 0 ∨ w = 0

Proof state:
case intro.intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
⊢ z = 0 ∨ w = 0

Tactic:
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

Result:
case intro.intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : z * w * (algebraMap A S) ↑y.2 * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1 * (algebraMap A S) y.1
⊢ z = 0 ∨ w = 0

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
⊢ z * (algebraMap A S) y.1 * (algebraMap A S) ↑x.2 = z * (algebraMap A S) ↑x.2 * (algebraMap A S) y.1

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : 0 = (algebraMap A S) (x.1 * y.1)
⊢ z = 0 ∨ w = 0

Tactic:
rcases eq_zero_or_eq_zero_of_mul_eq_zero ((to_map_eq_zero_iff S hM).mp this.symm) with H | H

Result:
case intro.intro.inl
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : 0 = (algebraMap A S) (x.1 * y.1)
H : x.1 = 0
⊢ z = 0 ∨ w = 0

case intro.intro.inr
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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 × ↥M
hx : z * (algebraMap A S) ↑x.2 = (algebraMap A S) x.1
y : A × ↥M
hy : w * (algebraMap A S) ↑y.2 = (algebraMap A S) y.1
this : 0 = (algebraMap A S) (x.1 * y.1)
H : y.1 = 0
⊢ z = 0 ∨ w = 0

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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

Tactic:
intro z w h

Result:
S : Type u_2
inst✝⁴ : CommRing S
A : Type u_6
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