awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ x ⊓ 0 = 0

Tactic:
simp only [zero_eq_bot, inf_bot_eq]

Premises used: Ideal.zero_eq_bot, inf_bot_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = I ⊔ J

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
⊢ @lcm _ CommSemiring.toCommMonoidWithZero _ I J = I ⊓ J

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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
rw₂ : I ⊔ J = ⊤ ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = ⊤
rw₃ rw₄ : I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
⊢ IsCoprime I J ↔ @gcd _ CommSemiring.toCommMonoidWithZero _ I J = 1

Tactic:
rw [isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]

Premises used: Ideal.one_eq_top, Ideal.gcd_eq_sup, codisjoint_iff, Ideal.isCoprime_iff_codisjoint
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
p : K[X]
inl : Eq (α := Multiset (Ideal K[X])) (factors (span {0})) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors 0))
inr :
  ∀ (hp : p ≠ 0),
    Eq (α := Multiset (Ideal K[X])) (factors (span {p})) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))
⊢ Eq (α := Multiset (Ideal K[X])) (factors (span {p})) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
⊢ Eq (α := Multiset (Ideal K[X])) (factors (span {0})) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors 0))

Tactic:
simpa [Set.singleton_zero] using normalizedFactors_zero

Premises used: UniqueFactorizationMonoid.normalizedFactors_zero, Set.singleton_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
p : K[X]
hp : p ≠ 0
q : Ideal K[X]
hq : Membership.mem (γ := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p)) q
obtain :
  ∀ (r : K[X]) (hr : r ∈ factors p)
    (hq :
      Membership.mem (γ := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p)) (span {r})),
    Prime (M := Ideal K[X]) (span {r})
⊢ Prime q

Tactic:
obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
p : K[X]
hp : p ≠ 0
r : K[X]
hr : r ∈ factors p
hq : Membership.mem (γ := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p)) (span {r})
⊢ Prime (M := Ideal K[X]) (span {r})

Tactic:
prime_span_singleton_iff.mpr <| prime_of_factor r hr

Premises used: Iff.mpr, Set.Mem, Ideal.prime_span_singleton_iff, UniqueFactorizationMonoid.prime_of_factor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
p : K[X]
hp : p ≠ 0
r : K[X]
hr : r ∈ factors p
hq : Membership.mem (γ := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p)) (span {r})
⊢ Prime (M := Ideal K[X]) (span {r})

Tactic:
exact prime_span_singleton_iff.mpr <| prime_of_factor r hr

Premises used: Iff.mpr, Ideal.prime_span_singleton_iff, UniqueFactorizationMonoid.prime_of_factor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
p : K[X]
hp : p ≠ 0
⊢ ∀ (q : Ideal K[X]),
    Membership.mem (γ := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p)) q → Prime q

Tactic:
have : ∀ q ∈ (factors p).map (fun q ↦ span {q}), Prime q := fun q hq ↦ by
    obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
    exact prime_span_singleton_iff.mpr <| prime_of_factor r hr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
K : Type u_3
inst : Field K
p : K[X]
hp : p ≠ 0
this :
  ∀ (q : Ideal K[X]),
    Membership.mem (γ := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p)) q → Prime q
inr :
  Eq (α := Multiset (Ideal K[X])) (factors (span {(factors p).prod}))
    (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))
inr₁ :
  Eq (α := Multiset (Ideal K[X])) (factors (Multiset.prod (Multiset.map (fun (x : K[X]) ↦ span {x}) (factors p))))
    (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))
inr₂ :
  Eq (α := Multiset (Ideal K[X]))
    (normalizedFactors (Multiset.prod (Multiset.map (fun (x : K[X]) ↦ span {x}) (factors p))))
    (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))
inr₃ inr₄ :
  Eq (α := Multiset (Ideal K[X])) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))
    (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))
⊢ Eq (α := Multiset (Ideal K[X])) (factors (span {p})) (Multiset.map (fun (q : K[X]) ↦ span {q}) (factors p))

Tactic:
rw [← span_singleton_eq_span_singleton.mpr (factors_prod hp), ← multiset_prod_span_singleton,
    factors_eq_normalizedFactors, normalizedFactors_prod_of_prime this]

Premises used: Iff.mpr, UniqueFactorizationMonoid.factors_eq_normalizedFactors, Ideal.span_singleton_eq_span_singleton, UniqueFactorizationMonoid.normalizedFactors_prod_of_prime, Ideal.multiset_prod_span_singleton, UniqueFactorizationMonoid.factors_prod
-- 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
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
    (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) ((↑I.den : A) * (↑I.den : A) * (↑J.den : A) * (↑J.den : A))) :
      FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
    (0 : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)

Tactic:
simp [spanSingleton_eq_zero_iff]

