R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
⊢ IsDedekindDomain Aₘ
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
⊢ IsDedekindDomain Aₘ
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)))
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
⊢ IsDedekindDomain Aₘ
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
⊢ IsDedekindDomain Aₘ
letI : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (IsLocalization.lift h)
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this : IsScalarTower A Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
⊢ IsDedekindDomain Aₘ
haveI : IsScalarTower A Aₘ (FractionRing A) :=
  IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this : IsScalarTower A Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
haveI : IsFractionRing Aₘ (FractionRing A) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M _ _
case refine'_1
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsNoetherianRing Aₘ

case refine'_2
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ

case refine'_3
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ ∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
refine' (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨_, _, _⟩
case mk
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit (↑(algebraMap A (FractionRing A)) ↑{ val := y, property := hy })
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
⊢ ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
rintro ⟨y, hy⟩
no goals
case mk
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit (↑(algebraMap A (FractionRing A)) ↑{ val := y, property := hy })
exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
no goals
case refine'_1
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsNoetherianRing Aₘ
exact IsLocalization.isNoetherianRing M _ (by infer_instance)
no goals
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsNoetherianRing A
infer_instance
no goals
case refine'_2
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ
exact IsDedekindDomain.dimensionLEOne.localization Aₘ hM
case refine'_3
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
case refine'_3
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ ∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
intro x hx
case refine'_3.intro.mk
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
case refine'_3
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
case refine'_3.intro.mk.intro
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
case refine'_3.intro.mk
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindDomain.isIntegrallyClosed hy
case refine'_3.intro.mk.intro
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ ↑(algebraMap A (FractionRing A)) z = ↑(algebraMap A (FractionRing A)) ↑{ val := y, property := y_mem } * x
case refine'_3.intro.mk.intro
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
refine' ⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr _⟩
case refine'_3.intro.mk.intro
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ { val := y, property := y_mem } • x = ↑{ val := y, property := y_mem } • x
case refine'_3.intro.mk.intro
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ ↑(algebraMap A (FractionRing A)) z = ↑(algebraMap A (FractionRing A)) ↑{ val := y, property := y_mem } * x
rw [hz, ← Algebra.smul_def]
no goals
case refine'_3.intro.mk.intro
R : Type ?u.6256
A : Type u_1
K : Type ?u.6262
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ { val := y, property := y_mem } • x = ↑{ val := y, property := y_mem } • x
rfl