awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
h : RingEquiv.{u_2, u_3} (FractionalIdeal (R := A) A⁰ (FractionRing A)) (FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) :=
  mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal (R := A) A⁰ (FractionRing A)
⊢ x ≠ ⊥ →
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) (x * x⁻¹) :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) 1 :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↔
    Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
          FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (⊥ : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) →
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          ((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (((h.toEquiv : (a : FractionalIdeal A⁰ (FractionRing A)) → FractionalIdeal A⁰ K) x)⁻¹ :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) =
        1

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
hI : IsUnit (M := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (adjoinIntegral A⁰ x hx)
set :
  let I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx;
  ∀ (hI : IsUnit I), I = 1
⊢ Eq (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (adjoinIntegral A⁰ x hx) 1

Tactic:
set I := adjoinIntegral A⁰ x hx

Premises used: FractionalIdeal.adjoinIntegral, nonZeroDivisors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
a :
  Eq.{u_3 + 1} (α := Submodule A K)
    ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) (I * I))
    ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) I)
⊢ IsIdempotentElem I

Tactic:
apply coeToSubmodule_injective

Premises used: FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
a :
  HMul.hMul (α := Submodule A K) (β := Submodule A K)
      ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
      ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K) =
    (Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x]
⊢ Eq.{u_3 + 1} (α := Submodule A K)
    ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) (I * I))
    ((fun (I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ (↑I : Submodule A K)) I)

Tactic:
simp only [coe_mul, adjoinIntegral_coe, I]

Premises used: FractionalIdeal.adjoinIntegral_coe, FractionalIdeal.coe_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
a a₁ :
  Eq (α := Submodule A K) ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
⊢ HMul.hMul (α := Submodule A K) (β := Submodule A K)
      ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K)
      ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x] : Submodule A K) =
    (Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) A[x]

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

Premises used: Subalgebra.isIdempotentElem_toSubmodule, Algebra.adjoin, Singleton.singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
⊢ IsIdempotentElem I

Tactic:
have mul_self : IsIdempotentElem I := by
    apply coeToSubmodule_injective
    simp only [coe_mul, adjoinIntegral_coe, I]
    rw [(Algebra.adjoin A {x}).isIdempotentElem_toSubmodule]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
    ((fun (x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ x * I⁻¹) (I * I))
    ((fun (x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ x * I⁻¹) I)

Tactic:
congr_arg (· * I⁻¹) mul_self

Premises used: HMul.hMul, congr_arg, Inv.inv
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
h : I = I * I * I⁻¹
h₁ : 1 = I * I⁻¹
⊢ I = 1

Tactic:
convert! congr_arg (· * I⁻¹) mul_self

Premises used: HMul.hMul, congr_arg, Inv.inv
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = I * I * I⁻¹

Tactic:
simp only [(mul_inv_cancel_iff_isUnit K).mpr hI, mul_assoc, mul_one]

Premises used: Iff.mpr, mul_assoc, FractionalIdeal.mul_inv_cancel_iff_isUnit, mul_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
x : K
hx : IsIntegral A x
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ 1 = I * I⁻¹

Tactic:
simp only [(mul_inv_cancel_iff_isUnit K).mpr hI, mul_assoc, mul_one]

Premises used: Iff.mpr, mul_assoc, FractionalIdeal.mul_inv_cancel_iff_isUnit, mul_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
inl : I / 0 = I * 0⁻¹
inr : ∀ (hJ : J ≠ 0), I / J = I * J⁻¹
⊢ I / J = I * J⁻¹

Tactic:
obtain rfl | hJ := eq_or_ne J 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
⊢ I / 0 = I * 0⁻¹

Tactic:
simp [inv_zero']

Premises used: FractionalIdeal.inv_zero'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
⊢ I / J = I * J⁻¹

Tactic:
le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_)

Premises used: Iff.mpr, FractionalIdeal.le_div_iff_mul_le, le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I / J ≤ I * J⁻¹
inr₁ : I * J⁻¹ * J ≤ I
⊢ I / J = I * J⁻¹

Tactic:
refine le_antisymm ?_ ((FractionalIdeal.le_div_iff_mul_le hJ).2 ?_)

Premises used: Iff.mpr, FractionalIdeal.le_div_iff_mul_le, le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
this : I / J * J ≤ I
⊢ I / J ≤ I * J⁻¹

Tactic:
simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this

Premises used: mul_assoc, mul_left_mono, Iff.mp, isDedekindDomainInv_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I / J * J ≤ I
⊢ I / J ≤ I * J⁻¹

Tactic:
suffices I / J * J ≤ I by
        simpa [mul_assoc, isDedekindDomainInv_iff.mp h _ hJ] using mul_left_mono (a := J⁻¹) this
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
⊢ I / J * J ≤ I

Tactic:
simp [FractionalIdeal.mul_le, mem_div_iff_of_ne_zero hJ]

Premises used: FractionalIdeal.mul_le, FractionalIdeal.mem_div_iff_of_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h : IsDedekindDomainInv A
I_1 J_1 I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hJ : J ≠ 0
inr : I * (J⁻¹ * J) ≤ I
inr₁ : I * (J * J⁻¹) ≤ I
inr₂ : I * 1 ≤ I
inr₃ inr₄ : I ≤ I
⊢ I * J⁻¹ * J ≤ I

Tactic:
rw [mul_assoc, mul_comm _ J, isDedekindDomainInv_iff.mp h _ hJ, mul_one]

Premises used: mul_assoc, Iff.mp, mul_comm, mul_one, isDedekindDomainInv_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
⊢ IsNoetherianRing A

Tactic:
isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩

Premises used: Iff.mpr, isNoetherianRing_iff, IsNoetherian.mk
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
refine : ∀ (I : Ideal A), Submodule.FG I
⊢ IsNoetherianRing A

Tactic:
refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩

Premises used: Iff.mpr, isNoetherianRing_iff, IsNoetherian.mk
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
pos : ∀ (hI : I = ⊥), Submodule.FG I
neg : ∀ (hI : ¬I = ⊥), Submodule.FG I
⊢ Submodule.FG I

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI : I = ⊥
pos : Submodule.FG.{u_2, u_2} (R := A) (M := A) ⊥
⊢ Submodule.FG I

Tactic:
rw [hI]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG.{u_2, u_2} (R := A) (M := A) ⊥

Tactic:
apply Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI : ¬I = ⊥
⊢ Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0

Tactic:
have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI_1 : ¬I = ⊥
hI : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ Submodule.FG I

Tactic:
I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) hI.isUnit

Premises used: IsFractionRing.injective, Ne.isUnit, FractionRing, Submodule.FG, Ideal.FG, Ideal.fg_of_isUnit
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI_1 : ¬I = ⊥
hI : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ Submodule.FG I

Tactic:
exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) hI.isUnit

