awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J_1 : Ideal S
I J : Ideal (R × S)
h :
  LE.le.{u} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* R) (RingHom.fst R S) J) ∧
    LE.le.{v} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) (map (F := R × S →+* S) (RingHom.snd R S) J)
rw :
  LE.le (α := Ideal (R × S))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) J) (map (F := R × S →+* S) (RingHom.snd R S) J))
⊢ I ≤ J

Tactic:
rw [ideal_prod_eq I, ideal_prod_eq J]

Premises used: Ideal.ideal_prod_eq
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J_1 : Ideal S
I J : Ideal (R × S)
h :
  LE.le.{u} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* R) (RingHom.fst R S) J) ∧
    LE.le.{v} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) (map (F := R × S →+* S) (RingHom.snd R S) J)
⊢ LE.le (α := Ideal (R × S))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) J) (map (F := R × S →+* S) (RingHom.snd R S) J))

Tactic:
inf_le_inf (comap_mono h.1) (comap_mono h.2)

Premises used: inf_le_inf, Set.Mem, Ideal.comap_mono, And.right, And.left
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J_1 : Ideal S
I J : Ideal (R × S)
h :
  LE.le.{u} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* R) (RingHom.fst R S) J) ∧
    LE.le.{v} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) (map (F := R × S →+* S) (RingHom.snd R S) J)
⊢ LE.le (α := Ideal (R × S))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) J) (map (F := R × S →+* S) (RingHom.snd R S) J))

Tactic:
exact inf_le_inf (comap_mono h.1) (comap_mono h.2)

Premises used: inf_le_inf, Ideal.comap_mono, And.right, And.left
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ (OrderIso.symm idealProdEquiv : (a : Ideal R × Ideal S) → Ideal (R × S)) (I, J) = I.prod J

Tactic:
rfl

Premises used: Ideal.prod, rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
rw :
  LE.le (α := Ideal (R × S))
    (prod (span ((⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t))
      (span ((⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t)))
    (prod (span s) (span t))
⊢ LE.le (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))

Tactic:
rw [ideal_prod_eq (span (s ×ˢ t)), map_span, map_span]

Premises used: SProd.sprod, Ideal.map_span, Ideal.ideal_prod_eq, Ideal.span
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hI : (⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t ⊆ s
hJ : (⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t ⊆ t
⊢ LE.le (α := Ideal (R × S))
    (prod (span ((⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t))
      (span ((⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t)))
    (prod (span s) (span t))

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
⊢ (⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t ⊆ s

Tactic:
Set.fst_image_prod_subset _ _

Premises used: Set.fst_image_prod_subset
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
⊢ (⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t ⊆ s

Tactic:
exact Set.fst_image_prod_subset _ _

Premises used: Set.fst_image_prod_subset
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
⊢ (⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t ⊆ t

Tactic:
Set.snd_image_prod_subset _ _

Premises used: Set.snd_image_prod_subset
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
⊢ (⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t ⊆ t

Tactic:
exact Set.snd_image_prod_subset _ _

Premises used: Set.snd_image_prod_subset
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hst : s.Nonempty ↔ t.Nonempty
⊢ s.Nonempty ∧ t.Nonempty ∨ s = ∅ ∧ t = ∅

Tactic:
simp_rw [iff_iff_and_or_not_and_not, Set.not_nonempty_iff_eq_empty] at hst

Premises used: Set.not_nonempty_iff_eq_empty, iff_iff_and_or_not_and_not
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hst : s.Nonempty ∧ t.Nonempty ∨ s = ∅ ∧ t = ∅
inl : ∀ (hs : s.Nonempty) (ht : t.Nonempty), Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))
inr : Eq (α := Ideal (R × S)) (span (SProd.sprod (α := Set R) (β := Set S) ∅ ∅)) (prod (span ∅) (span ∅))
⊢ Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))

Tactic:
obtain ⟨hs, ht⟩ | ⟨rfl, rfl⟩ := hst

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
rw :
  prod (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t)))
    (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t)))
| span (s ×ˢ t)

Tactic:
rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]

Premises used: SProd.sprod, Ideal.ideal_prod_eq, Ideal.span
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
inl :
  Eq (α := Ideal (R × S))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t)))
      (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t))))
    (prod (span s) (span t))
⊢ Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))

Tactic:
conv_lhs => rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]

