awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have 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
Tactic: rcases I.exists_le_maximal hI1 with ⟨M, hmax, hIM⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have hMbot : M ≠ ⊥
Tactic: have hMbot : M ≠ ⊥ := (M.bot_lt_of_maximal hNF).ne'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
have inr : Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) 0
Tactic: refine mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have inr₁ : Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑M : FractionalIdeal A⁰ K) 0
Tactic: refine mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have inr₂ : LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑M : FractionalIdeal A⁰ K)
Tactic: refine mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have hI0₁ : ⊥ < I
Tactic: have hI0 : ⊥ < I := I.bot_lt_of_maximal hNF
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have 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
Tactic: obtain ⟨⟨a, haI⟩, ha0⟩ := Submodule.nonzero_mem_of_bot_lt hI0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have ha0₁ : a ≠ 0
Tactic: replace ha0 : a ≠ 0 := Subtype.coe_injective.ne ha0
Cleared hypotheses: ha0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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}
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have hJ0 : J ≠ ⊥
Tactic: have hJ0 : J ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp ha0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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 ≠ ⊥
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have hJI : J ≤ I
Tactic: have hJI : J ≤ I := I.span_singleton_le_iff_mem.2 haI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have 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
Tactic: obtain ⟨Z, hle, hnle⟩ := PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le hNF hJ0 hJI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have 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
Tactic: obtain ⟨b, hbZ, hbJ⟩ := SetLike.not_le_iff_exists.mp hnle
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ 1
have hnz_fa : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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₀
⊢ 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₀)
have 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))
Tactic: obtain ⟨y, h_Iy, rfl⟩ := (mem_coeIdeal _).mp hy₀
Cleared hypotheses: y₀, hy₀
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: rw [mul_comm, ← mul_assoc, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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 ∈ J
have a₁ : y * b ∈ (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod
Tactic: apply hle
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
have a₁ : y * b ∈ I * (Multiset.map PrimeSpectrum.asIdeal Z).prod
Tactic: rw [Multiset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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)
⊢ 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))
have h_yb : y * b ∈ J
Tactic: have h_yb : y * b ∈ J := by
      apply hle
      rw [Multiset.prod_cons]
      exact Submodule.smul_mem_smul h_Iy hbZ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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)
h_yb : y * b ∈ J
⊢ 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))
have h_yb₁ : ∃ (a_1 : A), a_1 * a = y * b
Tactic: rw [Ideal.mem_span_singleton'] at h_yb
Cleared hypotheses: h_yb
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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)
h_yb : ∃ (a_1 : A), a_1 * a = y * b
⊢ 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))
have refine_2 : ∀ (c : A) (hc : c * a = y * b),
  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))
Tactic: rcases h_yb with ⟨c, hc⟩
Cleared hypotheses: h_yb
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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)
c : A
hc : c * a = y * b
⊢ 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))
have refine_2 : Membership.mem.{u_3, u_3} (α := K) (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1
  ((algebraMap A K : (a : A) → K) c : K)
Tactic: rw [← hc, map_mul, mul_assoc, mul_inv_cancel₀ hnz_fa, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K) ∉
    (↑1 : Set K)
have refine_3 : ¬∃ (x' : A),
    (algebraMap A K : (a : A) → K) x' =
      HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K)
Tactic: refine mt (mem_one_iff _).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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)
x' : A
h₂_abs :
  (algebraMap A K : (a : A) → K) x' =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (((algebraMap A K : (a : A) → K) a)⁻¹ : K)
⊢ False
have h₂_abs₁ : Eq.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) (x' * a) : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: rw [← div_eq_mul_inv, eq_div_iff_mul_eq hnz_fa, ← map_mul] at h₂_abs
Cleared hypotheses: h₂_abs
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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)
x' : A
h₂_abs : Eq.{u_3 + 1} (α := K) ((algebraMap A K : (a : A) → K) (x' * a) : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ False
have this : Membership.mem (γ := Ideal A) (span {a}) b
Tactic: have := Ideal.mem_span_singleton'.mpr ⟨x', IsFractionRing.injective A K h₂_abs⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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 ≠ ⊥
hI :
  (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹ ≤
    1
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1
have obtain : ∀ (J : Ideal A)
  (hJ :
    (↑J : FractionalIdeal A⁰ K) =
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹),
  HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
    1
Tactic: obtain ⟨J, hJ⟩ : ∃ J : Ideal A, (J : FractionalIdeal A⁰ K) = I * (I : FractionalIdeal A⁰ K)⁻¹ :=
    le_one_iff_exists_coeIdeal.mp mul_one_div_le_one