awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : ∀ (h : (Multiset.map asIdeal (Z.erase P)).prod ≤ I), (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
⊢ ¬(Multiset.map asIdeal (Z.erase P)).prod ≤ I

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

Premises used: Iff.mpr, Multiset.erase_lt, And.intro, Multiset.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
h : (Multiset.map asIdeal (Z.erase P)).prod ≤ I
⊢ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥

Tactic:
hZP0
-- 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 : (Multiset.map asIdeal (Z.erase P)).prod ≤ I
⊢ (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥

Tactic:
exact hZP0
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
⊢ ¬IsField A

Tactic:
have hNF : ¬IsField A := fun h ↦ letI := h.toField; (eq_bot_or_eq_top I).elim hI0 hI1
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
inr :
  ∀
    (this :
      ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
        ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1)
    (hM : ¬I.IsMaximal), ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
wlog :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
wlog hM : I.IsMaximal generalizing I

Premises used: Ideal.IsMaximal
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
inr :
  ∀ (M : Ideal A) (hmax : M.IsMaximal) (hIM : I ≤ M),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
rcases I.exists_le_maximal hI1 with ⟨M, hmax, hIM⟩

Premises used: Ideal.exists_le_maximal
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
⊢ M ≠ ⊥

Tactic:
have hMbot : M ≠ ⊥ := (M.bot_lt_of_maximal hNF).ne'
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax)

Premises used: FractionalIdeal.inv_anti_mono, mt, Ideal.IsMaximal.ne_top, le_trans
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
inr : Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) 0
inr₁ : Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑M : FractionalIdeal A⁰ K) 0
inr₂ :
  LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑M : FractionalIdeal A⁰ K)
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
refine mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax)

Premises used: FractionalIdeal.inv_anti_mono, mt, Ideal.IsMaximal.ne_top, le_trans
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) 0

Tactic:
simpa only [coeIdeal_ne_zero, coeIdeal_le_coeIdeal]

Premises used: FractionalIdeal.coeIdeal_ne_zero, FractionalIdeal.coeIdeal_le_coeIdeal
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑M : FractionalIdeal A⁰ K) 0

Tactic:
simpa only [coeIdeal_ne_zero, coeIdeal_le_coeIdeal]

Premises used: FractionalIdeal.coeIdeal_ne_zero, FractionalIdeal.coeIdeal_le_coeIdeal
-- 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 ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this :
  ∀ {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (hM : I.IsMaximal),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
hM : ¬I.IsMaximal
M : Ideal A
hmax : M.IsMaximal
hIM : I ≤ M
hMbot : M ≠ ⊥
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑M : FractionalIdeal A⁰ K)

Tactic:
simpa only [coeIdeal_ne_zero, coeIdeal_le_coeIdeal]

Premises used: FractionalIdeal.coeIdeal_ne_zero, FractionalIdeal.coeIdeal_le_coeIdeal
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
⊢ ⊥ < I

Tactic:
have hI0 : ⊥ < I := I.bot_lt_of_maximal hNF
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
obtain :
  ∀ (a : A) (haI : a ∈ I) (ha0 : Subtype.mk (p := fun (x : A) ↦ x ∈ I) a haI ≠ 0),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
obtain ⟨⟨a, haI⟩, ha0⟩ := Submodule.nonzero_mem_of_bot_lt hI0

Premises used: Submodule.nonzero_mem_of_bot_lt
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : Subtype.mk (p := fun (x : A) ↦ x ∈ I) a haI ≠ 0
⊢ a ≠ 0

Tactic:
replace ha0 : a ≠ 0 := Subtype.coe_injective.ne ha0
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
⊢ J ≠ ⊥

Tactic:
have hJ0 : J ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp ha0
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
⊢ J ≤ I

Tactic:
have hJI : J ≤ I := I.span_singleton_le_iff_mem.2 haI
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
obtain :
  ∀ (Z : Multiset (PrimeSpectrum A)) (hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J)
    (hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
obtain ⟨Z, hle, hnle⟩ := PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le hNF hJ0 hJI

Premises used: PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
obtain :
  ∀ (b : A) (hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod) (hbJ : b ∉ J),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
obtain ⟨b, hbZ, hbJ⟩ := SetLike.not_le_iff_exists.mp hnle

Premises used: Iff.mp, SetLike.not_le_iff_exists
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
⊢ Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)

Tactic:
have hnz_fa : algebraMap A K a ≠ 0 :=
    mt ((injective_iff_map_eq_zero _).mp (IsFractionRing.injective A K) a) ha0
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1

Tactic:
Set.not_subset.2 ⟨algebraMap A K b * (algebraMap A K a)⁻¹, (mem_inv_iff ?_).mpr ?_, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Algebra.algebraMap, Set.Subset, Inv.inv, And.intro, Set.not_subset, Exists.intro, DFunLike.coe, 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) 0

Tactic:
coeIdeal_ne_zero.mpr hI0.ne'

Premises used: Iff.mpr, LT.lt.ne', FractionalIdeal.coeIdeal_ne_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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) 0

Tactic:
exact coeIdeal_ne_zero.mpr hI0.ne'

Premises used: Iff.mpr, LT.lt.ne', FractionalIdeal.coeIdeal_ne_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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y₀ : K
hy₀ : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) y₀
refine_2 :
  ∀ (y : A) (h_Iy : y ∈ I)
    (hy₀ :
      Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        ((algebraMap A K : (a : A) → K) y : K)),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K))
        ((algebraMap A K : (a : A) → K) y : K))
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K) * y₀)

Tactic:
obtain ⟨y, h_Iy, rfl⟩ := (mem_coeIdeal _).mp hy₀

Premises used: FractionalIdeal.mem_coeIdeal, 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
refine_2 :
  Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (y * b) : K)
      (((algebraMap A K : (a : A) → K) a)⁻¹ : K))
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
    (HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K))
      ((algebraMap A K : (a : A) → K) y : K))

Tactic:
rw [mul_comm, ← mul_assoc, ← map_mul]

Premises used: mul_assoc, map_mul, 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
a₁ : y * b ∈ (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod
⊢ y * b ∈ J

Tactic:
apply hle
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
a₁ : y * b ∈ I * (Multiset.map PrimeSpectrum.asIdeal Z).prod
⊢ y * b ∈ (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod

Tactic:
rw [Multiset.prod_cons]

Premises used: Multiset.prod_cons
-- 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_1 : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0_1 : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : Ne.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) (0 : K)
y : A
h_Iy : y ∈ I
hy₀ :
  Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
⊢ y * b ∈ I * (Multiset.map PrimeSpectrum.asIdeal Z).prod

Tactic:
Submodule.smul_mem_smul h_Iy hbZ

Premises used: Set.Mem, Submodule.smul_mem_smul