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 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    0
pos : LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 0 1
⊢ (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1

Tactic:
rw [hJ0, inv_zero']

Premises used: FractionalIdeal.inv_zero'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    0
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 0 1

Tactic:
zero_le _

Premises used: FractionalIdeal.zero_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    0
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 0 1

Tactic:
exact zero_le _

Premises used: FractionalIdeal.zero_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
this : Membership.mem (γ := Subalgebra A K) (integralClosure A K) x
rwa :
  ∀ (this : Membership.mem (γ := Subalgebra A K) ⊥ x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
rwa₁ :
  ∀ (this : Membership.mem (γ := Set K) (Set.range.{u_3, u_2 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)) x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
rwa₂ :
  ∀ (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
rwa₃ :
  ∀ (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x)
    (this : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
S : (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x) → Submonoid A
rwa₄ :
  ∀ (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x)
    (this : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
S₁ : (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x) → Submonoid A
rwa₅ :
  ∀ (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x)
    (this : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
S₂ : (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x) → Submonoid A
rwa₆ :
  ∀ (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x)
    (this : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x
S₃ : (this : ∃ (y : A), (algebraMap A K : (a : A) → K) y = x) → Submonoid A
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x

Tactic:
rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
      ← mem_one_iff] at this

Premises used: Set.mem_range, Algebra.mem_bot, FractionalIdeal.mem_one_iff, IsIntegrallyClosed.integralClosure_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
neg : Membership.mem (γ := Subalgebra A K) (integralClosure A K) x
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 x

Tactic:
suffices x ∈ integralClosure A K by
    rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range,
      ← mem_one_iff] at this
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
neg :
  ∃ (M : Subalgebra A K),
    Submodule.FG.{u_2, u_3} (R := A) (M := K) ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) M) ∧
      x ∈ M
⊢ Membership.mem (γ := Subalgebra A K) (integralClosure A K) x

Tactic:
rw [mem_integralClosure_iff_mem_fg]

Premises used: mem_integralClosure_iff_mem_fg
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
b : K
hb : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b
rw :
  ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * b * y)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)

Tactic:
rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI0)]

Premises used: Iff.mpr, FractionalIdeal.coeIdeal_ne_zero, FractionalIdeal.mem_inv_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
b : K
hb : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b
rw :
  ∀
    (hx :
      ∀
        y ∈
          HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
            (↑I : FractionalIdeal A⁰ K)⁻¹,
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * y))
    (b : K) (hb : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b)
    (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * b * y)
⊢ ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * b * y)

Tactic:
rw [mem_inv_iff hJ0] at hx

Premises used: FractionalIdeal.mem_inv_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  ∀
    y ∈
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹,
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * y)
b : K
hb : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b
simp_rw :
  ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * (y * b))
⊢ ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * b * y)

Tactic:
simp_rw [mul_assoc, mul_comm b]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  ∀
    y ∈
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹,
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * y)
b : K
hb : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b
⊢ ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * (y * b))

Tactic:
fun y hy ↦ hx _ (mul_mem_mul hy hb)

Premises used: HMul.hMul, Set.Mem, FractionalIdeal.mul_mem_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 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  ∀
    y ∈
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹,
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * y)
b : K
hb : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b
⊢ ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (x * (y * b))

Tactic:
exact fun y hy ↦ hx _ (mul_mem_mul hy hb)

Premises used: HMul.hMul, FractionalIdeal.mul_mem_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 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
⊢ ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)

Tactic:
have x_mul_mem : ∀ b ∈ (I⁻¹ : FractionalIdeal A⁰ K), x * b ∈ (I⁻¹ : FractionalIdeal A⁰ K) := by
    intro b hb
    rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI0)]
    rw [mem_inv_iff hJ0] at hx
    simp_rw [mul_assoc, mul_comm b]
    exact fun y hy ↦ hx _ (mul_mem_mul hy hb)
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
⊢ ∃ (M : Subalgebra A K),
    Submodule.FG.{u_2, u_3} (R := A) (M := K) ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) M) ∧
      x ∈ M

Tactic:
⟨AlgHom.range (Polynomial.aeval x : A[X] →ₐ[A] K),
    isNoetherian_submodule.mp (isNoetherian (I : FractionalIdeal A⁰ K)⁻¹) _ fun y hy => ?_,
    ⟨Polynomial.X, Polynomial.aeval_X x⟩⟩

Premises used: isNoetherian_submodule, Inv.inv, And.intro, Exists.intro, Iff.mp, FractionalIdeal.isNoetherian, Polynomial.aeval, Polynomial.X, FractionalIdeal.coeIdeal, AlgHom.range, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
neg :
  ∀ (y : K)
    (hy :
      Membership.mem (γ := Submodule A K)
        ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
          Submodule A K)
        y),
    Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) y
⊢ ∃ (M : Subalgebra A K),
    Submodule.FG.{u_2, u_3} (R := A) (M := K) ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) M) ∧
      x ∈ M

Tactic:
refine ⟨AlgHom.range (Polynomial.aeval x : A[X] →ₐ[A] K),
    isNoetherian_submodule.mp (isNoetherian (I : FractionalIdeal A⁰ K)⁻¹) _ fun y hy => ?_,
    ⟨Polynomial.X, Polynomial.aeval_X x⟩⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
y : K
hy :
  Membership.mem (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    y
neg :
  ∀ (p : A[X])
    (hy :
      Membership.mem (α := K) (γ := Submodule A K)
        ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
          Submodule A K)
        ((Polynomial.aeval x : (a : A[X]) → K) p : K)),
    Membership.mem.{u_3, u_3} (α := K) (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K)
      ((Polynomial.aeval x : (a : A[X]) → K) p : K)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) y

Tactic:
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp hy

Premises used: AlgHom.mem_range, Iff.mp, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
neg :
  Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K)
    (∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i)
⊢ Membership.mem.{u_3, u_3} (α := K) (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)

Tactic:
rw [Polynomial.aeval_eq_sum_range]

Premises used: Polynomial.aeval_eq_sum_range
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K)
    (∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i)

Tactic:
Submodule.sum_mem _ fun i hi => Submodule.smul_mem _ _ ?_

Premises used: Set.Mem, Submodule.sum_mem, Polynomial.coeff, FractionalIdeal.coeToSubmodule, Inv.inv, FractionalIdeal.coeIdeal, Submodule.smul_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
neg :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (p.natDegree + 1)),
    Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ i)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K)
    (∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i)

Tactic:
refine Submodule.sum_mem _ fun i hi => Submodule.smul_mem _ _ ?_

Premises used: Submodule.sum_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
neg : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) 1
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (HPow.hPow (β := ℕ) x 0)

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) 1

Tactic:
one_mem_inv_coe_ideal hI0

Premises used: Set.Mem, FractionalIdeal.one_mem_inv_coe_ideal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) 1

Tactic:
exact one_mem_inv_coe_ideal hI0

Premises used: FractionalIdeal.one_mem_inv_coe_ideal