awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
rw rw₁ : Eq.{u_1 + 1} (α := Ideal R) (⨅ a ∈ s, (f a).asIdeal ^ e a) (⨅ i ∈ s, (f i).asIdeal ^ e i)
⊢ Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ (f i).asIdeal ^ e i) (⨅ i ∈ s, (f i).asIdeal ^ e i)

Tactic:
rw [Finset.inf_eq_iInf s fun i ↦ (f i).asIdeal ^ e i]

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, HPow.hPow, Finset.inf_eq_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime (fun (i : ι) ↦ (f i).asIdeal ^ e i) i j

Tactic:
HeightOneSpectrum.isCoprime_pow_of_ne _ _ (coprime i hi j hj hij) _ _

Premises used: IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime (fun (i : ι) ↦ (f i).asIdeal ^ e i) i j

Tactic:
exact HeightOneSpectrum.isCoprime_pow_of_ne _ _ (coprime i hi j hj hij) _ _

Premises used: IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
rw : (↑s : Set ι).Pairwise (Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime fun (i : ι) ↦ f i ^ e i)
⊢ Eq.{u_1 + 1} (α := Ideal R) (s.inf fun (i : ι) ↦ f i ^ e i) (∏ i ∈ s, f i ^ e i)

Tactic:
rw [prod_eq_iInf_of_pairwise_isCoprime, Finset.inf_eq_iInf s fun i ↦ (f i) ^ e i]

Premises used: HPow.hPow, Finset.inf_eq_iInf, Ideal.prod_eq_iInf_of_pairwise_isCoprime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime (fun (i : ι) ↦ f i ^ e i) i j

Tactic:
Ideal.isCoprime_iff_sup_eq.mpr (pow_sup_pow_eq_top (IsMaximal.coprime_of_ne
    (IsPrime.isMaximal (isPrime_of_prime (prime i hi)) (prime i hi).ne_zero)
    (IsPrime.isMaximal (isPrime_of_prime (prime j hj)) (prime j hj).ne_zero)
    (coprime i hi j hj hij)))

Premises used: Iff.mpr, Ideal.pow_sup_pow_eq_top, Ideal.IsPrime.isMaximal, Ideal.IsMaximal.coprime_of_ne, Prime.ne_zero, Ideal.isPrime_of_prime, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ (↑s : Set ι)
j : ι
hj : j ∈ (↑s : Set ι)
hij : i ≠ j
⊢ Function.onFun.{u_4 + 1, u_1 + 1, 1} (β := Ideal R) IsCoprime (fun (i : ι) ↦ f i ^ e i) i j

Tactic:
exact Ideal.isCoprime_iff_sup_eq.mpr (pow_sup_pow_eq_top (IsMaximal.coprime_of_ne
    (IsPrime.isMaximal (isPrime_of_prime (prime i hi)) (prime i hi).ne_zero)
    (IsPrime.isMaximal (isPrime_of_prime (prime j hj)) (prime j hj).ne_zero)
    (coprime i hi j hj hij)))

Premises used: Iff.mpr, Ideal.pow_sup_pow_eq_top, Ideal.IsPrime.isMaximal, Ideal.IsMaximal.coprime_of_ne, Prime.ne_zero, Ideal.isPrime_of_prime, Ideal.isCoprime_iff_sup_eq
-- 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
ι : Type u_4
inst_3 : IsDedekindDomain R
inst_4 : Fintype ι
I : Ideal R
P : ι → HeightOneSpectrum R
e : ι → ℕ
coprime : Pairwise fun (i j : ι) ↦ P i ≠ P j
prod_eq : ∏ i : ι, (P i).asIdeal ^ e i = I
⊢ I = ⨅ (i : ι), (P i).asIdeal ^ e i

Tactic:
simp [← prod_eq, Finset.inf_eq_iInf, Finset.mem_univ,
      ← HeightOneSpectrum.inf_pow_eq_prod _ _ _ (coprime.set_pairwise _)]