Premises used: SProd.sprod, Ideal.ideal_prod_eq, Ideal.span
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
inl : Eq (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t))) (span s)
inl₁ : Eq (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t))) (span t)
⊢ Eq (α := Ideal (R × S))
    (prod (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t)))
      (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t))))
    (prod (span s) (span t))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
inl : Eq (α := Ideal R) (span ((⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t)) (span s)
⊢ Eq (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t))) (span s)

Tactic:
rw [Ideal.map_span]

Premises used: Ideal.map_span
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ Eq (α := Ideal R) (span ((⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t)) (span s)

Tactic:
simp [Set.fst_image_prod _ ht]

Premises used: Set.fst_image_prod
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
inl : Eq (α := Ideal S) (span ((⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t)) (span t)
⊢ Eq (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t))) (span t)

Tactic:
rw [Ideal.map_span]

Premises used: Ideal.map_span
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ Eq (α := Ideal S) (span ((⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t)) (span t)

Tactic:
simp [Set.snd_image_prod hs]

Premises used: Set.snd_image_prod
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
⊢ Eq (α := Ideal (R × S)) (span (SProd.sprod (α := Set R) (β := Set S) ∅ ∅)) (prod (span ∅) (span ∅))

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I I' : Ideal R
J J' : Ideal S
⊢ I.prod J = I'.prod J' ↔ I = I' ∧ J = J'

Tactic:
simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk_inj]

Premises used: Function.Injective.eq_iff, Ideal.idealProdEquiv, Prod.mk_inj, Ideal.idealProdEquiv_symm_apply, OrderIso.symm, OrderIso.injective
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
rw : I.prod J = ⊥ ↔ I.prod J = prod ⊥ ⊥
rw₁ rw₂ : I.prod J = ⊥ ↔ I.prod J = ⊥
⊢ I.prod J = ⊥ ↔ I = ⊥ ∧ J = ⊥

Tactic:
rw [← prod_inj, prod_bot_bot]

Premises used: Ideal.prod_inj, Ideal.prod_bot_bot
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
rw : I.prod J = ⊤ ↔ I.prod J = prod ⊤ ⊤
rw₁ rw₂ : I.prod J = ⊤ ↔ I.prod J = ⊤
⊢ I.prod J = ⊤ ↔ I = ⊤ ∧ J = ⊤

Tactic:
rw [← prod_inj, prod_top_top]

Premises used: Ideal.prod_inj, Ideal.prod_top_top
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
ne_top' : I ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsPrime

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
ne_top' : ∀ (h : I = ⊤), ¬IsPrime (α := R × S) (I.prod ⊤)
⊢ I ≠ ⊤

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I = ⊤
ne_top' :
  ¬(Ne (α := Ideal (R × S)) ⊤ ⊤ ∧
      ∀ {x y : R × S},
        Membership.mem (γ := Ideal (R × S)) ⊤ (x * y) →
          Membership.mem (γ := Ideal (R × S)) ⊤ x ∨ Membership.mem (γ := Ideal (R × S)) ⊤ y)
⊢ ¬IsPrime (α := R × S) (I.prod ⊤)

Tactic:
rw [h, prod_top_top, isPrime_iff]

Premises used: Ideal.isPrime_iff, Ideal.prod_top_top
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(Ne (α := Ideal (R × S)) ⊤ ⊤ ∧
      ∀ {x y : R × S},
        Membership.mem (γ := Ideal (R × S)) ⊤ (x * y) →
          Membership.mem (γ := Ideal (R × S)) ⊤ x ∨ Membership.mem (γ := Ideal (R × S)) ⊤ y)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
x y : R
hxy : x * y ∈ I
rw : (x * y, 1).1 ∈ I ∧ Membership.mem (γ := Ideal S) ⊤ (x * y, 1).2
⊢ Membership.mem (γ := Ideal (R × S)) (I.prod ⊤) (HMul.hMul (α := R × S) (x, 1) (y, 1))

Tactic:
rw [Prod.mk_mul_mk, mul_one, mem_prod]

Premises used: Prod.mk_mul_mk, mul_one, Ideal.mem_prod
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
x y : R
hxy : x * y ∈ I
⊢ (x * y, 1).1 ∈ I ∧ Membership.mem (γ := Ideal S) ⊤ (x * y, 1).2

Tactic:
⟨hxy, trivial⟩

Premises used: trivial, And.intro
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
x y : R
hxy : x * y ∈ I
⊢ (x * y, 1).1 ∈ I ∧ Membership.mem (γ := Ideal S) ⊤ (x * y, 1).2

