R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ ∃ y, ↑(algebraMap A (FractionRing A)) y = x
R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
⊢ IsIntegrallyClosed A
refine ⟨fun {x hx} => ?_⟩
R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)

R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0
R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ ∃ y, ↑(algebraMap A (FractionRing A)) y = x
rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot, ←
  coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
  FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (h.isUnit _)]
no goals
R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)
exact mem_adjoinIntegral_self A⁰ x hx
no goals
R : Type ?u.131805
A : Type u_1
K : Type ?u.131811
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0
exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)