awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
this :
  IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
⊢ Eq.{u_1 + 1} (α := R ⧸ p)
    (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
            RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
        ((Algebra.trace (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            (a : Sₚ ⧸ pSₚ) → Rₚ ⧸ maximalIdeal Rₚ)
          (((equivQuotientMapMaximalIdeal S p Rₚ Sₚ :
                RingEquiv.{u_2, u_4}
                  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                    (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
              (a : S ⧸ pS) → Sₚ ⧸ pSₚ)
            ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x))) :
      R ⧸ p)
    (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
            RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
        ((Algebra.trace (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            (a : Sₚ ⧸ pSₚ) → Rₚ ⧸ maximalIdeal Rₚ)
          ((algebraMap S
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                  (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
              (a : S) → Sₚ ⧸ pSₚ)
            x)) :
      R ⧸ p)

Tactic:
congr
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
this :
  IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
he :
  ∀ (x : R),
    Eq.{u_4 + 1} (α :=
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                    (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
                (↑(equivQuotMaximalIdeal p Rₚ) : R ⧸ p →+* Rₚ ⧸ maximalIdeal Rₚ))
              (Ideal.Quotient.mk p) :
            (a : R) → Sₚ ⧸ pSₚ)
          x :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
      (((RingHom.comp
                (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                  (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ) : S ⧸ pS →+* Sₚ ⧸ pSₚ)
                  (algebraMap (R ⧸ p)
                    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))))
                (Ideal.Quotient.mk p) :
              RingHom.{u_1, u_4} R
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                  (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
            (a : R) → Sₚ ⧸ pSₚ)
          x :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
⊢ Eq (α :=
    RingHom.{u_1, u_4} (R ⧸ p)
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
      (↑(equivQuotMaximalIdeal p Rₚ) : R ⧸ p →+* Rₚ ⧸ maximalIdeal Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ) : S ⧸ pS →+* Sₚ ⧸ pSₚ)
      (algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
rw :
  Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
    (RingHom.comp (IsLocalization.map (T := algebraMapSubmonoid S p.primeCompl) Sₚ (algebraMap R S) ⋯)
      (algebraMap R Rₚ))
rw₁ :
  Eq (α := R →+* Sₚ) (algebraMap R Sₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S))
rw₂ rw₃ : Eq (α := R →+* Sₚ) (algebraMap R Sₚ) (algebraMap R Sₚ)
⊢ Eq (α := R →+* Sₚ) (algebraMap R Sₚ) (RingHom.comp (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Premises used: IsLocalization.map_comp, IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ IsScalarTower R Rₚ Sₚ

Tactic:
haveI : IsScalarTower R Rₚ Sₚ := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq])
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this : IsScalarTower R Rₚ Sₚ
⊢ IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ

Tactic:
haveI : IsLocalization (Submonoid.map (algebraMap R S) (Ideal.primeCompl p)) Sₚ :=
    inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ)
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
⊢ LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰

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 _
        (FaithfulSMul.algebraMap_injective _ _))
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
⊢ IsDomain Sₚ

Tactic:
haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this : IsDomain Sₚ
rw : ∀ (x : Rₚ), Eq.{u_2 + 1} (α := Sₚ) (((algebraMap Rₚ Sₚ : Rₚ →+* Sₚ) : (a : Rₚ) → Sₚ) x : Sₚ) (0 : Sₚ) → x = 0
⊢ IsTorsionFree Rₚ Sₚ

Tactic:
rw [isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
      RingHom.ker_eq_bot_iff_eq_zero]

Premises used: RingHom.ker_eq_bot_iff_eq_zero, Module.isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), Eq.{u_2 + 1} (α := Sₚ) (((algebraMap Rₚ Sₚ : Rₚ →+* Sₚ) : (a : Rₚ) → Sₚ) x : Sₚ) (0 : Sₚ) → x = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this : IsDomain Sₚ
⊢ IsTorsionFree Rₚ Sₚ

Tactic:
haveI : IsTorsionFree Rₚ Sₚ := by
    rw [isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
      RingHom.ker_eq_bot_iff_eq_zero]
    simp
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this : IsTorsionFree Rₚ Sₚ
⊢ Module.Finite Rₚ Sₚ

Tactic:
haveI : Module.Finite Rₚ Sₚ := .of_isLocalization R S p.primeCompl
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ IsIntegrallyClosed Sₚ

Tactic:
haveI : IsIntegrallyClosed Sₚ := isIntegrallyClosed_of_isLocalization _ _ e
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
pos : ∀ (hp : p = ⊥), IsPrincipalIdealRing Rₚ
neg : ∀ (hp : ¬p = ⊥), IsPrincipalIdealRing Rₚ
⊢ IsPrincipalIdealRing Rₚ

Tactic:
by_cases hp : p = ⊥
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsPrincipalIdealRing Rₚ

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
⊢ IsDiscreteValuationRing.{u_1} (Localization.AtPrime p)

Tactic:
have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this_7 : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
this : IsDiscreteValuationRing.{u_1} (Localization.AtPrime p)
⊢ IsPrincipalIdealRing Rₚ

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
⊢ IsPrincipalIdealRing Rₚ

Tactic:
have : IsPrincipalIdealRing Rₚ := by
    by_cases hp : p = ⊥
    · infer_instance
    · have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
      infer_instance
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this_7 : IsIntegrallyClosed Sₚ
this : IsPrincipalIdealRing Rₚ
⊢ Free Rₚ Sₚ

Tactic:
haveI : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this_7 : IsIntegrallyClosed Sₚ
this_8 : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
a :
  Eq (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((equivQuotMaximalIdeal p Rₚ : (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((trace (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
            (a : S ⧸ pS) → R ⧸ p)
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((equivQuotMaximalIdeal p Rₚ : (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((intTrace R S : (a : S) → R) x)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
⊢ Eq.{u_1 + 1} (α := R ⧸ p)
    ((trace (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      R ⧸ p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((intTrace R S : (a : S) → R) x) : R ⧸ p)

Tactic:
apply (equivQuotMaximalIdeal p Rₚ).injective

Premises used: RingEquiv.injective, IsLocalization.AtPrime.equivQuotMaximalIdeal
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this_7 : IsIntegrallyClosed Sₚ
this_8 : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
a :
  Eq (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) : (a : R) → Rₚ ⧸ maximalIdeal Rₚ)
        ((intTrace R S : (a : S) → R) x) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((equivQuotMaximalIdeal p Rₚ : (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((intTrace R S : (a : S) → R) x)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
⊢ Eq (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((equivQuotMaximalIdeal p Rₚ : (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((trace (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
            (a : S ⧸ pS) → R ⧸ p)
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((equivQuotMaximalIdeal p Rₚ : (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((intTrace R S : (a : S) → R) x)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))

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]

Premises used: RingEquiv.apply_symm_apply, Algebra.intTrace_eq_of_isLocalization, Ideal.Quotient.algebraMap_eq, Algebra.trace_quotient_mk, IsScalarTower.algebraMap_eq, trace_quotient_eq_trace_localization_quotient, RingHom.comp_apply, Ideal.primeCompl, IsScalarTower.algebraMap_apply, Algebra.intTrace_eq_trace