awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K_1 : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K_1
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : { x : Ideal A // 0 < x }
J K : Ideal A
e :
  (fun (x1 x2 : Ideal A) ↦ x1 ≤ x2) ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I J)
    ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I K)
rwa :
  LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑K : FractionalIdeal A⁰ (FractionRing A))
rwa₁ :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A))
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A)) (↑K : FractionalIdeal A⁰ (FractionRing A))
rwa₂ :
  (↑((↑I : Ideal A) * J) : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A)) (↑K : FractionalIdeal A⁰ (FractionRing A))
rwa₃ :
  LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A))
    (↑((↑I : Ideal A) * J) : FractionalIdeal A⁰ (FractionRing A))
    (↑((↑I : Ideal A) * K) : FractionalIdeal A⁰ (FractionRing A))
rwa₄ rwa₅ rwa₆ rwa₇ : (↑I : Ideal A) * J ≤ (↑I : Ideal A) * K
⊢ J ≤ K

Tactic:
rwa [← FractionalIdeal.coeIdeal_le_coeIdeal (FractionRing A),
      ← mul_le_mul_iff_right₀ (α := FractionalIdeal A⁰ (FractionRing A)) (a := I.1)
        (by simpa [pos_iff_ne_zero] using I.2.ne'),
      ← FractionalIdeal.coeIdeal_mul, ← FractionalIdeal.coeIdeal_mul,
      FractionalIdeal.coeIdeal_le_coeIdeal]

Premises used: FractionRing, FractionalIdeal.coeIdeal_mul, mul_le_mul_iff_right₀, FractionalIdeal.coeIdeal_le_coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDomain A
⊢ IsDedekindDomain A ↔ IsDedekindDomainInv A

Tactic:
⟨fun _h _I => mul_inv_cancel₀, fun h => h.isDedekindDomain⟩

Premises used: mul_inv_cancel₀, Iff.intro, IsDedekindDomainInv.isDedekindDomain
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ IsCancelMulZero.{u_2} (Ideal A)

Tactic:
Function.Injective.isCancelMulZero (coeIdealHom A⁰ (FractionRing A)) coeIdeal_injective
    (map_zero _) (map_mul _)

Premises used: Function.Injective.isCancelMulZero, FractionRing, nonZeroDivisors, map_zero, FractionalIdeal.coeIdeal_injective, map_mul, DFunLike.coe, FractionalIdeal.coeIdealHom
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ PosMulStrictMono.{u_2} (Ideal A)

Tactic:
PosMulMono.toPosMulStrictMono

Premises used: Set.Mem, PosMulMono.toPosMulStrictMono
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ MulPosStrictMono.{u_2} (Ideal A)

Tactic:
MulPosMono.toMulPosStrictMono

Premises used: Set.Mem, MulPosMono.toMulPosStrictMono
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
pos : ∀ (hI : I = ⊥), I ∣ J
neg : ∀ (hI : ¬I = ⊥), I ∣ J
⊢ I ∣ J

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
rwa : ∀ (h : J ≤ ⊥) (hI : I = ⊥), J = ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : J = ⊥) (hI : I = ⊥), J = ⊥
⊢ J = ⊥

Tactic:
rwa [hI, ← eq_bot_iff] at h

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
⊢ J = ⊥

Tactic:
have hJ : J = ⊥ := by rwa [hI, ← eq_bot_iff] at h
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
hJ : J = ⊥
pos : ⊥ ∣ J
pos₁ pos₂ : Dvd.dvd.{u_2} (α := Ideal A) ⊥ ⊥
⊢ I ∣ J

Tactic:
rw [hI, hJ]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
⊢ 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
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
rw :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑I : FractionalIdeal A⁰ (FractionRing A))
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1

Tactic:
rw [← inv_mul_cancel₀ hI']

Premises used: inv_mul_cancel₀
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑I : FractionalIdeal A⁰ (FractionRing A))

Tactic:
gcongr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1