Premises used: FractionalIdeal.spanSingleton_eq_zero_iff
-- 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
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
a :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
    ((fun (a : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) a
          (spanSingleton A⁰
              ((algebraMap A K : (a : A) → K) ((↑I.den : A) * (↑I.den : A) * (↑J.den : A) * (↑J.den : A))) :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K))
      ((I ⊓ J) * (I ⊔ J)))
    ((fun (a : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) a
          (spanSingleton A⁰
              ((algebraMap A K : (a : A) → K) ((↑I.den : A) * (↑I.den : A) * (↑J.den : A) * (↑J.den : A))) :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K))
      (I * J))
⊢ (I ⊓ J) * (I ⊔ J) = I * J

Tactic:
apply mul_left_injective₀ (b := spanSingleton A⁰ (algebraMap A K
    (I.den.1 * I.den.1 * J.den.1 * J.den.1))) (by simp [spanSingleton_eq_zero_iff])

Premises used: mul_left_injective₀
-- 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
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
⊢ (Ideal.span {(↑J.den : A)} * I.num ⊔ Ideal.span {(↑I.den : A)} * J.num) *
      (Ideal.span {(↑J.den : A)} * I.num ⊓ Ideal.span {(↑I.den : A)} * J.num) =
    Ideal.span {(↑J.den : A)} * I.num * (Ideal.span {(↑I.den : A)} * J.num)

Tactic:
have := Ideal.sup_mul_inf (Ideal.span {J.den.1} * I.num) (Ideal.span {I.den.1} * J.num)
-- 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
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
this :
  (Ideal.span {(↑J.den : A)} * I.num ⊔ Ideal.span {(↑I.den : A)} * J.num) *
      (Ideal.span {(↑J.den : A)} * I.num ⊓ Ideal.span {(↑I.den : A)} * J.num) =
    Ideal.span {(↑J.den : A)} * I.num * (Ideal.span {(↑I.den : A)} * J.num)
⊢ (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            I) +
        HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            J)) *
      (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            I) ⊓
        HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
            J)) =
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          I) *
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) J)

Tactic:
simp only [← coeIdeal_inj (K := K), coeIdeal_mul, coeIdeal_sup, coeIdeal_inf,
    ← den_mul_self_eq_num', coeIdeal_span_singleton] at this

Premises used: FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_inj, FractionalIdeal.coeIdeal_sup, FractionalIdeal.coeIdeal_inf, FractionalIdeal.coeIdeal_mul, FractionalIdeal.den_mul_self_eq_num'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
⊢ (normalizedFactors I).prod = I

Tactic:
associated_iff_eq.1 (prod_normalizedFactors hI)

Premises used: associated_iff_eq, UniqueFactorizationMonoid.prod_normalizedFactors, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
h : I ≤ J
hI : I ≠ ⊥
K : Ideal T
⊢ count K (normalizedFactors J) ≤ count K (normalizedFactors I)

Tactic:
le_iff_count.1 ((dvd_iff_normalizedFactors_le_normalizedFactors (ne_bot_of_le_ne_bot hI h) hI).1
    (dvd_iff_le.2 h))
    _

Premises used: Iff.mpr, Ideal.dvd_iff_le, Multiset.le_iff_count, ne_bot_of_le_ne_bot, Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0

Tactic:
have := prod_inter_normalizedFactors_ne_zero I J
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : I ⊔ J ≤ (normalizedFactors I ∩ normalizedFactors J).prod
a₁ : (normalizedFactors I ∩ normalizedFactors J).prod ≤ I ⊔ J
⊢ I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : (normalizedFactors I ∩ normalizedFactors J).prod ∣ I ∧ (normalizedFactors I ∩ normalizedFactors J).prod ∣ J
⊢ I ⊔ J ≤ (normalizedFactors I ∩ normalizedFactors J).prod

Tactic:
rw [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:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : (normalizedFactors I ∩ normalizedFactors J).prod ∣ I
a₁ : (normalizedFactors I ∩ normalizedFactors J).prod ∣ J
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ∣ I ∧ (normalizedFactors I ∩ normalizedFactors J).prod ∣ J

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors I
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ∣ I

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
        normalizedFactors_prod_inter_eq_inter]

Premises used: UniqueFactorizationMonoid.normalizedFactors_prod_inter_eq_inter, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ J ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors J
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ∣ J

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
        normalizedFactors_prod_inter_eq_inter]

Premises used: UniqueFactorizationMonoid.normalizedFactors_prod_inter_eq_inter, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors I

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors J

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors I

Tactic:
exacts [inf_le_left, inf_le_right]

Premises used: inf_le_right, inf_le_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : ∀ (a : Ideal T), count a (normalizedFactors (I ⊔ J)) ≤ count a (normalizedFactors I ∩ normalizedFactors J)
rw : I ⊔ J ≠ 0
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≤ I ⊔ J

Tactic:
rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors ?H this,
      normalizedFactors_prod_inter_eq_inter, le_iff_count]

Premises used: Ideal.dvd_iff_le, Multiset.le_iff_count, UniqueFactorizationMonoid.normalizedFactors_prod_inter_eq_inter, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ⊔ J ≠ 0

