case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (prod I J) ↔ x ∈ J
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ map (RingHom.snd R S) (prod I J) = J
ext x
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) ↔ x ∈ J
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (prod I J) ↔ x ∈ J
rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
no goals
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) ↔ x ∈ J
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ prod I J
⊢ ↑(RingHom.snd R S) x ∈ J
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) → x ∈ J
rintro ⟨x, ⟨h, rfl⟩⟩
no goals
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ prod I J
⊢ ↑(RingHom.snd R S) x ∈ J
exact h.2