case intro
R : Type u_2
A : Type ?u.1320972
K : Type ?u.1320975
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), i ∈ s → Prime (P i)
coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → P i ≠ P j
x : { x // x ∈ s } → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s),
    ↑(Ideal.Quotient.mk (P i ^ e i)) y =
      ↑(Ideal.Quotient.mk (P ↑{ val := i, property := hi } ^ e ↑{ val := i, property := hi }))
        (x { val := i, property := hi })
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x { val := i, property := hi } ∈ P i ^ e i
R : Type u_2
A : Type ?u.1320972
K : Type ?u.1320975
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), i ∈ s → Prime (P i)
coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → P i ≠ P j
x : { x // x ∈ s } → R
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x { val := i, property := hi } ∈ P i ^ e i
obtain ⟨y, hy⟩ :=
  IsDedekindDomain.exists_representative_mod_finset P e prime coprime fun i =>
    Ideal.Quotient.mk _ (x i)
no goals
case intro
R : Type u_2
A : Type ?u.1320972
K : Type ?u.1320975
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), i ∈ s → Prime (P i)
coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → P i ≠ P j
x : { x // x ∈ s } → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s),
    ↑(Ideal.Quotient.mk (P i ^ e i)) y =
      ↑(Ideal.Quotient.mk (P ↑{ val := i, property := hi } ^ e ↑{ val := i, property := hi }))
        (x { val := i, property := hi })
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x { val := i, property := hi } ∈ P i ^ e i
exact ⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