awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
b : A
x : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
refine_2 : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (b • (a * x))
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * b • x)

Tactic:
rw [mul_smul_comm]

Premises used: mul_smul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
b : A
x : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (b • (a * x))

Tactic:
Submodule.smul_mem _ b hx

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
y : K
hy : y ∈ I
b : A
x : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (b • (a * x))

Tactic:
exact Submodule.smul_mem _ b hx

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
suffices : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)

Tactic:
suffices ↑J / I < I⁻¹ by
    obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this
    rw [mem_inv_iff hI0] at hI
    refine ⟨a, fun i hi => ?_, ?_⟩
    -- By definition, `a ∈ I⁻¹` multiplies elements of `I` into elements of `1`,
    -- in other words, `a * f i` is an integer.
    · exact (mem_one_iff _).mp (hI (f i) (Submodule.subset_span (Set.mem_image_of_mem f hi)))
    · contrapose! hpI
      -- And if all `a`-multiples of `I` are an element of `J`,
      -- then `a` is actually an element of `J / I`, contradiction.
      refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
      · rintro _ ⟨i, hi, rfl⟩; exact hpI i hi
      · rw [mul_zero]; exact Submodule.zero_mem _
      · intro x y _ _ hx hy; rw [mul_add]; exact Submodule.add_mem _ hx hy
      · intro b x _ hx; rw [mul_smul_comm]; exact Submodule.smul_mem _ b hx
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
rw : (↑J : FractionalIdeal A⁰ K) * I⁻¹ < I⁻¹
⊢ (↑J : FractionalIdeal A⁰ K) / I < I⁻¹

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ 0 < I⁻¹

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
refine : LT.lt.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 1
⊢ (↑J : FractionalIdeal A⁰ K) * I⁻¹ < I⁻¹

Tactic:
refine mul_lt_of_lt_one_left (by simpa [pos_iff_ne_zero]) ?_

Premises used: mul_lt_of_lt_one_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ LT.lt.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (↑⊤ : FractionalIdeal A⁰ K)

Tactic:
strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm)
      (lt_top_iff_ne_top.mpr hJ)

Premises used: Iff.mpr, strictMono_of_le_iff_le, lt_top_iff_ne_top, Iff.symm, FractionalIdeal.coeIdeal_le_coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ LT.lt.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (↑⊤ : FractionalIdeal A⁰ K)

Tactic:
exact
    strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm)
      (lt_top_iff_ne_top.mpr hJ)

Premises used: Iff.mpr, strictMono_of_le_iff_le, lt_top_iff_ne_top, Iff.symm, FractionalIdeal.coeIdeal_le_coeIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
pos : ∀ (hI : I = 0), I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
neg : ∀ (hI : ¬I = 0), I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
⊢ I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i

Tactic:
by_cases hI : I = 0
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : I = 0
⊢ I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i

Tactic:
simp [hI]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
⊢ I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i

Tactic:
(le_iInf fun i ↦ mul_mono_right (iInf_le _ _)).antisymm ?_

Premises used: le_iInf, LE.le.antisymm, Ideal.mul_mono_right, iInf_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
neg : ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i
⊢ I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i

Tactic:
refine (le_iInf fun i ↦ mul_mono_right (iInf_le _ _)).antisymm ?_

Premises used: le_iInf, LE.le.antisymm, Ideal.mul_mono_right, iInf_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
⊢ ⨅ (i : ι), I * J i ≤ I

Tactic:
have H : ⨅ i, I * J i ≤ I := (iInf_le _ (Nonempty.some ‹_›)).trans mul_le_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
neg : ∀ (K : Ideal A) (hK : ⨅ (i : ι), I * J i = I * K), ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i
⊢ ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i

Tactic:
obtain ⟨K, hK⟩ := dvd_iff_le.mpr H

Premises used: Iff.mpr, Ideal.dvd_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
K : Ideal A
hK : ⨅ (i : ι), I * J i = I * K
grw : ∀ (i : ι), K ≤ J i
⊢ ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i

Tactic:
grw [hK, le_iInf (a := K) fun i ↦ ?_]

Premises used: le_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
K : Ideal A
hK : ⨅ (i : ι), I * J i = I * K
i : ι
rw : ⨅ (i : ι), I * J i ≤ I * J i
rw₁ : 0 < I
⊢ K ≤ J i

Tactic:
rw [← mul_le_mul_iff_of_pos_left (a := I), ← hK]

Premises used: mul_le_mul_iff_of_pos_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
K : Ideal A
hK : ⨅ (i : ι), I * J i = I * K
i : ι
⊢ ⨅ (i : ι), I * J i ≤ I * J i

Tactic:
iInf_le _ _

Premises used: Set.Mem, iInf_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
K : Ideal A
hK : ⨅ (i : ι), I * J i = I * K
i : ι
⊢ ⨅ (i : ι), I * J i ≤ I * J i

Tactic:
exact iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
K : Ideal A
hK : ⨅ (i : ι), I * J i = I * K
i : ι
⊢ 0 < I

Tactic:
bot_lt_iff_ne_bot.mpr hI

Premises used: Iff.mpr, bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ (i : ι), I * J i ≤ I
K : Ideal A
hK : ⨅ (i : ι), I * J i = I * K
i : ι
⊢ 0 < I

Tactic:
exact bot_lt_iff_ne_bot.mpr hI

Premises used: Iff.mpr, bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst_2 : Nonempty ι
J : ι → Ideal A
⊢ (⨅ (i : ι), J i) * I = ⨅ (i : ι), J i * I

Tactic:
simp only [mul_iInf, mul_comm _ I]