Premises used: Finset.mem_univ, Finset.inf_eq_iInf, Pairwise.set_pairwise, IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod
-- 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
ι_1 : ?m.1
inst_3 : IsDedekindDomain R
ι : Type u_4
inst_4 : Fintype ι
I : Ideal R
P : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), Prime (P i)
coprime : Pairwise fun (i j : ι) ↦ P i ≠ P j
prod_eq : ∏ i : ι, P i ^ e i = I
⊢ Pairwise fun (i j : ι) ↦
    Ne.{u_1 + 1} (α := HeightOneSpectrum R)
      ((fun (i : ι) ↦ { asIdeal := P i, isPrime := ⋯, ne_bot := ⋯ : HeightOneSpectrum R }) i)
      ((fun (i : ι) ↦ { asIdeal := P i, isPrime := ⋯, ne_bot := ⋯ : HeightOneSpectrum R }) j)

Tactic:
grind
-- 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
ι : ?m.1
inst_3 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
rw rw₁ : (factors I).prod = (factors I).prod
⊢ Multiset.prod (Multiset.map (fun (P : Ideal R) ↦ P) (factors I)) = (factors I).prod

Tactic:
rw [Multiset.map_id']

Premises used: Multiset.map_id'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
x : R
⊢ Eq (α := (P : ↥(factors I).toFinset) → R ⧸ (↑P : Ideal R) ^ Multiset.count (↑P : Ideal R) (factors I))
    (((quotientEquivPiFactors hI :
            R ⧸ I ≃+* ((P : ↥(factors I).toFinset) → R ⧸ (↑P : Ideal R) ^ Multiset.count (↑P : Ideal R) (factors I))) :
          (a : R ⧸ I) → (P : ↥(factors I).toFinset) → R ⧸ (↑P : Ideal R) ^ Multiset.count (↑P : Ideal R) (factors I))
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) :
      (P : ↥(factors I).toFinset) → R ⧸ (↑P : Ideal R) ^ Multiset.count (↑P : Ideal R) (factors I))
    fun (_P : ↥(factors I).toFinset) ↦
    ((Ideal.Quotient.mk ((↑_P : Ideal R) ^ Multiset.count (↑_P : Ideal R) (factors I)) :
          (a : R) → R ⧸ (↑_P : Ideal R) ^ Multiset.count (↑_P : Ideal R) (factors I))
        x :
      R ⧸ (↑_P : Ideal R) ^ Multiset.count (↑_P : Ideal R) (factors I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : (i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)
f : HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i) ≃+* ((i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)) :=
  quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯
obtain :
  ∀ (y : HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i)),
    ∃ (y_1 : R),
      ∀ (i : ι) (hi : i ∈ s),
        Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y_1 : R ⧸ P i ^ e i)
          ((f : (a : R ⧸ ∏ i ∈ s, P i ^ e i) → (i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)) y
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
            R ⧸
              P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
                e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
⊢ ∃ (y : R),
    ∀ (i : ι) (hi : i ∈ s),
      Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
          R ⧸
            P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
              e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
obtain ⟨y, rfl⟩ := f.surjective x

Premises used: RingEquiv.surjective, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
f : HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i) ≃+* ((i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)) :=
  quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯
y : HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i)
obtain :
  ∀ (z : R),
    ∃ (y : R),
      ∀ (i : ι) (hi : i ∈ s),
        Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
          ((f : (a : R ⧸ ∏ i ∈ s, P i ^ e i) → (i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι))
              ((Ideal.Quotient.mk (∏ i ∈ s, P i ^ e i) : (a : R) → R ⧸ ∏ i ∈ s, P i ^ e i) z :
                HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
            R ⧸
              P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
                e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
⊢ ∃ (y_1 : R),
    ∀ (i : ι) (hi : i ∈ s),
      Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y_1 : R ⧸ P i ^ e i)
        ((f : (a : R ⧸ ∏ i ∈ s, P i ^ e i) → (i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)) y
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
          R ⧸
            P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
              e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
f : HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i) ≃+* ((i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)) :=
  quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯
z : R
⊢ ∃ (y : R),
    ∀ (i : ι) (hi : i ∈ s),
      Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
        ((f : (a : R ⧸ ∏ i ∈ s, P i ^ e i) → (i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι))
            ((Ideal.Quotient.mk (∏ i ∈ s, P i ^ e i) : (a : R) → R ⧸ ∏ i ∈ s, P i ^ e i) z :
              HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i))
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
          R ⧸
            P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
              e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
⟨z, fun i _hi => rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
f : HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i) ≃+* ((i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι)) :=
  quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯
