awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0
le_one :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
y : A
_hy : Membership.mem (γ := Ideal A) ⊤ y
hx :
  Membership.mem (α := FractionRing A)
    (HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)))
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)
z : A
hzM : z ∈ M
hzp : z ∉ P
zy_mem :
  Membership.mem (α := FractionRing A) (γ := FractionalIdeal (R := A) A⁰ (FractionRing A))
    (↑P : FractionalIdeal A⁰ (FractionRing A))
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (z * y) : FractionRing A)
zy : A
hzy : z * y ∈ P
zy_eq :
  Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) zy : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (z * y) : FractionRing A)
⊢ Membership.mem (α := FractionRing A) (γ := FractionalIdeal (R := A) A⁰ (FractionRing A))
    (↑P : FractionalIdeal A⁰ (FractionRing A))
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)

Tactic:
exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp)

Premises used: nonZeroDivisors, Or.resolve_left, FractionalIdeal.mem_coeIdeal_of_mem, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
⊢ IsDedekindDomain A

Tactic:
{ h.isNoetherianRing, h.dimensionLEOne, h.integrallyClosed with }

Premises used: IsDedekindDomainInv.isNoetherianRing, IsDedekindDomainInv.dimensionLEOne, IsDedekindDomainInv.integrallyClosed, IsDedekindDomain.mk
-- 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 : IsDomain A
I : Ideal A
hI : I ≠ ⊥
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 (1 * y)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

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

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 : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y
rw : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 y
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (1 * y)

Tactic:
rw [one_mul]

Premises used: one_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 : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : 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 y

Tactic:
coeIdeal_le_one hy

Premises used: FractionalIdeal.coeIdeal_le_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 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
I : Ideal A
hI : I ≠ ⊥
y : K
hy : 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 y

Tactic:
exact coeIdeal_le_one hy

Premises used: FractionalIdeal.coeIdeal_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
obtain :
  ∀ (Z₀ : Multiset (PrimeSpectrum A)) (hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥),
    ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
obtain ⟨Z₀, hZ₀⟩ := exists_primeSpectrum_prod_le_and_ne_bot_of_domain hNF hI0

