awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
R : Type u_2
Rₘ : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
M : Submonoid R
inst_4 : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' :
  LT.lt.{u_2} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (((IsLocalization.orderIsoOfPrime M Rₘ :
            OrderIso.{u_3, u_2} { p : Ideal Rₘ // p.IsPrime }
              { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
          (a : { p : Ideal Rₘ // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        (Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) p hpp) :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (((IsLocalization.orderIsoOfPrime M Rₘ :
            OrderIso.{u_3, u_2} { p : Ideal Rₘ // p.IsPrime }
              { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
          (a : { p : Ideal Rₘ // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        (Subtype.mk (p := fun (p : Ideal Rₘ) ↦ p.IsPrime) P ⋯) :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
⊢ LT.lt (α := Ideal R) ⊥ (Ideal.under R p)

Tactic:
exact IsLocalization.bot_lt_under_prime _ _ hM _ hp0

Premises used: IsLocalization.bot_lt_under_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit (M := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ M) y hy) : A) :
      FractionRing A)

Tactic:
IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))

Premises used: mt, IsFractionRing.to_map_eq_zero_iff, nonZeroDivisors.ne_zero, IsUnit.mk0, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit (M := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ M) y hy) : A) :
      FractionRing A)

Tactic:
exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))

Premises used: mt, nonZeroDivisors.ne_zero, IsUnit.mk0
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
⊢ ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)

Tactic:
have h : ∀ y : M, IsUnit (algebraMap A (FractionRing A) y) := by
    rintro ⟨y, hy⟩
    exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
⊢ IsScalarTower A Aₘ (FractionRing A)

Tactic:
haveI : IsScalarTower A Aₘ (FractionRing A) :=
    IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this : IsScalarTower A Aₘ (FractionRing A)
⊢ IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)

Tactic:
haveI : IsFractionRing Aₘ (FractionRing A) :=
    IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M _ _
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ

Tactic:
(isDedekindDomain_iff _ (FractionRing A)).mpr ⟨?_, ?_, ?_, ?_⟩

Premises used: Iff.mpr, FractionRing, And.intro, isDedekindDomain_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
refine_1 : IsDomain Aₘ
refine_2 : IsNoetherianRing Aₘ
refine_3 : Ring.DimensionLEOne Aₘ
refine_4 :
  ∀ {x : FractionRing A},
    IsIntegral Aₘ x → ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x
⊢ IsDedekindDomain Aₘ

Tactic:
refine (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨?_, ?_, ?_, ?_⟩

Premises used: Iff.mpr, FractionRing, And.intro, isDedekindDomain_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
⊢ IsDomain Aₘ

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
⊢ IsNoetherianRing Aₘ

Tactic:
IsLocalization.isNoetherianRing M _ inferInstance

Premises used: IsLocalization.isNoetherianRing, inferInstance
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
⊢ IsNoetherianRing Aₘ

Tactic:
exact IsLocalization.isNoetherianRing M _ inferInstance

Premises used: IsLocalization.isNoetherianRing, inferInstance
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ

Tactic:
Ring.DimensionLEOne.localization Aₘ hM

Premises used: Ring.DimensionLEOne.localization
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ

Tactic:
exact Ring.DimensionLEOne.localization Aₘ hM

Premises used: Ring.DimensionLEOne.localization
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
refine_4 :
  ∀ (y : A) (y_mem : y ∈ M) (hy : IsIntegral A (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x)),
    ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x
⊢ ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x

Tactic:
obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _

Premises used: IsIntegral.exists_multiple_integral_of_isLocalization
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x)
refine_4 :
  ∀ (z : A)
    (hz :
      (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z = Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x),
    ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x
⊢ ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x

Tactic:
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindRing.toIsIntegralClosure hy

Premises used: IsDedekindRing.toIsIntegralClosure, Iff.mp, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x)
z : A
hz : (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z = Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x
⊢ ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x

Tactic:
⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩

Premises used: Iff.mpr, IsLocalization.lift_mk'_spec, Subtype.mk, IsLocalization.mk', Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x)
z : A
hz : (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z = Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x
refine_4 :
  (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z =
    HMul.hMul (α := FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
          (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem) : A) :
        FractionRing A)
      x
⊢ ∃ (y : Aₘ), (algebraMap Aₘ (FractionRing A) : (a : Aₘ) → FractionRing A) y = x

Tactic:
refine ⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x)
z : A
hz : (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z = Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x
refine_4 :
  Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x = (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem) : A) • x
⊢ (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z =
    HMul.hMul (α := FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
          (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem) : A) :
        FractionRing A)
      x

Tactic:
rw [hz, ← Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization M Aₘ
h :
  ∀ (y : ↥M),
    IsUnit (M := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑y : A) : FractionRing A)
this_1 : Algebra.{u_2, u_1} Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this_2 : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing.{u_2, u_1} Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x)
z : A
hz : (algebraMap A (FractionRing A) : (a : A) → FractionRing A) z = Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x
⊢ Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem • x = (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ M) y y_mem) : A) • x

Tactic:
rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
P : Ideal A
inst_3 : P.IsPrime
Aₘ : Type u_2
inst_4 : CommRing Aₘ
inst_5 : IsDomain Aₘ
inst_6 : Algebra A Aₘ
inst_7 : IsLocalization.AtPrime Aₘ P
⊢ IsDedekindDomain Aₘ

