awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
he :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K)) : (a : K) → FractionRing Rₘ)
          ((algebraMap R K : (a : R) → K) x)) :
      FractionRing Sₘ)
    ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L)) : (a : L) → FractionRing Sₘ)
        ((algebraMap R L : (a : R) → L) x) :
      FractionRing Sₘ)
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing Rₘ) (FractionRing Sₘ))
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K))) : K →+* FractionRing Rₘ))
            (algebraMap R K) :
          (a : R) → FractionRing Sₘ)
        x :
      FractionRing Sₘ)
    (((@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L))) : L →+* FractionRing Sₘ) (algebraMap K L))
              (algebraMap R K) :
            RingHom.{u_1, u_5} R (FractionRing Sₘ)) :
          (a : R) → FractionRing Sₘ)
        x :
      FractionRing Sₘ)

Tactic:
simp only [RingHom.coe_comp,
      RingHom.coe_coe, Function.comp_apply, ← algebraMap_apply]

Premises used: RingHom.coe_coe, RingHom.coe_comp, Function.comp_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
he :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
      FractionRing Sₘ)
    ((algebraMap Sₘ (FractionRing Sₘ) : (a : Sₘ) → FractionRing Sₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x : S)) :
      FractionRing Sₘ)
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Rₘ K)) : (a : K) → FractionRing Rₘ)
          ((algebraMap R K : (a : R) → K) x)) :
      FractionRing Sₘ)
    ((AlgEquiv.toRingEquiv (AlgEquiv.symm (algEquiv Sₘ L)) : (a : L) → FractionRing Sₘ)
        ((algebraMap R L : (a : R) → L) x) :
      FractionRing Sₘ)

Tactic:
rw [algebraMap_apply R Rₘ (FractionRing R), AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
    algebraMap_apply R S L, algebraMap_apply S Sₘ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]

Premises used: FractionRing, AlgEquiv.commutes, AlgEquiv.coe_ringEquiv, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
he :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap R (FractionRing Rₘ) : (a : R) → FractionRing Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
      FractionRing Sₘ)
    ((algebraMap Sₘ (FractionRing Sₘ) : (a : Sₘ) → FractionRing Sₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x : S)) :
      FractionRing Sₘ)

Tactic:
simp only [← algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
inst_7 : Algebra R Rₘ
inst_8 : IsTorsionFree R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
M : Submonoid R
inst_10 : IsLocalization M Rₘ
inst_11 : Algebra Rₘ Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra R Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_17 : Algebra.{u_4, u_5} (FractionRing Rₘ) (FractionRing Sₘ)
inst_18 : IsScalarTower.{u_4, u_4, u_5} Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : LE.le (α := Submonoid S) (algebraMapSubmonoid S M) S⁰
f₁ : RingHom.{u_4, u_1} Rₘ K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
f₂ : RingHom.{u_5, u_2} Sₘ L := IsLocalization.map (M := algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) hM'
algInst : Algebra.{u_4, u_1} Rₘ K := f₁.toAlgebra
algInst_1 : Algebra.{u_5, u_2} Sₘ L := f₂.toAlgebra
this_1 : IsScalarTower R Rₘ K
this_2 : IsScalarTower S Sₘ L
this_3 : IsFractionRing.{u_4, u_1} Rₘ K
this_4 : IsFractionRing.{u_5, u_2} Sₘ L
this : IsDomain Rₘ
x : R
he :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap Rₘ (FractionRing Rₘ) : (a : Rₘ) → FractionRing Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x)) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
he₁ :
  Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap Rₘ (FractionRing Sₘ) : (a : Rₘ) → FractionRing Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
he₂ he₃ :
  Eq.{u_5 + 1} (α := FractionRing Sₘ) ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)
⊢ Eq.{u_5 + 1} (α := FractionRing Sₘ)
    ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ) : (a : FractionRing Rₘ) → FractionRing Sₘ)
        ((algebraMap R (FractionRing Rₘ) : (a : R) → FractionRing Rₘ) x) :
      FractionRing Sₘ)
    ((algebraMap R (FractionRing Sₘ) : (a : R) → FractionRing Sₘ) x : FractionRing Sₘ)

Tactic:
rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]