Premises used: PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
obtain :
  ∀ (Z : Multiset (PrimeSpectrum A))
    (h_eraseZ :
      ∀ (x : Multiset (PrimeSpectrum A)),
        Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
            {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
          ¬x < Z)
    (hZI : (Multiset.map asIdeal Z).prod ≤ I) (hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥),
    ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
obtain ⟨Z, ⟨hZI, hprodZ⟩, h_eraseZ⟩ :=
    wellFounded_lt.has_min
      {Z | (Z.map asIdeal).prod ≤ I ∧ (Z.map asIdeal).prod ≠ ⊥}
      ⟨Z₀, hZ₀.1, hZ₀.2⟩

Premises used: setOf, Ne, Bot.bot, LE.le, And, wellFounded_lt, And.intro, Exists.intro, WellFounded.has_min
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
obtain :
  ∀ (w : Ideal A) (hPZ' : w ∈ Multiset.map asIdeal Z) (hPM : w ≤ M),
    ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
obtain ⟨_, hPZ', hPM⟩ := hM.isPrime.multiset_prod_le.mp (hZI.trans hIM)

Premises used: Ideal.IsMaximal.isPrime, Ideal.IsPrime.multiset_prod_le, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
w : Ideal A
hPZ' : w ∈ Multiset.map asIdeal Z
hPM : w ≤ M
obtain :
  ∀ (P : PrimeSpectrum A) (hPZ : P ∈ Z) (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M),
    ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
obtain ⟨P, hPZ, rfl⟩ := Multiset.mem_map.mp hPZ'

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
⊢ Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal

Tactic:
have := Multiset.map_erase asIdeal (fun _ _ => PrimeSpectrum.ext) P Z
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
rwa :
  ∀ (hprodZ : ¬(Multiset.map asIdeal Z).prod = ⊥) (P : PrimeSpectrum A) (hPZ : P ∈ Z)
    (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M)
    (this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal),
    P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
rwa₁ :
  ∀ (P : PrimeSpectrum A) (hprodZ : ¬(P.asIdeal ::ₘ (Multiset.map asIdeal Z).erase P.asIdeal).prod = ⊥) (hPZ : P ∈ Z)
    (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M)
    (this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal),
    P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
rwa₂ :
  ∀ (P : PrimeSpectrum A) (hprodZ : ¬P.asIdeal * ((Multiset.map asIdeal Z).erase P.asIdeal).prod = ⊥) (hPZ : P ∈ Z)
    (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M)
    (this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal),
    P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
rwa₃ :
  ∀ (P : PrimeSpectrum A) (hprodZ : ¬(P.asIdeal = ⊥ ∨ ((Multiset.map asIdeal Z).erase P.asIdeal).prod = ⊥))
    (hPZ : P ∈ Z) (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M)
    (this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal),
    P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
rwa₄ :
  ∀ (P : PrimeSpectrum A) (hprodZ : ¬P.asIdeal = ⊥ ∧ ¬((Multiset.map asIdeal Z).erase P.asIdeal).prod = ⊥) (hPZ : P ∈ Z)
    (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M)
    (this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal),
    P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (P : PrimeSpectrum A) (hprodZ : ¬P.asIdeal = ⊥ ∧ ¬(Multiset.map asIdeal (Z.erase P)).prod = ⊥) (hPZ : P ∈ Z)
    (hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z) (hPM : P.asIdeal ≤ M)
    (this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal),
    P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
⊢ P.asIdeal ≠ ⊥ ∧ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥

Tactic:
rwa [Ne, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ←
        this] at hprodZ

Premises used: Multiset.prod_cons, Ne, not_or, Multiset.cons_erase, Ideal.mul_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
⊢ P.asIdeal ≠ ⊥

Tactic:
obtain ⟨hP0, hZP0⟩ : P.asIdeal ≠ ⊥ ∧ ((Z.erase P).map asIdeal).prod ≠ ⊥ := by
      rwa [Ne, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ←
        this] at hprodZ

Premises used: Multiset.map, Multiset.prod, Multiset.erase, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
⊢ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥

Tactic:
obtain ⟨hP0, hZP0⟩ : P.asIdeal ≠ ⊥ ∧ ((Z.erase P).map asIdeal).prod ≠ ⊥ := by
      rwa [Ne, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ←
        this] at hprodZ

Premises used: Multiset.map, Multiset.prod, Multiset.erase, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
⊢ P.asIdeal = M

Tactic:
have hPM' := (P.isPrime.isMaximal hP0).eq_of_le hM.ne_top hPM
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I M : Ideal A
hI0 : I ≠ ⊥
hIM : I ≤ M
hM : M.IsMaximal
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
hPM : P.asIdeal ≤ M
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hPM' : P.asIdeal = M
subst :
  ∀ (hIM : I ≤ P.asIdeal) [hM : P.asIdeal.IsMaximal] (hPM : P.asIdeal ≤ P.asIdeal),
    ∃ (Z : Multiset (PrimeSpectrum A)),
      (P.asIdeal ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (M ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
subst hPM'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ ∃ (Z : Multiset (PrimeSpectrum A)),
    (P.asIdeal ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
⟨Z.erase P, ?_, ?_⟩

Premises used: And.intro, Multiset.erase, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
refine_1 : (P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P)).prod ≤ I
refine_2 : ¬(Multiset.map asIdeal (Z.erase P)).prod ≤ I
⊢ ∃ (Z : Multiset (PrimeSpectrum A)),
    (P.asIdeal ::ₘ Multiset.map asIdeal Z).prod ≤ I ∧ ¬(Multiset.map asIdeal Z).prod ≤ I

Tactic:
refine ⟨Z.erase P, ?_, ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ (Multiset.map asIdeal Z).prod ≤ I

Tactic:
hZI
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
h : P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P) = Multiset.map asIdeal Z
⊢ (P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P)).prod ≤ I

Tactic:
convert! hZI
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
h : P.asIdeal ::ₘ (Multiset.map asIdeal Z).erase P.asIdeal = Multiset.map asIdeal Z
h₁ h₂ : Multiset.map asIdeal Z = Multiset.map asIdeal Z
⊢ P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P) = Multiset.map asIdeal Z

Tactic:
rw [this, Multiset.cons_erase hPZ']

Premises used: Multiset.cons_erase
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ :
  ∀ (x : Multiset (PrimeSpectrum A)),
    Membership.mem (γ := Set (Multiset (PrimeSpectrum A)))
        {Z : Multiset (PrimeSpectrum A) | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥} x →
      ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ ¬(Multiset.map asIdeal (Z.erase P)).prod ≤ I

Tactic:
fun h => h_eraseZ (Z.erase P) ⟨h, ?_⟩ (Multiset.erase_lt.mpr hPZ)

Premises used: Iff.mpr, Multiset.erase_lt, And.intro, Multiset.erase, Not