Tactic:
exact ⟨hxy, trivial⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
x y : R
hxy : x * y ∈ I
⊢ Membership.mem (γ := Ideal (R × S)) (I.prod ⊤) (HMul.hMul (α := R × S) (x, 1) (y, 1))

Tactic:
have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ := by
      rw [Prod.mk_mul_mk, mul_one, mem_prod]
      exact ⟨hxy, trivial⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
x y : R
hxy : x * y ∈ I
this : Membership.mem (γ := Ideal (R × S)) (I.prod ⊤) (HMul.hMul (α := R × S) (x, 1) (y, 1))
⊢ x ∈ I ∨ y ∈ I

Tactic:
simpa using h.mem_or_mem this

Premises used: Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : IsPrime (α := R × S) (prod ⊤ I)
apply : IsPrime (α := S × R) (I.prod ⊤)
⊢ I.IsPrime

Tactic:
apply isPrime_of_isPrime_prod_top (S := R)

Premises used: Ideal.isPrime_of_isPrime_prod_top
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : IsPrime (α := R × S) (prod ⊤ I)
rw : IsPrime (α := S × R) (map (R := R × S) (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (prod ⊤ I))
⊢ IsPrime (α := S × R) (I.prod ⊤)

Tactic:
rw [← map_prodComm_prod]

Premises used: Ideal.map_prodComm_prod
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : IsPrime (α := R × S) (prod ⊤ I)
⊢ IsPrime (α := S × R) (map (R := R × S) (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (prod ⊤ I))

Tactic:
map_isPrime_of_equiv (RingEquiv.prodComm (R := R) (S := S))

Premises used: Ideal.map, RingEquiv.prodComm, Ideal.map_isPrime_of_equiv, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : IsPrime (α := R × S) (prod ⊤ I)
⊢ IsPrime (α := S × R) (map (R := R × S) (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (prod ⊤ I))

Tactic:
exact map_isPrime_of_equiv (RingEquiv.prodComm (R := R) (S := S))

Premises used: RingEquiv.prodComm, Ideal.map_isPrime_of_equiv
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I.IsPrime
⊢ Ne (α := Ideal (R × S)) (I.prod ⊤) ⊤

Tactic:
simpa using h.ne_top

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I.IsPrime
x y : R × S
⊢ Membership.mem (γ := Ideal (R × S)) (I.prod ⊤) (x * y) →
    Membership.mem (γ := Ideal (R × S)) (I.prod ⊤) x ∨ Membership.mem (γ := Ideal (R × S)) (I.prod ⊤) y

Tactic:
simpa using h.mem_or_mem

Premises used: Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : I.IsPrime
this : IsPrime (α := S × R) (I.prod ⊤) := ⋯
rw : IsPrime (α := R × S) (map (R := S × R) (F := S × R →+* R × S) (↑RingEquiv.prodComm : S × R →+* R × S) (I.prod ⊤))
⊢ IsPrime (α := R × S) (prod ⊤ I)

Tactic:
rw [← map_prodComm_prod]

Premises used: Ideal.map_prodComm_prod
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : I.IsPrime
this : IsPrime (α := S × R) (I.prod ⊤) := ⋯
⊢ IsPrime (α := R × S) (map (R := S × R) (F := S × R →+* R × S) (↑RingEquiv.prodComm : S × R →+* R × S) (I.prod ⊤))

Tactic:
map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

Premises used: Ideal.map, RingEquiv.prodComm, Ideal.map_isPrime_of_equiv, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : I.IsPrime
this : IsPrime (α := S × R) (I.prod ⊤) := ⋯
⊢ IsPrime (α := R × S) (map (R := S × R) (F := S × R →+* R × S) (↑RingEquiv.prodComm : S × R →+* R × S) (I.prod ⊤))

Tactic:
exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

Premises used: RingEquiv.prodComm, Ideal.map_isPrime_of_equiv
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
contrapose! : I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime
⊢ (I.prod J).IsPrime → I = ⊤ ∨ J = ⊤

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
simp :
  1 ∉ I ∧ 1 ∉ J → 1 ∉ I.prod J → ∃ (x : R × S) (x_1 : R × S) (_ : x * x_1 ∈ I.prod J), x ∉ I.prod J ∧ x_1 ∉ I.prod J
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime

Tactic:
simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]

Premises used: Ideal.ne_top_iff_one, not_or, Ideal.isPrime_iff, not_and, Classical.not_forall
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
h : 1 ∉ I ∧ 1 ∉ J
h_1 : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ HMul.hMul (α := R × S) (0, 1) (1, 0) ∈ I.prod J

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
h : 1 ∉ I ∧ 1 ∉ J
h_1 : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) ∉ I.prod J

Tactic:
simp [hJ]
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
h : 1 ∉ I ∧ 1 ∉ J
h_1 : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (1, 0) ∉ I.prod J

Tactic:
simp [hI]
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ 1 ∉ I ∧ 1 ∉ J → 1 ∉ I.prod J → ∃ (x : R × S) (x_1 : R × S) (_ : x * x_1 ∈ I.prod J), x ∉ I.prod J ∧ x_1 ∉ I.prod J

Tactic:
exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
mp : I.IsPrime → (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p
mpr : ((∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p) → I.IsPrime
⊢ I.IsPrime ↔ (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
mp :
  IsPrime (α := R × S)
      (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) →
    (∃ (p : Ideal R),
        p.IsPrime ∧
          Eq (α := Ideal (R × S))
            (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
            (p.prod ⊤)) ∨
      ∃ (p : Ideal S),
        p.IsPrime ∧
          Eq (α := Ideal (R × S))
            (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)
⊢ I.IsPrime → (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p

Tactic:
rw [ideal_prod_eq I]

Premises used: Ideal.ideal_prod_eq
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI :
  IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
mp :
  ∀ (h : Eq.{u + 1} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤),
    (∃ (p : Ideal R),
        p.IsPrime ∧
          Eq (α := Ideal (R × S))
            (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
            (p.prod ⊤)) ∨
      ∃ (p : Ideal S),
        p.IsPrime ∧
          Eq (α := Ideal (R × S))
            (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)
mp₁ :
  ∀ (h : Eq.{v + 1} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) ⊤),
    (∃ (p : Ideal R),
        p.IsPrime ∧
          Eq (α := Ideal (R × S))
            (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
            (p.prod ⊤)) ∨
      ∃ (p : Ideal S),
        p.IsPrime ∧
          Eq (α := Ideal (R × S))
            (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)
⊢ (∃ (p : Ideal R),
      p.IsPrime ∧
        Eq (α := Ideal (R × S))
          (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (p.prod ⊤)) ∨
    ∃ (p : Ideal S),
      p.IsPrime ∧
        Eq (α := Ideal (R × S))
          (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)

Tactic:
rcases ideal_prod_prime_aux hI with (h | h)

Premises used: Ideal.ideal_prod_prime_aux
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI :
  IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
h : Eq.{u + 1} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤
mp :
  ∃ (p : Ideal S),
    p.IsPrime ∧
      Eq (α := Ideal (R × S))
        (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)
⊢ (∃ (p : Ideal R),
      p.IsPrime ∧
        Eq (α := Ideal (R × S))
          (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (p.prod ⊤)) ∨
    ∃ (p : Ideal S),
      p.IsPrime ∧
        Eq (α := Ideal (R × S))
          (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)

Tactic:
right
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI :
  IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
h : Eq.{u + 1} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤
mp :
  ∀ (hI : IsPrime (α := R × S) (prod ⊤ (map (F := R × S →+* S) (RingHom.snd R S) I)))
    (h : Eq.{u + 1} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤),
    ∃ (p : Ideal S),
      p.IsPrime ∧ Eq (α := Ideal (R × S)) (prod ⊤ (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)
⊢ ∃ (p : Ideal S),
    p.IsPrime ∧
      Eq (α := Ideal (R × S))
        (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)

Tactic:
rw [h] at hI ⊢
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI : IsPrime (α := R × S) (prod ⊤ (map (F := R × S →+* S) (RingHom.snd R S) I))
h : Eq.{u + 1} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤
⊢ ∃ (p : Ideal S), p.IsPrime ∧ Eq (α := Ideal (R × S)) (prod ⊤ (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)

Tactic:
⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩

Premises used: Ideal.isPrime_of_isPrime_prod_top', And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI : IsPrime (α := R × S) (prod ⊤ (map (F := R × S →+* S) (RingHom.snd R S) I))
h : Eq.{u + 1} (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤
⊢ ∃ (p : Ideal S), p.IsPrime ∧ Eq (α := Ideal (R × S)) (prod ⊤ (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)

Tactic:
exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