awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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)
refine_2 :
  ∀ (y : K) (hy : y ∈ I) (x : K) (h : x ∈ f '' (↑s : Set ι)),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
⊢ a ∈ (↑J : FractionalIdeal A⁰ K) / I
have refine_2₁ : ∀ (y : K) (hy : y ∈ I),
  Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * 0)
Tactic: refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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)
refine_2 :
  ∀ (y : K) (hy : y ∈ I) (x : K) (h : x ∈ f '' (↑s : Set ι)),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
refine_2₁ :
  ∀ (y : K) (hy : y ∈ I),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * 0)
⊢ a ∈ (↑J : FractionalIdeal A⁰ K) / I
have refine_2₂ : ∀ (y : K) (hy : y ∈ I) (x y : K) (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x)
  (hy : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y),
  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) (a * y) →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))
Tactic: refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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)
refine_2 :
  ∀ (y : K) (hy : y ∈ I) (x : K) (h : x ∈ f '' (↑s : Set ι)),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
refine_2₁ :
  ∀ (y : K) (hy : y ∈ I),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * 0)
refine_2₂ :
  ∀ (y : K) (hy : y ∈ I) (x y : K) (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x)
    (hy : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y),
    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) (a * y) →
        Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))
⊢ a ∈ (↑J : FractionalIdeal A⁰ K) / I
have refine_2₃ : ∀ (y : K) (hy : y ∈ I) (a_1 : A) (x : K)
  (hx : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x),
  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) (a * a_1 • x)
Tactic: refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * 0)
have refine_2 : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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_1 : K
hy_1 : y_1 ∈ I
x y : K
hx_1 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) x
hy_2 : Membership.mem (γ := Submodule A K) (Submodule.span A (f '' (↑s : Set ι))) y
hx : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
hy : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * y)
⊢ Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * (x + y))
have refine_2 : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x + a * y)
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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) (a * b • x)
have refine_2 : Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (b • (a * x))
Tactic: rw [mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have suffices : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
have rw : (↑J : FractionalIdeal A⁰ K) * I⁻¹ < I⁻¹
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (↑J : FractionalIdeal A⁰ K) * I⁻¹ < I⁻¹
have refine : LT.lt.{u_3} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) 1
Tactic: refine mul_lt_of_lt_one_left (by simpa [pos_iff_ne_zero]) ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
have pos : ∀ (hI : I = 0), I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
have neg : ∀ (hI : ¬I = 0), I * ⨅ (i : ι), J i = ⨅ (i : ι), I * J i
Tactic: by_cases hI : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
have neg : ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i
Tactic: refine (le_iInf fun i ↦ mul_mono_right (iInf_le _ _)).antisymm ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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
have H : ⨅ (i : ι), I * J i ≤ I
Tactic: have H : ⨅ i, I * J i ≤ I := (iInf_le _ (Nonempty.some ‹_›)).trans mul_le_right
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i
have neg : ∀ (K : Ideal A) (hK : ⨅ (i : ι), I * J i = I * K), ⨅ (i : ι), I * J i ≤ I * ⨅ (i : ι), J i
Tactic: obtain ⟨K, hK⟩ := dvd_iff_le.mpr H
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 * J i ≤ I * ⨅ (i : ι), J i
have grw : ∀ (i : ι), K ≤ J i
Tactic: grw [hK, le_iInf (a := K) fun i ↦ ?_]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 : ι
⊢ K ≤ J i
have rw : ⨅ (i : ι), I * J i ≤ I * J i
Tactic: rw [← mul_le_mul_iff_of_pos_left (a := I), ← hK]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ K ≤ J i
have rw₁ : 0 < I
Tactic: rw [← mul_le_mul_iff_of_pos_left (a := I), ← hK]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J K : Ideal A
⊢ I * (J ⊓ K) = I * J ⊓ I * K
have 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)
Tactic: rw [inf_eq_iInf, mul_iInf, inf_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ⊔ J
Tactic: rw [gcd_eq_normalize _ _, normalize_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J
have rw₁ : I ⊔ J ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ I J
Tactic: rw [gcd_eq_normalize _ _, normalize_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ I J ∣ J
Tactic: rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 ⊔ J ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ I J
have rw : I ≤ I ⊔ J ∧ J ≤ I ⊔ J
Tactic: rw [dvd_gcd_iff, dvd_iff_le, dvd_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 ⊔ J) * (I ⊓ J) = I * J
have hgcd : @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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
have rw : @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∣ I ⊓ J
Tactic: rw [lcm_eq_normalize _ _, normalize_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I ⊓ J
have rw₁ : I ⊓ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J
Tactic: rw [lcm_eq_normalize _ _, normalize_eq]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
have rw : I ⊓ J ≤ I ∧ I ⊓ J ≤ J
Tactic: rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J
have rw : I ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J ∧ J ∣ @lcm _ CommSemiring.toCommMonoidWithZero _ I J
Tactic: rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 ⊓ J) = I * J
have hlcm : @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 _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (I ⊔ J) * (I ⊓ J) = I * J
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ I J * (I ⊓ J) = I * J
Tactic: rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (I ⊔ J) * (I ⊓ J) = I * J
have rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ I J * @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I * J
Tactic: rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (I ⊔ J) * (I ⊓ J) = I * J
have rw₂ : I * J = I * J
Tactic: rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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}, a ∣ c → a ∣ b → a ∣ c ⊔ b
have simp : ∀ {a b c : Ideal A}, c ≤ a → b ≤ a → c ⊔ b ≤ a
Tactic: simp only [dvd_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Associated ((x ⊔ x_1) * (x ⊓ x_1)) (x * x_1)
have rw : (x ⊔ x_1) * (x ⊓ x_1) = x * x_1
Tactic: rw [associated_iff_eq, sup_mul_inf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Associated ((x ⊔ x_1) * (x ⊓ x_1)) (x * x_1)
have rw₁ : x * x_1 = x * x_1
Tactic: rw [associated_iff_eq, sup_mul_inf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
⊢ IsCoprime I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
have rw : Codisjoint I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
rw : Codisjoint I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
⊢ IsCoprime I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
have rw₁ : I ⊔ J = ⊤ ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
rw : Codisjoint I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
rw₁ : I ⊔ J = ⊤ ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
⊢ IsCoprime I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1
have rw₂ : I ⊔ J = ⊤ ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = ⊤
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]