R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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 : (i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i
f : R ⧸ ∏ i in s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i in s, P i ^ e i) P e prime coprime (_ : ∏ i in s, P i ^ e i = ∏ i in s, P i ^ e i)
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), ↑(Ideal.Quotient.mk (P i ^ e i)) y = x { val := i, property := hi }
R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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 : (i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), ↑(Ideal.Quotient.mk (P i ^ e i)) y = x { val := i, property := hi }
let f := IsDedekindDomain.quotientEquivPiOfFinsetProdEq _ P e prime coprime rfl
case intro
R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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
f : R ⧸ ∏ i in s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i in s, P i ^ e i) P e prime coprime (_ : ∏ i in s, P i ^ e i = ∏ i in s, P i ^ e i)
y : R ⧸ ∏ i in s, P i ^ e i
⊢ ∃ y_1, ∀ (i : ι) (hi : i ∈ s), ↑(Ideal.Quotient.mk (P i ^ e i)) y_1 = ↑f y { val := i, property := hi }
R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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 : (i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i
f : R ⧸ ∏ i in s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i in s, P i ^ e i) P e prime coprime (_ : ∏ i in s, P i ^ e i = ∏ i in s, P i ^ e i)
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), ↑(Ideal.Quotient.mk (P i ^ e i)) y = x { val := i, property := hi }
obtain ⟨y, rfl⟩ := f.surjective x
case intro.intro
R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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
f : R ⧸ ∏ i in s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i in s, P i ^ e i) P e prime coprime (_ : ∏ i in s, P i ^ e i = ∏ i in s, P i ^ e i)
z : R
⊢ ∃ y,
    ∀ (i : ι) (hi : i ∈ s),
      ↑(Ideal.Quotient.mk (P i ^ e i)) y =
        ↑f (↑(Ideal.Quotient.mk (∏ i in s, P i ^ e i)) z) { val := i, property := hi }
case intro
R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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
f : R ⧸ ∏ i in s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i in s, P i ^ e i) P e prime coprime (_ : ∏ i in s, P i ^ e i = ∏ i in s, P i ^ e i)
y : R ⧸ ∏ i in s, P i ^ e i
⊢ ∃ y_1, ∀ (i : ι) (hi : i ∈ s), ↑(Ideal.Quotient.mk (P i ^ e i)) y_1 = ↑f y { val := i, property := hi }
obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective y
no goals
case intro.intro
R : Type u_2
A : Type ?u.1294364
K : Type ?u.1294367
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
f : R ⧸ ∏ i in s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i in s, P i ^ e i) P e prime coprime (_ : ∏ i in s, P i ^ e i = ∏ i in s, P i ^ e i)
z : R
⊢ ∃ y,
    ∀ (i : ι) (hi : i ∈ s),
      ↑(Ideal.Quotient.mk (P i ^ e i)) y =
        ↑f (↑(Ideal.Quotient.mk (∏ i in s, P i ^ e i)) z) { val := i, property := hi }
exact ⟨z, fun i _hi => rfl⟩