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_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))
⊢ 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)) ≤
    (↑P : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑M : FractionalIdeal A⁰ (FractionRing A))

Tactic:
gcongr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
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))
⊢ (↑P : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑M : FractionalIdeal A⁰ (FractionRing A)) =
    (↑M : FractionalIdeal A⁰ (FractionRing A))

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
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))
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))
⊢ LE.le (α := _root_.FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑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 [*]

Premises used: HMul.hMul, Inv.inv, OfNat.ofNat
-- 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
maximalOfPrime :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    (↑P : FractionalIdeal A⁰ (FractionRing A))
⊢ M = ⊤

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 [*]
-- 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
x : FractionRing A
hx :
  x ∈
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A))
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))
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑P : FractionalIdeal A⁰ (FractionRing A)) ≤
    1

Tactic:
rw [← inv_mul_cancel₀ M'_ne]

Premises used: inv_mul_cancel₀
-- 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
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)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑M : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑M : FractionalIdeal A⁰ (FractionRing A))

Tactic:
gcongr
-- 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
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

Tactic:
have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 := by
    rw [← inv_mul_cancel₀ M'_ne]; gcongr
-- 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
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
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)
⊢ Membership.mem (γ := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑P : FractionalIdeal A⁰ (FractionRing A)) x

Tactic:
obtain ⟨y, _hy, rfl⟩ := (mem_coeIdeal _).mp (le_one hx)

Premises used: FractionalIdeal.mem_coeIdeal, Iff.mp, rfl
-- 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)
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)
⊢ 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

Premises used: SetLike.exists_of_lt
-- 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
⊢ 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
-- 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 :
  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) (z * y) : FractionRing A)

Tactic:
rw [← map_mul, ← mul_assoc, mul_inv_cancel₀ M'_ne, one_mul] at zy_mem

Premises used: mul_inv_cancel₀, mul_assoc, map_mul, one_mul
-- 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)
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)
⊢ 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

Premises used: nonZeroDivisors, FractionalIdeal.mem_coeIdeal, Iff.mp
-- 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 : 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)
⊢ z * y ∈ P

Tactic:
rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy

Premises used: IsFractionRing.injective, FractionRing
-- 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 : 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)
hzy₁ : z * y ∈ P
⊢ 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)

Tactic:
rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy

Premises used: IsFractionRing.injective, FractionRing
-- 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:
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