-- Mathlib/RingTheory/Localization/Defs.lean
theorem nonZeroDivisors_le_comap [IsLocalization M S] :
    nonZeroDivisors R ≤ (nonZeroDivisors S).comap (algebraMap R S)

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s c : ↥M
e : ↑c * x * a = 0
⊢ mk' S x s = 0

Tactic:
rw [mk'_eq_zero_iff]

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s c : ↥M
e : ↑c * x * a = 0
⊢ ∃ m, ↑m * x = 0

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s c : ↥M
e : ↑c * x * a = 0
⊢ ∃ m, ↑m * x = 0

Tactic:
exact ⟨c, ha _ e⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s : ↥M
e : mk' S x s * (algebraMap R S) a = 0
⊢ mk' S x s = 0

Tactic:
rw [← @mk'_one R _ M, ← mk'_mul, ← (algebraMap R S).map_zero, ← @mk'_one R _ M,
  IsLocalization.eq] at e

Result:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s : ↥M
e : ∃ c, ↑c * (↑1 * (x * a)) = ↑c * (↑(s * 1) * 0)
⊢ mk' S x s = 0

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s c : ↥M
e : ↑c * (↑1 * (x * a)) = ↑c * (↑(s * 1) * 0)
⊢ mk' S x s = 0

Tactic:
rw [mul_zero, mul_zero, Submonoid.coe_one, one_mul, ← mul_assoc] at e

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s c : ↥M
e : ↑c * x * a = 0
⊢ mk' S x s = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ nonZeroDivisors R ≤ Submonoid.comap (algebraMap R S) (nonZeroDivisors S)

Tactic:
rintro a ha b (e : b * algebraMap R S a = 0)

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
b : S
e : b * (algebraMap R S) a = 0
⊢ b = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
b : S
e : b * (algebraMap R S) a = 0
⊢ b = 0

Tactic:
obtain ⟨x, s, rfl⟩ := mk'_surjective M b

Result:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s : ↥M
e : mk' S x s * (algebraMap R S) a = 0
⊢ mk' S x s = 0

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s : ↥M
e : ∃ c, ↑c * (↑1 * (x * a)) = ↑c * (↑(s * 1) * 0)
⊢ mk' S x s = 0

Tactic:
obtain ⟨c, e⟩ := e

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : R
ha : a ∈ nonZeroDivisors R
x : R
s c : ↥M
e : ↑c * (↑1 * (x * a)) = ↑c * (↑(s * 1) * 0)
⊢ mk' S x s = 0