awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
I : Ideal A
hI : ¬I = ⊥
⊢ Submodule.FG I
have hI₁ : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
Tactic: have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
⊢ IsIntegrallyClosed A
have refine : ∀ {x : FractionRing A} {hx : IsIntegral A x},
  ∃ (y : A), (algebraMap A (FractionRing A) : (a : A) → FractionRing A) y = x
Tactic: refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
⊢ ∃ (y : A), (algebraMap A (FractionRing A) : (a : A) → FractionRing A) y = x
have rw : x ∈ (↑(adjoinIntegral A⁰ x hx) : Submodule A (FractionRing A))
Tactic: rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
    Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
    FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
x : FractionRing A
hx : IsIntegral A x
rw : x ∈ (↑(adjoinIntegral A⁰ x hx) : Submodule A (FractionRing A))
⊢ ∃ (y : A), (algebraMap A (FractionRing A) : (a : A) → FractionRing A) y = x
have rw₁ : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (adjoinIntegral A⁰ x hx) 0
Tactic: rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
    Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
    FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (Ne.isUnit _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ DimensionLEOne A
have maximalOfPrime : ∀ {p : Ideal A}, p ≠ ⊥ → p.IsPrime → p.IsMaximal
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
⊢ P.IsMaximal
have maximalOfPrime : ∀ (M : Ideal A) (hM : P < M), M = ⊤
Tactic: refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
⊢ M = ⊤
have P'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0
Tactic: have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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 = ⊤
have M'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0
Tactic: have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this_1 : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0
M'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : FractionalIdeal A⁰ (FractionRing A))
⊢ M = ⊤
have rw : LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑M : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this_1 : CommGroupWithZero (FractionalIdeal (R := A) A⁰ (FractionRing A)) := h.commGroupWithZero
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) 0
M'_ne : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : FractionalIdeal A⁰ (FractionRing A))
⊢ LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑M : FractionalIdeal A⁰ (FractionRing A))
have FractionalIdeal : 1 =
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) *
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑M : FractionalIdeal A⁰ (FractionRing A))
Tactic: calc
      (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by
        simp [mul_assoc, *]
      _ ≤ P * ((↑P)⁻¹ * M) := by gcongr
      _ = M := by simp [*]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this_1 : CommGroupWithZero (_root_.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 (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) 0
M'_ne :
  Ne (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : _root_.FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))
FractionalIdeal :
  1 =
    HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
⊢ LE.le (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
have FractionalIdeal₁ : HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
    HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A)) ≤
  (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
    HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
Tactic: calc
      (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by
        simp [mul_assoc, *]
      _ ≤ P * ((↑P)⁻¹ * M) := by gcongr
      _ = M := by simp [*]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainInv A
this_1 : CommGroupWithZero (_root_.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 (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) 0
M'_ne :
  Ne (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : _root_.FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))
FractionalIdeal :
  1 =
    HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
FractionalIdeal₁ :
  HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
        (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
⊢ LE.le (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
have FractionalIdeal₂ : (↑P : _root_.FractionalIdeal A⁰ (FractionRing A)) *
    HMul.hMul (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑P : _root_.FractionalIdeal A⁰ (FractionRing A))⁻¹ (↑M : _root_.FractionalIdeal A⁰ (FractionRing A)) =
  (↑M : _root_.FractionalIdeal A⁰ (FractionRing A))
Tactic: calc
      (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by
        simp [mul_assoc, *]
      _ ≤ P * ((↑P)⁻¹ * M) := by gcongr
      _ = M := by simp [*]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
⊢ M = ⊤
have maximalOfPrime : HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
  (↑P : FractionalIdeal A⁰ (FractionRing A))
Tactic: suffices (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ P by
    rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]
    calc
      (1 : FractionalIdeal A⁰ (FractionRing A)) = (↑M)⁻¹ * P * ((↑P)⁻¹ * M) := by
        simp [mul_assoc, *]
      _ ≤ P * ((↑P)⁻¹ * M) := by gcongr
      _ = M := by simp [*]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
x : FractionRing A
hx :
  x ∈
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A))
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
have rw : HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑M : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [← inv_mul_cancel₀ M'_ne]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
x : FractionRing A
hx :
  x ∈
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A))
⊢ Membership.mem (γ := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) x
have le_one : HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
  1
Tactic: have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 := by
    rw [← inv_mul_cancel₀ M'_ne]; gcongr
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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
x : FractionRing A
hx :
  x ∈
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A))
le_one :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
⊢ Membership.mem (γ := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) x
have maximalOfPrime : ∀ (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)),
  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: obtain ⟨y, _hy, rfl⟩ := (mem_coeIdeal _).mp (le_one hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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)
⊢ 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)
have maximalOfPrime : ∀ (z : A) (hzM : z ∈ M) (hzp : z ∉ P),
  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: obtain ⟨z, hzM, hzp⟩ := SetLike.exists_of_lt hM
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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
⊢ 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)
have zy_mem : HMul.hMul (α := FractionRing A) (β := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) z : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A) ∈
  (↑M : FractionalIdeal A⁰ (FractionRing A)) *
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A))
Tactic: have zy_mem := mul_mem_mul (mem_coeIdeal_of_mem A⁰ hzM) hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
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 :
  HMul.hMul (α := FractionRing A) (β := FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) z : FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A) ∈
    (↑M : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑P : FractionalIdeal A⁰ (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)
have 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)
Tactic: rw [← map_mul, ← mul_assoc, mul_inv_cancel₀ M'_ne, one_mul] at zy_mem
Cleared hypotheses: zy_mem
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
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)
⊢ 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)
have maximalOfPrime : ∀ (zy : A) (hzy : zy ∈ 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: obtain ⟨zy, hzy, zy_eq⟩ := (mem_coeIdeal A⁰).mp zy_mem