Tactic:
have : (I : FractionalIdeal A⁰ (FractionRing A))⁻¹ * J ≤ 1 := by
      rw [← inv_mul_cancel₀ hI']; gcongr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
neg :
  ∀ (H : Ideal A)
    (hH :
      (↑H : FractionalIdeal A⁰ (FractionRing A)) =
        HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
          (↑J : FractionalIdeal A⁰ (FractionRing A))),
    I ∣ J
⊢ I ∣ J

Tactic:
obtain ⟨H, hH⟩ := le_one_iff_exists_coeIdeal.mp this

Premises used: FractionalIdeal.le_one_iff_exists_coeIdeal, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ : J = I * H
⊢ I ∣ J

Tactic:
use H
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ J = I * H

Tactic:
coeIdeal_injective (show (J : FractionalIdeal A⁰ (FractionRing A)) = ↑(I * H) from ?_)

Premises used: FractionalIdeal.coeIdeal_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ :
  Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
⊢ J = I * H

Tactic:
refine coeIdeal_injective (show (J : FractionalIdeal A⁰ (FractionRing A)) = ↑(I * H) from ?_)

Premises used: FractionalIdeal.coeIdeal_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
      (↑H : FractionalIdeal A⁰ (FractionRing A))
h₂ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    (↑I : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑J : FractionalIdeal A⁰ (FractionRing A))
h₃ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
        (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹ *
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₄ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑J : FractionalIdeal A⁰ (FractionRing A))
h₅ h₆ :
  Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))

Tactic:
rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]

Premises used: mul_inv_cancel₀, mul_assoc, FractionalIdeal.coeIdeal_mul, one_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 rwa rwa₁ rwa₂ rwa₃ : p.IsMaximal
⊢ IsCoatom p

Tactic:
rwa [← isMaximal_def]

Premises used: Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
rw₁ : p = under R P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₂ : p = comap (F := R →+* A) (algebraMap R A) P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₃ : p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P
rw₄ : p = comap (F := R →+* A) (algebraMap R A) P ↔ comap (F := R →+* A) (algebraMap R A) P = p
rw₅ rw₆ : comap (F := R →+* A) (algebraMap R A) P = p ↔ comap (F := R →+* A) (algebraMap R A) P = p
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p

Tactic:
rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]

Premises used: Ideal.dvd_iff_le, Ideal.liesOver_iff, Ideal.comap_ne_top, eq_comm, Ideal.map_le_iff_le_comap, Ideal.under_def, IsCoatom.le_iff_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h_1 : DvdNotUnit I J
hI : I ≠ 0
H : Ideal A
hunit : ¬IsUnit H
hmul : J = I * H
h : J = I
rw : J = I * 1
rw₁ : I = I * 1
rw₂ rw₃ : I = I
⊢ I * H = I * 1

Tactic:
rw [← hmul, h, mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ WellFoundedGT.{u_2} (Ideal A)

Tactic:
have : WellFoundedGT (Ideal A) := inferInstance
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
this : WellFoundedGT.{u_2} (Ideal A)
⊢ WellFounded fun (x1 x2 : Ideal A) ↦ x2 < x1

Tactic:
this.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
this : WellFoundedGT.{u_2} (Ideal A)
h : ∀ (x x_1 : Ideal A), DvdNotUnit x x_1 ↔ x_1 < x
⊢ WellFounded.{u_2 + 1} (α := Ideal A) DvdNotUnit

Tactic:
convert! this.wf using 3

Premises used: IsWellFounded.wf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
this : WellFoundedGT.{u_2} (Ideal A)
x x_1 : Ideal A
⊢ DvdNotUnit x x_1 ↔ x_1 < x

Tactic:
Ideal.dvdNotUnit_iff_lt

Premises used: Ideal.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
this : WellFoundedGT.{u_2} (Ideal A)
x x_1 : Ideal A
⊢ DvdNotUnit x x_1 ↔ x_1 < x

Tactic:
exact Ideal.dvdNotUnit_iff_lt

Premises used: Ideal.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
⊢ P.IsMaximal

Tactic:
⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩

Premises used: Iff.mpr, Irreducible.not_isUnit, mt, Ideal.IsMaximal.mk, And.intro, Ideal.isUnit_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
refine : ∀ (b : Ideal A), P < b → b = ⊤
⊢ P.IsMaximal

Tactic:
refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J_1 J : Ideal A
hJ : P < J
obtain : ∀ (_J_ne : J ≠ 0) (H : Ideal A) (hunit : ¬IsUnit H) (P_eq : P = J * H), J = ⊤
⊢ J = ⊤

Tactic:
obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ

Premises used: Iff.mpr, Ideal.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J_1 J : Ideal A
hJ : P < J
_J_ne : J ≠ 0
H : Ideal A
hunit : ¬IsUnit H
P_eq : P = J * H
⊢ J = ⊤

Tactic:
Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)

