-- Mathlib/RingTheory/Localization/Ideal.lean
lemma _root_.NoZeroSMulDivisors_of_isLocalization (Rₚ Sₚ : Type*) [CommRing Rₚ] [CommRing Sₚ]
    [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ]
    [IsScalarTower R Rₚ Sₚ] {M : Submonoid R} (hM : M ≤ R⁰) [IsLocalization M Rₚ]
    [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [NoZeroSMulDivisors R S] [IsDomain S] :
    NoZeroSMulDivisors Rₚ Sₚ

Proof state:
case h
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)

Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ NoZeroSMulDivisors Rₚ Sₚ

Tactic:
rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
  RingHom.ker_eq_bot_iff_eq_zero]

Result:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
simp only [← _root_.map_mul,
  (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : ∃ a ∈ Algebra.algebraMapSubmonoid S M, a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

Proof state:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

Tactic:
intro x hx

Result:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0