-- Mathlib/RingTheory/DedekindDomain/Dvr.lean
theorem IsLocalization.isDedekindDomain [IsDedekindDomain A] {M : Submonoid A} (hM : M ≤ A⁰)
    (Aₘ : Type*) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [IsLocalization M Aₘ] :
    IsDedekindDomain Aₘ

Proof state:
case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ ∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, (algebraMap Aₘ (FractionRing A)) y = x

Tactic:
intro x hx

Result:
case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
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

Proof state:
case refine_4.intro.mk.intro
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
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 (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ (algebraMap A (FractionRing A)) z = (algebraMap A (FractionRing A)) ↑⟨y, y_mem⟩ * x

Tactic:
rw [hz, ← Algebra.smul_def]

Result:
case refine_4.intro.mk.intro
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
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 (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x

Proof state:
case refine_4.intro.mk.intro
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
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 (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap Aₘ (FractionRing A)) y = x

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

Result:
case refine_4.intro.mk.intro
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
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 (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ (algebraMap A (FractionRing A)) z = (algebraMap A (FractionRing A)) ↑⟨y, y_mem⟩ * x

Proof state:
case refine_3
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ

Tactic:
exact Ring.DimensionLEOne.localization Aₘ hM

Result:
no goals

Proof state:
case refine_4.intro.mk.intro
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
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 (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
⊢ IsDedekindDomain Aₘ

Tactic:
haveI : IsScalarTower A Aₘ (FractionRing A) :=
  IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm

Result:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this : IsScalarTower A Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
⊢ IsDedekindDomain Aₘ

Tactic:
letI : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (IsLocalization.lift h)

Result:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
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 : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
⊢ IsDedekindDomain Aₘ