awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have this₁ : 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ₚ)
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have e : 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 _ _))
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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⁰
⊢ 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)
have this₁ : IsDomain Sₚ
Tactic: haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
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ₚ
have rw : ∀ (x : Rₚ), Eq.{u_2 + 1} (α := Sₚ) (((algebraMap Rₚ Sₚ : Rₚ →+* Sₚ) : (a : Rₚ) → Sₚ) x : Sₚ) (0 : Sₚ) → x = 0
Tactic: rw [isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
      RingHom.ker_eq_bot_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have this₁ : Module.Finite Rₚ Sₚ
Tactic: haveI : Module.Finite Rₚ Sₚ := .of_isLocalization R S p.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have this₁ : IsIntegrallyClosed Sₚ
Tactic: haveI : IsIntegrallyClosed Sₚ := isIntegrallyClosed_of_isLocalization _ _ e
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
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ₚ
have pos : ∀ (hp : p = ⊥), IsPrincipalIdealRing Rₚ
Tactic: by_cases hp : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
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ₚ
⊢ IsPrincipalIdealRing Rₚ
have neg : ∀ (hp : ¬p = ⊥), IsPrincipalIdealRing Rₚ
Tactic: by_cases hp : p = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
have this₁ : IsDiscreteValuationRing.{u_1} (Localization.AtPrime p)
Tactic: have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have this₁ : IsPrincipalIdealRing Rₚ
Tactic: have : IsPrincipalIdealRing Rₚ := by
    by_cases hp : p = ⊥
    · infer_instance
    · have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
      infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (hypothesis)
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ₚ
⊢ 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)
have this₁ : Free Rₚ Sₚ
Tactic: haveI : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
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ₚ
⊢ 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)
have 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ₚ))
Tactic: apply (equivQuotMaximalIdeal p Rₚ).injective
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (goal)
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ₚ
⊢ 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ₚ))
have 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ₚ))
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]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
inst_1 : Nontrivial R
⊢ Nontrivial.{u_1} (TwoSidedIdeal R)
have obtain : ∀ (I J : RingCon R) (h : I ≠ J), Nontrivial.{u_1} (TwoSidedIdeal R)
Tactic: obtain ⟨I, J, h⟩ : Nontrivial (RingCon R) := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 : TwoSidedIdeal R
inst_1 : Nontrivial R
I J : RingCon R
h : I ≠ J
⊢ { ringCon := I : TwoSidedIdeal R } ≠ { ringCon := J }
have contrapose : ∀ (h : { ringCon := I : TwoSidedIdeal R } = { ringCon := J }), I = J
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
⊢ { ringCon := t₁ : TwoSidedIdeal R } = { ringCon := t₂ }
have e_ringCon : t₁ = t₂
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
⊢ t₁ = t₂
have e_ringCon : ∀ (a b : R) (H : (t₁ : (a : R) → R → Prop) a b), (t₂ : (a : R) → R → Prop) a b
Tactic: refine RingCon.ext fun a b ↦ ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
e_ringCon : ∀ (a b : R) (H : (t₁ : (a : R) → R → Prop) a b), (t₂ : (a : R) → R → Prop) a b
⊢ t₁ = t₂
have e_ringCon₁ : ∀ (a b : R) (H : (t₂ : (a : R) → R → Prop) a b), (t₁ : (a : R) → R → Prop) a b
Tactic: refine RingCon.ext fun a b ↦ ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
⊢ (t₂ : (a : R) → R → Prop) a b
have H' : Membership.mem (γ := Set R) {x : R | (t₁ : (a : R) → R → Prop) x 0} (a - b)
Tactic: have H' : a - b ∈ {x | t₁ x 0} := sub_self b ▸ t₁.sub H (t₁.refl b)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' : Membership.mem (γ := Set R) {x : R | (t₁ : (a : R) → R → Prop) x 0} (a - b)
⊢ (t₂ : (a : R) → R → Prop) a b
have H'₁ : Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
Tactic: rw [h] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ (t₂ : (a : R) → R → Prop) a b
have h₁ : a = a - b + b
Tactic: convert! t₂.add H' (t₂.refl b) using 1
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
h₁ : a = a - b + b
⊢ (t₂ : (a : R) → R → Prop) a b
have h₂ : b = 0 + b
Tactic: convert! t₂.add H' (t₂.refl b) using 1
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
⊢ (t₁ : (a : R) → R → Prop) a b
have H' : Membership.mem (γ := Set R) {x : R | (t₂ : (a : R) → R → Prop) x 0} (a - b)
Tactic: have H' : a - b ∈ {x | t₂ x 0} := sub_self b ▸ t₂.sub H (t₂.refl b)