z : R
⊢ ∃ (y : R),
    ∀ (i : ι) (hi : i ∈ s),
      Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
        ((f : (a : R ⧸ ∏ i ∈ s, P i ^ e i) → (i : ↥s) → R ⧸ P (↑i : ι) ^ e (↑i : ι))
            ((Ideal.Quotient.mk (∏ i ∈ s, P i ^ e i) : (a : R) → R ⧸ ∏ i ∈ s, P i ^ e i) z :
              HasQuotient.Quotient R (B := Ideal R) (∏ i ∈ s, P i ^ e i))
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) :
          R ⧸
            P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
              e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))

Tactic:
exact ⟨z, fun i _hi => rfl⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : ↥s → R
obtain :
  ∀ (y : R)
    (hy :
      ∀ (i : ι) (hi : i ∈ s),
        Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
          ((Ideal.Quotient.mk
                  (P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
                    e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι)) :
                (a : R) → R ⧸ P (↑⟨i, hi⟩ : ι) ^ e (↑⟨i, hi⟩ : ι))
              (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) :
            R ⧸
              P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
                e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))),
    ∃ (y : R), ∀ (i : ι) (hi : i ∈ s), y - x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) ∈ P i ^ e i
⊢ ∃ (y : R), ∀ (i : ι) (hi : i ∈ s), y - x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) ∈ P i ^ e i

Tactic:
obtain ⟨y, hy⟩ :=
    exists_representative_mod_finset P e prime coprime fun i =>
      Ideal.Quotient.mk _ (x i)

Premises used: Ideal.Quotient.mk, HPow.hPow, IsDedekindDomain.exists_representative_mod_finset, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : ↥s → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s),
    Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
      ((Ideal.Quotient.mk
              (P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
                e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι)) :
            (a : R) → R ⧸ P (↑⟨i, hi⟩ : ι) ^ e (↑⟨i, hi⟩ : ι))
          (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) :
        R ⧸
          P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^ e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
⊢ ∃ (y : R), ∀ (i : ι) (hi : i ∈ s), y - x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) ∈ P i ^ e i

Tactic:
⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩

Premises used: Ideal.Quotient.eq, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : ↥s → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s),
    Eq (α := R ⧸ P i ^ e i) ((Ideal.Quotient.mk (P i ^ e i) : (a : R) → R ⧸ P i ^ e i) y : R ⧸ P i ^ e i)
      ((Ideal.Quotient.mk
              (P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^
                e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι)) :
            (a : R) → R ⧸ P (↑⟨i, hi⟩ : ι) ^ e (↑⟨i, hi⟩ : ι))
          (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) :
        R ⧸
          P (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι) ^ e (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι))
⊢ ∃ (y : R), ∀ (i : ι) (hi : i ∈ s), y - x (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) ∈ P i ^ e i

Tactic:
exact ⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a b : R
⊢ Dvd.dvd (α := Ideal R) (span {a}) (span {b}) ↔ a ∣ b

Tactic:
⟨fun h => mem_span_singleton.mp (dvd_iff_le.mp h (mem_span_singleton.mpr (dvd_refl b))), fun h =>
    dvd_iff_le.mpr fun _d hd => mem_span_singleton.mpr (dvd_trans h (mem_span_singleton.mp hd))⟩

Premises used: Iff.mpr, Ideal.dvd_iff_le, dvd_trans, Iff.intro, Iff.mp, Ideal.mem_span_singleton, dvd_refl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
⊢ Squarefree (R := Ideal R) (span {a}) ↔ Squarefree a

Tactic:
⟨fun h x hx ↦ ?_, fun h I hI ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
refine_1 : ∀ (h : Squarefree (R := Ideal R) (span {a})) (x : R) (hx : x * x ∣ a), IsUnit x
refine_2 : ∀ (h : Squarefree a) (I : Ideal R) (hI : I * I ∣ span {a}), IsUnit I
⊢ Squarefree (R := Ideal R) (span {a}) ↔ Squarefree a

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h I hI ↦ ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : Squarefree (R := Ideal R) (span {a})
x : R
hx : x * x ∣ a
⊢ HMul.hMul (α := Ideal R) (span {x}) (span {x}) ∣ span {a}