Premises used: IsFractionRing.injective, Ne.isUnit, FractionRing, Ideal.fg_of_isUnit
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
⊢ IsIntegrallyClosed A

Tactic:
(isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)

Premises used: Iff.mpr, FractionRing, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
refine :
  ∀ {x : FractionRing A} {hx : IsIntegral A x},
    ∃ (y : A), (algebraMap A (FractionRing A) : (a : A) → FractionRing A) y = x
⊢ IsIntegrallyClosed A

Tactic:
refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)

Premises used: Iff.mpr, FractionRing, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
rw : x ∈ (↑(adjoinIntegral A⁰ x hx) : Submodule A (FractionRing A))
rw₁ : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (adjoinIntegral A⁰ x hx) 0
⊢ ∃ (y : A), (algebraMap A (FractionRing A) : (a : A) → FractionRing A) y = x

Tactic:
rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
    Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
    FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)]

Premises used: Set.mem_range, Ne.isUnit, Algebra.mem_bot, Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot, nonZeroDivisors, FractionalIdeal.coe_spanSingleton, FractionalIdeal.spanSingleton_one, OfNat.ofNat, FractionalIdeal.adjoinIntegral_eq_one_of_isUnit, Submodule.one_eq_span
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ (↑(adjoinIntegral A⁰ x hx) : Submodule A (FractionRing A))

Tactic:
mem_adjoinIntegral_self A⁰ x hx

Premises used: FractionalIdeal.mem_adjoinIntegral_self, Set.Mem, setOf, nonZeroDivisors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ (↑(adjoinIntegral A⁰ x hx) : Submodule A (FractionRing A))

Tactic:
exact mem_adjoinIntegral_self A⁰ x hx

Premises used: FractionalIdeal.mem_adjoinIntegral_self, nonZeroDivisors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
⊢ Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (adjoinIntegral A⁰ x hx) 0

Tactic:
fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)

Premises used: FractionalIdeal.eq_zero_iff, Algebra.adjoin, Iff.mp, one_ne_zero, Singleton.singleton, OfNat.ofNat, Subalgebra.one_mem, Not
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
⊢ Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (adjoinIntegral A⁰ x hx) 0

Tactic:
exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)

Premises used: FractionalIdeal.eq_zero_iff, Iff.mp, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
maximalOfPrime : ∀ {p : Ideal A}, p ≠ ⊥ → p.IsPrime → p.IsMaximal
⊢ DimensionLEOne A

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
⊢ P.IsMaximal

Tactic:
Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩

Premises used: Iff.mpr, And.intro, Ideal.IsPrime.ne_top, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
maximalOfPrime : ∀ (M : Ideal A) (hM : P < M), M = ⊤
⊢ P.IsMaximal

Tactic:
refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩

Premises used: Iff.mpr, And.intro, Ideal.IsPrime.ne_top, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
⊢ Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0

Tactic:
have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0

Tactic:
have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this_1 : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0
M'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : FractionalIdeal A⁰ (FractionRing A))
rw : LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑M : FractionalIdeal A⁰ (FractionRing A))
⊢ M = ⊤

Tactic:
rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]

Premises used: FractionalIdeal.coeIdeal_top, eq_top_iff, FractionRing, FractionalIdeal.coeIdeal_le_coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this_1 : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0
M'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : FractionalIdeal A⁰ (FractionRing A))
⊢ 1 =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑P : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑M : FractionalIdeal A⁰ (FractionRing A))

Tactic:
simp [mul_assoc, *]

Premises used: mul_assoc