-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit [Algebra A K] [IsFractionRing A K] (x : K)
    (hx : IsIntegral A x) (hI : IsUnit (adjoinIntegral A⁰ x hx)) : adjoinIntegral A⁰ x hx = 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ I = 1

Tactic:
have mul_self : IsIdempotentElem I := by
  apply coeToSubmodule_injective
  simp only [coe_mul, adjoinIntegral_coe, I]
  rw [(Algebra.adjoin A {x}).isIdempotentElem_toSubmodule]

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = 1

Proof state:
case a
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ (fun I => ↑I) (I * I) = (fun I => ↑I) I

Tactic:
simp only [coe_mul, adjoinIntegral_coe, I]

Result:
case a
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ Subalgebra.toSubmodule (Algebra.adjoin A {x}) * Subalgebra.toSubmodule (Algebra.adjoin A {x}) =
    Subalgebra.toSubmodule (Algebra.adjoin A {x})

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ IsIdempotentElem I

Tactic:
apply coeToSubmodule_injective

Result:
case a
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ (fun I => ↑I) (I * I) = (fun I => ↑I) I

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
hI : IsUnit (adjoinIntegral A⁰ x hx)
⊢ adjoinIntegral A⁰ x hx = 1

Tactic:
set I := adjoinIntegral A⁰ x hx

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ I = 1

Proof state:
case a
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ Subalgebra.toSubmodule (Algebra.adjoin A {x}) * Subalgebra.toSubmodule (Algebra.adjoin A {x}) =
    Subalgebra.toSubmodule (Algebra.adjoin A {x})

Tactic:
rw [(Algebra.adjoin A {x}).isIdempotentElem_toSubmodule]

Result:
no goals