Tactic:
IsLocalization.isDedekindDomain A P.primeCompl_le_nonZeroDivisors Aₘ

Premises used: IsLocalization.isDedekindDomain, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
P : Ideal A
inst_3 : P.IsPrime
⊢ IsDedekindDomain.{u_1} (Localization.AtPrime P)

Tactic:
IsLocalization.AtPrime.isDedekindDomain A P _

Premises used: IsLocalization.AtPrime.isDedekindDomain
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_2 : CommRing Aₘ
inst_3 : Algebra A Aₘ
inst_4 : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
obtain : ∀ (x : A) (x_mem : x ∈ P) (x_ne : x ≠ 0), False
⊢ False

Tactic:
obtain ⟨x, x_mem, x_ne⟩ := P.ne_bot_iff.mp hP

Premises used: Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_2 : CommRing Aₘ
inst_3 : Algebra A Aₘ
inst_4 : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False

Tactic:
(IsLocalRing.maximalIdeal.isMaximal _).ne_top
      (Ideal.eq_top_of_isUnit_mem _
        ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
        (isUnit_iff_ne_zero.mpr
          ((map_ne_zero_iff (algebraMap A Aₘ)
                (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr
            x_ne)))

Premises used: Iff.mpr, Algebra.algebraMap, Ideal.eq_top_of_isUnit_mem, IsLocalization.injective, IsLocalization.AtPrime.to_map_mem_maximal_iff, isUnit_iff_ne_zero, IsLocalRing.maximalIdeal.isMaximal, IsLocalization.AtPrime.isLocalRing, Ideal.primeCompl_le_nonZeroDivisors, Ideal.IsMaximal.ne_top, map_ne_zero_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_2 : CommRing Aₘ
inst_3 : Algebra A Aₘ
inst_4 : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False

Tactic:
exact
    (IsLocalRing.maximalIdeal.isMaximal _).ne_top
      (Ideal.eq_top_of_isUnit_mem _
        ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
        (isUnit_iff_ne_zero.mpr
          ((map_ne_zero_iff (algebraMap A Aₘ)
                (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr
            x_ne)))

Premises used: Iff.mpr, Algebra.algebraMap, Ideal.eq_top_of_isUnit_mem, IsLocalization.injective, IsLocalization.AtPrime.to_map_mem_maximal_iff, isUnit_iff_ne_zero, IsLocalRing.maximalIdeal.isMaximal, IsLocalization.AtPrime.isLocalRing, Ideal.primeCompl_le_nonZeroDivisors, Ideal.IsMaximal.ne_top, map_ne_zero_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization.AtPrime Aₘ P
this_1 : IsNoetherianRing Aₘ := ⋯
this : IsLocalRing Aₘ := ⋯
⊢ ¬IsField Aₘ

Tactic:
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization.AtPrime Aₘ P
this_1 : IsNoetherianRing Aₘ := ⋯
this : IsLocalRing Aₘ := ⋯
hnf : ¬IsField Aₘ
⊢ IsDiscreteValuationRing Aₘ

Tactic:
((IsDiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
      (IsLocalization.AtPrime.isDedekindDomain A P _)

Premises used: Iff.mpr, List.TFAE.out, IsDiscreteValuationRing.TFAE, IsLocalization.AtPrime.isDedekindDomain, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization.AtPrime Aₘ P
this_1 : IsNoetherianRing Aₘ := ⋯
this : IsLocalRing Aₘ := ⋯
hnf : ¬IsField Aₘ
⊢ IsDiscreteValuationRing Aₘ

Tactic:
exact
    ((IsDiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
      (IsLocalization.AtPrime.isDedekindDomain A P _)

Premises used: Iff.mpr, List.TFAE.out, IsDiscreteValuationRing.TFAE, IsLocalization.AtPrime.isDedekindDomain, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst_3 : CommRing Aₘ
inst_4 : IsDomain Aₘ
inst_5 : Algebra A Aₘ
inst_6 : IsLocalization.AtPrime Aₘ P
letI letI₁ letI₂ letI₃ : IsDiscreteValuationRing Aₘ
letI₄ : ∀ (hnf : ¬IsField Aₘ), IsDiscreteValuationRing Aₘ
⊢ IsDiscreteValuationRing Aₘ

Tactic:
classical
  letI : IsNoetherianRing Aₘ :=
    IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindRing.toIsNoetherian
  letI : IsLocalRing Aₘ := IsLocalization.AtPrime.isLocalRing Aₘ P
  have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
  exact
    ((IsDiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
      (IsLocalization.AtPrime.isDedekindDomain A P _)
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
rcases : ∀ (q : Ideal A) (hq : q.IsMaximal) (hpq : p ≤ q), p.IsMaximal
⊢ p.IsMaximal

Tactic:
rcases p.exists_le_maximal (Ideal.IsPrime.ne_top hpp) with ⟨q, hq, hpq⟩

Premises used: Ideal.exists_le_maximal, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
⊢ Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)

Tactic:
have hinj : Function.Injective (algebraMap A (Localization.AtPrime q)) :=
      IsLocalization.injective (Localization.AtPrime q) q.primeCompl_le_nonZeroDivisors