Premises used: mul_comm, Ideal.mul_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J K : Ideal A
rw : Eq.{u_2 + 1} (α := Ideal A) (⨅ (i : Bool), I * bif i then J else K) (⨅ (b : Bool), bif b then I * J else I * K)
⊢ I * (J ⊓ K) = I * J ⊓ I * K

Tactic:
rw [inf_eq_iInf, mul_iInf, inf_eq_iInf]

Premises used: inf_eq_iInf, Ideal.mul_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J K : Ideal A
⊢ Eq.{u_2 + 1} (α := Ideal A) (⨅ (i : Bool), I * bif i then J else K) (⨅ (b : Bool), bif b then I * J else I * K)

Tactic:
congr! 2 with ⟨⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J K : Ideal A
⊢ (I ⊓ J) * K = I * K ⊓ J * K

Tactic:
simp only [mul_inf, mul_comm _ K]

Premises used: mul_comm, Ideal.mul_inf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K_1 : Type u_3
inst : CommRing A
inst_1 : Field K_1
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
I J K : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1
⊢ I * (J ⊓ K) = I * J ⊓ I * K

Tactic:
mul_inf₀ (zero_le _) _ _

Premises used: mul_inf₀
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
K_1 : Type u_3
inst : CommRing A
inst_1 : Field K_1
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
I J K : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1
⊢ (I ⊓ J) * K = I * K ⊓ J * K

Tactic:
inf_mul₀ (zero_le _) _ _

Premises used: inf_mul₀
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
rw : @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ⊔ J
rw₁ : I ⊔ J ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ I J
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J

Tactic:
rw [gcd_eq_normalize _ _, normalize_eq]

Premises used: gcd_eq_normalize, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
rw : @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ J
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ⊔ J

Tactic:
rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]

Premises used: Ideal.dvd_iff_le, sup_le_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ J

Tactic:
⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩

Premises used: And.intro, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ J

Tactic:
exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
rw : I ≤ I ⊔ J ∧ J ≤ I ⊔ J
⊢ I ⊔ J ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ I J

Tactic:
rw [dvd_gcd_iff, dvd_iff_le, dvd_iff_le]

Premises used: Ideal.dvd_iff_le, dvd_gcd_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J

Tactic:
have hgcd : gcd I J = I ⊔ J := by
    rw [gcd_eq_normalize _ _, normalize_eq]
    · rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
      exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩
    · rw [dvd_gcd_iff, dvd_iff_le, dvd_iff_le]
      simp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
rw : @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ⊓ J
rw₁ : I ⊓ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J
⊢ @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I ⊓ J

Tactic:
rw [lcm_eq_normalize _ _, normalize_eq]

Premises used: lcm_eq_normalize, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
rw : I ⊓ J ≤ I ∧ I ⊓ J ≤ J
⊢ @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ⊓ J

Tactic:
rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]

Premises used: Ideal.dvd_iff_le, lcm_dvd_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
rw : I ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∧ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J
⊢ I ⊓ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J

Tactic:
rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]

Premises used: Ideal.dvd_iff_le, le_inf_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
⊢ I ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∧ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J

Tactic:
⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩

Premises used: dvd_lcm_right, dvd_lcm_left, And.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
⊢ I ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∧ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J

Tactic:
exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
⊢ @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I ⊓ J

Tactic:
have hlcm : lcm I J = I ⊓ J := by
    rw [lcm_eq_normalize _ _, normalize_eq]
    · rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]
      simp
    · rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]
      exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
hlcm : @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I ⊓ J
rw : @gcd _ CommSemiring.toCommMonoidWithZero _ I J * (I ⊓ J) = I * J
rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ I J * @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I * J
rw₂ rw₃ : I * J = I * J
⊢ (I ⊔ J) * (I ⊓ J) = I * J

Tactic:
rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]

Premises used: gcd_mul_lcm, associated_iff_eq, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
x x_1 : Ideal A
⊢ x ⊔ x_1 ∣ x

Tactic:
simpa only [dvd_iff_le] using le_sup_left

Premises used: Ideal.dvd_iff_le, le_sup_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
x x_1 : Ideal A
⊢ x ⊔ x_1 ∣ x_1

Tactic:
simpa only [dvd_iff_le] using le_sup_right

Premises used: Ideal.dvd_iff_le, le_sup_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
simp : ∀ {a b c : Ideal A}, c ≤ a → b ≤ a → c ⊔ b ≤ a
⊢ ∀ {a b c : Ideal A}, a ∣ c → a ∣ b → a ∣ c ⊔ b

Tactic:
simp only [dvd_iff_le]

Premises used: Ideal.dvd_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
a b c : Ideal A
⊢ c ≤ a → b ≤ a → c ⊔ b ≤ a

Tactic:
fun h1 h2 => @sup_le (Ideal A) _ _ _ _ h1 h2

Premises used: Set.Mem, sup_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
⊢ ∀ {a b c : Ideal A}, c ≤ a → b ≤ a → c ⊔ b ≤ a

Tactic:
exact fun h1 h2 => @sup_le (Ideal A) _ _ _ _ h1 h2

Premises used: sup_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
x x_1 : Ideal A
rw : (x ⊔ x_1) * (x ⊓ x_1) = x * x_1
rw₁ rw₂ : x * x_1 = x * x_1
⊢ Associated ((x ⊔ x_1) * (x ⊓ x_1)) (x * x_1)

Tactic:
rw [associated_iff_eq, sup_mul_inf]

Premises used: associated_iff_eq, Ideal.sup_mul_inf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
x : Ideal A
⊢ 0 ⊓ x = 0

Tactic:
simp only [zero_eq_bot, bot_inf_eq]

Premises used: Ideal.zero_eq_bot, bot_inf_eq