Premises used: FractionRing, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
rw : ∀ (c : ↥P'), IsRegular (↑c : S)
⊢ IsTorsionFree S Sₚ

Tactic:
rw [isTorsionFree_iff_algebraMap_injective,
    injective_iff_isRegular (algebraMapSubmonoid S P.primeCompl)]

Premises used: Module.isTorsionFree_iff_algebraMap_injective, IsLocalization.injective_iff_isRegular, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
x_1 : ↥P'
x : S
hx : Membership.mem (γ := Submonoid S) P' x
⊢ 0 ∉ P'

Tactic:
simp [Algebra.algebraMapSubmonoid]

Premises used: Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ ∀ (c : ↥P'), IsRegular (↑c : S)

Tactic:
exact fun ⟨x, hx⟩ ↦ isRegular_iff_ne_zero'.mpr <|
    ne_of_mem_of_not_mem hx <| by simp [Algebra.algebraMapSubmonoid]
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ FaithfulSMul R Rₚ

Tactic:
have := IsLocalization.AtPrime.faithfulSMul Rₚ R P
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
this : FaithfulSMul R Rₚ
⊢ IsTorsionFree.{u_1, u_2} R Sₚ

Tactic:
IsTorsionFree.trans_faithfulSMul R Rₚ _

Premises used: Localization.AtPrime, Module.IsTorsionFree.trans_faithfulSMul
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
this : FaithfulSMul R Rₚ
⊢ IsTorsionFree.{u_1, u_2} R Sₚ

Tactic:
exact IsTorsionFree.trans_faithfulSMul R Rₚ _
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsScalarTower S Sₚ L

Tactic:
localization_isScalarTower_of_submonoid_le _ _ _ _
    (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _
      P.primeCompl_le_nonZeroDivisors)

Premises used: Quotient.mk', Ideal.primeCompl_le_nonZeroDivisors, OreLocalization.oreDiv, IsLocalization.localization_isScalarTower_of_submonoid_le, algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsFractionRing.{u_1, u_1} Rₚ K

Tactic:
isFractionRing_of_isDomain_of_isLocalization P.primeCompl _ _

Premises used: IsFractionRing.isFractionRing_of_isDomain_of_isLocalization, Ideal.primeCompl
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsFractionRing.{u_2, u_2} Sₚ L

Tactic:
isFractionRing_of_isDomain_of_isLocalization P' _ _

Premises used: IsFractionRing.isFractionRing_of_isDomain_of_isLocalization, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
x_1 : ↥P.primeCompl
x : R
hx : x ∈ P.primeCompl
h : x = 0
⊢ x ∈ (↑P : Set R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
x_1 : ↥P.primeCompl
x : R
hx : x ∈ P.primeCompl
⊢ IsUnit.{u_2} (M := L)
    ((algebraMap R L : (a : R) → L) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) x hx) : R) : L)

Tactic:
simpa using fun h ↦ hx <| by simp [h]
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ Eq (α := Algebra Rₚ (Localization (M := R) R⁰)) (instAlgebraLocalizationAtPrime P) (instAlgebraAtPrimeFractionRing R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ Eq (α := Algebra Rₚ (Localization (M := R) R⁰)) (instAlgebraLocalizationAtPrime P) (instAlgebraAtPrimeFractionRing R)

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
x : R
⊢ Eq.{u_2 + 1} (α := L)
    ((@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ) : (a : R) → L) x : L)
    ((@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ K _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap Rₚ K)) (algebraMap R Rₚ) :
          (a : R) → L)
        x :
      L)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
x : R
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) x : K)
    ((@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ K) (algebraMap R Rₚ) : (a : R) → K) x : K)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
⊢ IsScalarTower.{u_1, u_2, u_2} Rₚ Sₚ L

Tactic:
IsScalarTower.of_algebraMap_eq' <| IsLocalization.ringHom_ext P.primeCompl ?_

Premises used: IsScalarTower.of_algebraMap_eq', Ideal.primeCompl, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
refine :
  Eq (α := RingHom.{u_1, u_2} R L)
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ L) (algebraMap R Rₚ))
    (@RingHom.comp _ Rₚ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ L) (algebraMap Rₚ Sₚ)) (algebraMap R Rₚ))
⊢ IsScalarTower.{u_1, u_2, u_2} Rₚ Sₚ L

Tactic:
refine IsScalarTower.of_algebraMap_eq' <| IsLocalization.ringHom_ext P.primeCompl ?_

Premises used: IsScalarTower.of_algebraMap_eq', Ideal.primeCompl, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : IsDedekindDomain S
⊢ IsDedekindDomain.{u_2} Sₚ

Tactic:
isDedekindDomain S
    (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ P.primeCompl_le_nonZeroDivisors) _

Premises used: IsLocalization.isDedekindDomain, Ideal.primeCompl_le_nonZeroDivisors, algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Module.Finite R S
hP : NeZero P
⊢ IsPrincipalIdealRing.{u_2} Sₚ

Tactic:
IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P (fun h ↦ hP.1 h)

Premises used: IsDedekindDomain.isPrincipalIdealRing_localization_over_prime, NeZero.out
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra.IsSeparable.{u_1, u_2} K L
⊢ Algebra.IsSeparable.{u_1, u_2} (FractionRing Rₚ) (FractionRing Sₚ)

Tactic:
let _ : Algebra Rₚ (FractionRing Sₚ) := OreLocalization.instAlgebra
  FractionRing.isSeparable_of_isLocalization S _ _ P.primeCompl_le_nonZeroDivisors

Premises used: OreLocalization.instAlgebra, Localization.AtPrime, FractionRing.isSeparable_of_isLocalization, Localization, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
⊢ Eq (α := Submonoid T) (algebraMapSubmonoid T P') P''

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw : IsLocalization P'' Tₚ
⊢ IsLocalization (algebraMapSubmonoid T P') Tₚ

Tactic:
rw [show algebraMapSubmonoid T P' = P'' by simp]
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
⊢ IsLocalization P'' Tₚ

Tactic:
Localization.isLocalization

Premises used: Localization.isLocalization
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
⊢ IsLocalization P'' Tₚ

Tactic:
exact Localization.isLocalization

Premises used: Localization.isLocalization
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := P') (T := algebraMapSubmonoid T P') Tₚ (algebraMap S T) ⋯) (algebraMap S Sₚ))
rw₁ :
  Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T Tₚ) (algebraMap S T))
rw₂ rw₃ : Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ) (algebraMap S Tₚ)
⊢ Eq (α := RingHom.{u_2, u_3} S Tₚ) (algebraMap S Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ))

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

Premises used: IsLocalization.map_comp, IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra