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 : R
⊢ x ∈ map (RingHom.fst R S) (prod I J) ↔ x ∈ I
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.fst R S) (prod I J) = I
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 : R
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) ↔ x ∈ I
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 : R
⊢ x ∈ map (RingHom.fst R S) (prod I J) ↔ x ∈ I
rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_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 : R
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) ↔ x ∈ I
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, 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.fst R S) x ∈ I
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
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) → x ∈ I
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.fst R S) x ∈ I
exact h.1