Tactic:
ne_bot_of_le_ne_bot hI le_sup_left

Premises used: ne_bot_of_le_ne_bot, le_sup_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ⊔ J ≠ 0

Tactic:
exact ne_bot_of_le_ne_bot hI le_sup_left

Premises used: ne_bot_of_le_ne_bot, le_sup_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ⊔ J ≠ 0

Tactic:
case H => exact ne_bot_of_le_ne_bot hI le_sup_left

Premises used: ne_bot_of_le_ne_bot, le_sup_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : Ideal T
a₁ : count a (normalizedFactors (I ⊔ J)) ≤ min (count a (normalizedFactors I)) (count a (normalizedFactors J))
⊢ count a (normalizedFactors (I ⊔ J)) ≤ count a (normalizedFactors I ∩ normalizedFactors J)

Tactic:
rw [Multiset.count_inter]

Premises used: Multiset.count_inter
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : Ideal T
⊢ count a (normalizedFactors (I ⊔ J)) ≤ min (count a (normalizedFactors I)) (count a (normalizedFactors J))

Tactic:
le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)

Premises used: le_min, Ideal.count_le_of_ideal_ge
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
a : Ideal T
⊢ count a (normalizedFactors (I ⊔ J)) ≤ min (count a (normalizedFactors I)) (count a (normalizedFactors J))

Tactic:
exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)

Premises used: le_min, Ideal.count_le_of_ideal_ge
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
rw : (normalizedFactors (J ^ n) ∩ normalizedFactors I).prod = J ^ min (count J (normalizedFactors I)) n
rw₁ : (normalizedFactors (J ^ n) ∩ normalizedFactors I).prod = J ^ min n (count J (normalizedFactors I))
rw₂ :
  Multiset.prod (replicate n ((normalize : (a : Ideal T) → Ideal T) J) ∩ normalizedFactors I) =
    J ^ min n (count J (normalizedFactors I))
rw₃ : (replicate n J ∩ normalizedFactors I).prod = J ^ min n (count J (normalizedFactors I))
rw₄ : (replicate (min n (count J (normalizedFactors I))) J).prod = J ^ min n (count J (normalizedFactors I))
rw₅ rw₆ : J ^ min n (count J (normalizedFactors I)) = J ^ min n (count J (normalizedFactors I))
⊢ J ^ n ⊔ I = J ^ min (count J (normalizedFactors I)) n

Tactic:
rw [sup_eq_prod_inf_factors (pow_ne_zero n hJ.ne_zero) hI, min_comm,
    normalizedFactors_of_irreducible_pow hJ, normalize_eq J, replicate_inter, prod_replicate]

Premises used: Multiset.prod_replicate, min_comm, Ideal.sup_eq_prod_inf_factors, pow_ne_zero, Multiset.replicate_inter, Irreducible.ne_zero, UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : (↑n : ℕ∞) ≤ emultiplicity J I
pos : ∀ (hI : I = ⊥), J ^ n ⊔ I = J ^ n
neg : ∀ (hI : ¬I = ⊥), J ^ n ⊔ I = J ^ n
⊢ J ^ n ⊔ I = J ^ n

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : (↑n : ℕ∞) ≤ emultiplicity J I
hI : I = ⊥
⊢ J ^ n ⊔ I = J ^ n

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : (↑n : ℕ∞) ≤ emultiplicity J I
hI : ¬I = ⊥
neg : n ≤ count J (normalizedFactors I)
⊢ J ^ n ⊔ I = J ^ n

Tactic:
rw [irreducible_pow_sup hI hJ, min_eq_right]

Premises used: Ideal.irreducible_pow_sup, min_eq_right
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : (↑n : ℕ∞) ≤ emultiplicity J I
hI : ¬I = ⊥
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞)

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn

Premises used: UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : (↑n : ℕ∞) ≤ emultiplicity J I
hI : ¬I = ⊥
hn₁ : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞)
⊢ ¬I = ⊥

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn

Premises used: UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞)
hI : ¬I = ⊥
⊢ n ≤ count J (normalizedFactors I)

Tactic:
exact_mod_cast hn
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hJ : Irreducible J
n : ℕ
hn : (↑n : ℕ∞) ≤ emultiplicity J I
pos : ∀ (hI : I = ⊥), J ^ n ⊔ I = J ^ n
neg neg₁ : ∀ (hI : ¬I = ⊥), J ^ n ⊔ I = J ^ n
neg₂ : ∀ (hI : ¬I = ⊥), n ≤ count J (normalizedFactors I)
neg₃ :
  ∀ (hn : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞)) (hI : ¬I = ⊥),
    n ≤ count J (normalizedFactors I)
⊢ J ^ n ⊔ I = J ^ n

Tactic:
classical
  by_cases hI : I = ⊥
  · simp_all
  rw [irreducible_pow_sup hI hJ, min_eq_right]
  rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn
  exact_mod_cast hn

Premises used: min_eq_right, normalize_eq