Premises used: Irreducible.isUnit_or_isUnit, Ideal.isUnit_iff, Iff.mp, Or.resolve_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J_1 J : Ideal A
hJ : P < J
_J_ne : J ≠ 0
H : Ideal A
hunit : ¬IsUnit H
P_eq : P = J * H
⊢ J = ⊤

Tactic:
exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)

Premises used: Irreducible.isUnit_or_isUnit, Ideal.isUnit_iff, Iff.mp, Or.resolve_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
⊢ P.IsMaximal

Tactic:
have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
rw : (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → (∀ ⦃x : A⦄, x ∈ I → x ∈ P) ∨ ∀ ⦃x : A⦄, x ∈ J → x ∈ P
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J

Tactic:
rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]

Premises used: Ideal.dvd_iff_le, SetLike.le_def
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
contrapose! : ((∃ x ∈ I, x ∉ P) ∧ ∃ x ∈ J, x ∉ P) → ∃ x ∈ I * J, x ∉ P
⊢ (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → (∀ ⦃x : A⦄, x ∈ I → x ∈ P) ∨ ∀ ⦃x : A⦄, x ∈ J → x ∈ P

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
x : A
x_mem : x ∈ I
x_notMem : x ∉ P
y : A
y_mem : y ∈ J
y_notMem : y ∉ P
⊢ ∃ x ∈ I * J, x ∉ P

Tactic:
⟨x * y, Ideal.mul_mem_mul x_mem y_mem,
            mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩

Premises used: HMul.hMul, mt, Ideal.IsMaximal.isPrime, not_or_intro, Ideal.mul_mem_mul, Ideal.IsPrime.mem_or_mem, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
x : A
x_mem : x ∈ I
x_notMem : x ∉ P
y : A
y_mem : y ∈ J
y_notMem : y ∉ P
⊢ ∃ x ∈ I * J, x ∉ P

Tactic:
exact
          ⟨x * y, Ideal.mul_mem_mul x_mem y_mem,
            mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
⊢ Irreducible P ↔ Prime P

Tactic:
exact ⟨fun hirr => ⟨hirr.ne_zero, hirr.not_isUnit, fun I J => by
        have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
        rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]
        contrapose!
        rintro ⟨⟨x, x_mem, x_notMem⟩, ⟨y, y_mem, y_notMem⟩⟩
        exact
          ⟨x * y, Ideal.mul_mem_mul x_mem y_mem,
            mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩⟩, Prime.irreducible⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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 ≠ ⊤
⊢ ∃ (x : K), Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ x ∧ x ∉ 1

Tactic:
Set.not_subset.1 <| not_inv_le_one_of_ne_bot hI0 hI1

Premises used: Set.not_subset, FractionalIdeal.not_inv_le_one_of_ne_bot, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
x : A
⊢ I ∣ span {x} ↔ x ∈ I

Tactic:
dvd_iff_le.trans (span_le.trans Set.singleton_subset_iff)

Premises used: Ideal.span_le, Ideal.dvd_iff_le, Set.singleton_subset_iff, Iff.trans
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P.IsPrime

Tactic:
⟨?_, fun hxy => ?_⟩

Premises used: Ideal.IsPrime.mk
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
refine_1 : P ≠ ⊤
refine_2 : ∀ {x y : A} (hxy : x * y ∈ P), x ∈ P ∨ y ∈ P
⊢ P.IsPrime

Tactic:
refine ⟨?_, fun hxy => ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
h : Prime.{u_2} (M := Ideal A) ⊤
⊢ Prime.{u_2} (M := Ideal A) 1

Tactic:
rw [← one_eq_top] at h

Premises used: Ideal.one_eq_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
h : Prime.{u_2} (M := Ideal A) 1
⊢ False

Tactic:
h.not_unit isUnit_one

Premises used: Prime.not_unit, isUnit_one
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
h : Prime.{u_2} (M := Ideal A) 1
⊢ False

Tactic:
exact h.not_unit isUnit_one

Premises used: Prime.not_unit, isUnit_one