Tactic:
rw [← span_singleton_dvd_span_singleton_iff_dvd, ← span_singleton_mul_span_singleton] at hx

Premises used: Ideal.span_singleton_dvd_span_singleton_iff_dvd, Ideal.span_singleton_mul_span_singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : Squarefree (R := Ideal R) (span {a})
x : R
hx : HMul.hMul (α := Ideal R) (span {x}) (span {x}) ∣ span {a}
⊢ IsUnit x

Tactic:
simpa using h _ hx
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : I * I ∣ span {a}
⊢ Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a

Tactic:
rw [← span_singleton_generator I, span_singleton_mul_span_singleton,
      span_singleton_dvd_span_singleton_iff_dvd] at hI

Premises used: Ideal.span_singleton_dvd_span_singleton_iff_dvd, Ideal.span_singleton_generator, Ideal.span_singleton_mul_span_singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a
⊢ IsUnit I

Tactic:
isUnit_iff.mpr <| eq_top_of_isUnit_mem _ (Submodule.IsPrincipal.generator_mem I) (h _ hI)

Premises used: Iff.mpr, Ideal.eq_top_of_isUnit_mem, Submodule.IsPrincipal.generator_mem, Ideal.isUnit_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a
⊢ IsUnit I

Tactic:
exact isUnit_iff.mpr <| eq_top_of_isUnit_mem _ (Submodule.IsPrincipal.generator_mem I) (h _ hI)

Premises used: Iff.mpr, Ideal.eq_top_of_isUnit_mem, Submodule.IsPrincipal.generator_mem, Ideal.isUnit_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
pos : ∀ (hb : b = 0), Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})
neg : ∀ (hb : ¬b = 0), Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})
⊢ Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
pos : Membership.mem (γ := Multiset (Ideal R)) 0 (span {a})
⊢ Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})

Tactic:
rw [span_singleton_eq_bot.mpr hb, bot_eq_zero, normalizedFactors_zero]

Premises used: Iff.mpr, Ideal.span_singleton_eq_bot, UniqueFactorizationMonoid.normalizedFactors_zero, bot_eq_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ Membership.mem (γ := Multiset R) 0 a

Tactic:
rw [hb, normalizedFactors_zero] at ha

Premises used: UniqueFactorizationMonoid.normalizedFactors_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
ha₁ : Membership.mem (γ := Multiset R) 0 a
⊢ b = 0

Tactic:
rw [hb, normalizedFactors_zero] at ha

Premises used: UniqueFactorizationMonoid.normalizedFactors_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : Membership.mem (γ := Multiset R) 0 a
hb : b = 0
⊢ Membership.mem (γ := Multiset (Ideal R)) 0 (span {a})

Tactic:
absurd ha (Multiset.notMem_zero a)

Premises used: Multiset.notMem_zero, absurd
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : Membership.mem (γ := Multiset R) 0 a
hb : b = 0
⊢ Membership.mem (γ := Multiset (Ideal R)) 0 (span {a})

Tactic:
exact absurd ha (Multiset.notMem_zero a)

Premises used: Multiset.notMem_zero, absurd
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (M := Ideal R) (span {a})
obtain :
  ∀ (c : Ideal R) (hc : Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) c)
    (hc' : Associated (span {a}) c), Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})
⊢ Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})

Tactic:
obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
          (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))

Premises used: Prime.irreducible, Iff.mpr, Ideal.dvd_iff_le, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Ideal.span_singleton_le_span_singleton, UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (M := Ideal R) (span {a})
c : Ideal R
hc : Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) c
hc' : Associated (span {a}) c
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) c
⊢ Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})

Tactic:
rwa [associated_iff_eq.mp hc']

Premises used: associated_iff_eq, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
neg : ∀ (this : Prime (M := Ideal R) (span {a})), Ne (α := Ideal R) (span {b}) 0
neg₁ : Prime (M := Ideal R) (span {a})
⊢ Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {b})) (span {a})

Tactic:
suffices Prime (span ({a} : Set R)) by
      obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
          (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))
      rwa [associated_iff_eq.mp hc']