Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain (FltRegular/NumberTheory/QuotientTrace.lean)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ : Type ?u.335608
Sₚ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ
inst✝¹⁵ : CommRing Sₚ
inst✝¹⁴ : Algebra R Rₚ
inst✝¹³ : IsLocalization.AtPrime Rₚ p
inst✝¹² : LocalRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra S Sₚ
inst✝⁹ : Algebra R Sₚ
inst✝⁸ : Algebra Rₚ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : IsScalarTower R S Sₚ
inst✝⁵ : IsScalarTower R Rₚ Sₚ
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
let Rₚ := Localization.AtPrime p
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra S Sₚ
inst✝⁹ : Algebra R Sₚ
inst✝⁸ : Algebra Rₚ✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : IsScalarTower R S Sₚ
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra S Sₚ
inst✝⁹ : Algebra R Sₚ
inst✝⁸ : Algebra Rₚ✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : IsScalarTower R S Sₚ
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
let Sₚ := Localization (Algebra.algebraMapSubmonoid S p.primeCompl)
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
letI : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsScalarTower R Rₚ Sₚ := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq])
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this : IsScalarTower R Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this : IsScalarTower R Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsLocalization (Submonoid.map (algebraMap R S) (Ideal.primeCompl p)) Sₚ :=
  inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ)
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝¹ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
this : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝¹ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
this : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
have e : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
  Submonoid.map_le_of_le_comap _ <| p.primeCompl_le_nonZeroDivisors.trans
    (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
      (NoZeroSMulDivisors.algebraMap_injective _ _))
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝¹ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
this : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝¹ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
this : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : NoZeroSMulDivisors Rₚ Sₚ := by
  rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
    RingHom.ker_eq_bot_iff_eq_zero]
  intro x hx
  obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl x
  simp only [RingHom.algebraMap_toAlgebra, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    mul_eq_zero, Subtype.exists, exists_prop] at hx ⊢
  obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
  simp only [(injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
  refine ⟨a, ha, H⟩
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝³ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝² : IsScalarTower R Rₚ Sₚ
this✝¹ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝ : IsDomain Sₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝³ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝² : IsScalarTower R Rₚ Sₚ
this✝¹ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝ : IsDomain Sₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : Module.Finite Rₚ Sₚ := Module.Finite_of_isLocalization R S _ _ p.primeCompl
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁴ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝³ : IsScalarTower R Rₚ Sₚ
this✝² : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : IsDomain Sₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁴ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝³ : IsScalarTower R Rₚ Sₚ
this✝² : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : IsDomain Sₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsIntegrallyClosed Sₚ := isIntegrallyClosed_of_isLocalization _ e _
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
this : IsPrincipalIdealRing Rₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
apply (equivQuotMaximalIdealOfIsLocalization p Rₚ).injective
State after:
case a
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x)) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

State before:
case a
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x)) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Tactic:
rw [trace_quotient_eq_trace_localization_quotient S p Rₚ Sₚ, IsScalarTower.algebraMap_eq S Sₚ,
  RingHom.comp_apply, Ideal.Quotient.algebraMap_eq, Algebra.trace_quotient_mk,
  RingEquiv.apply_symm_apply, ← Algebra.intTrace_eq_trace,
  ← Algebra.intTrace_eq_of_isLocalization R S p.primeCompl (Aₘ := Rₚ) (Bₘ := Sₚ) x,
  ← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
State after:
case a
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

State before:
case a
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Tactic:
simp only [equivQuotMaximalIdealOfIsLocalization, RingHom.quotientKerEquivOfSurjective,
  RingEquiv.coe_trans, Function.comp_apply, Ideal.quotEquivOfEq_mk,
  RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ algebraMap R Sₚ = (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
  RingHom.ker_eq_bot_iff_eq_zero]
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Tactic:
intro x hx
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl x
State after:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0

State before:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0
Tactic:
simp only [RingHom.algebraMap_toAlgebra, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
  mul_eq_zero, Subtype.exists, exists_prop] at hx ⊢
State after:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : ∃ a ∈ algebraMapSubmonoid S p.primeCompl, a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0

State before:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : ∃ a ∈ algebraMapSubmonoid S p.primeCompl, a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
State after:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : (algebraMap R S) a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0

State before:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : (algebraMap R S) a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Tactic:
simp only [(injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
State after:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : a = 0 ∨ x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0

State before:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : a = 0 ∨ x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Tactic:
refine ⟨a, ha, H⟩
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
⊢ IsPrincipalIdealRing Rₚ
Tactic:
by_cases hp : p = ⊥
State after:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsPrincipalIdealRing Rₚ

case neg
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
⊢ IsPrincipalIdealRing Rₚ

State before:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsPrincipalIdealRing Rₚ
Tactic:
have : IsFractionRing R Rₚ := by
  delta IsFractionRing
  convert inferInstanceAs (IsLocalization p.primeCompl Rₚ)
  ext; simp [hp, Ideal.primeCompl, mem_nonZeroDivisors_iff_ne_zero]
State after:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this : IsFractionRing R Rₚ
⊢ IsPrincipalIdealRing Rₚ

State before:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this : IsFractionRing R Rₚ
⊢ IsPrincipalIdealRing Rₚ
Tactic:
letI : Field Rₚ := IsFractionRing.toField R
State after:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this✝ : IsFractionRing R Rₚ
this : Field Rₚ := IsFractionRing.toField R
⊢ IsPrincipalIdealRing Rₚ

State before:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this✝ : IsFractionRing R Rₚ
this : Field Rₚ := IsFractionRing.toField R
⊢ IsPrincipalIdealRing Rₚ
Tactic:
infer_instance
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsFractionRing R Rₚ
Tactic:
delta IsFractionRing
State after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsLocalization R⁰ Rₚ

State before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsLocalization R⁰ Rₚ
Tactic:
convert inferInstanceAs (IsLocalization p.primeCompl Rₚ)
State after:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ R⁰ = p.primeCompl

State before:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ R⁰ = p.primeCompl
Tactic:
ext
State after:
case h.e'_3.h
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
x✝ : R
⊢ x✝ ∈ R⁰ ↔ x✝ ∈ p.primeCompl

State before:
case h.e'_3.h
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
x✝ : R
⊢ x✝ ∈ R⁰ ↔ x✝ ∈ p.primeCompl
Tactic:
simp [hp, Ideal.primeCompl, mem_nonZeroDivisors_iff_ne_zero]
State after:
no goals

State before:
case neg
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
⊢ IsPrincipalIdealRing Rₚ
Tactic:
have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
State after:
case neg
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
this : DiscreteValuationRing (Localization.AtPrime p)
⊢ IsPrincipalIdealRing Rₚ

State before:
case neg
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
this : DiscreteValuationRing (Localization.AtPrime p)
⊢ IsPrincipalIdealRing Rₚ
Tactic:
infer_instance
State after:
no goals