awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ Membership.mem (γ := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (I.prod J)) x ↔ x ∈ J
have h : (∃ x_1 ∈ I.prod J, (RingHom.snd R S : (a : R × S) → S) x_1 = x) ↔ x ∈ J
Tactic: rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J) = J.prod I
have refine : prod
    (map (R := S × R) (F := S × R →+* S) (RingHom.fst S R)
      (map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J)))
    (map (R := S × R) (F := S × R →+* R) (RingHom.snd S R)
      (map (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (I.prod J))) =
  J.prod I
Tactic: refine Trans.trans (ideal_prod_eq _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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)
⊢ 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) ↔
    I ≤ J
have refine : ∀
  (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)),
  I ≤ J
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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)
⊢ I ≤ J
have 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))
Tactic: rw [ideal_prod_eq I, ideal_prod_eq J]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
⊢ LE.le (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))
have 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))
Tactic: rw [ideal_prod_eq (span (s ×ˢ t)), map_span, map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
s : Set R
t : Set S
⊢ 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))
have hI : (⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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
⊢ 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))
have hJ : (⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t ⊆ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (hypothesis)
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
⊢ Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))
have hst₁ : s.Nonempty ∧ t.Nonempty ∨ s = ∅ ∧ t = ∅
Tactic: simp_rw [iff_iff_and_or_not_and_not, Set.not_nonempty_iff_eq_empty] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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 = ∅
⊢ Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))
have inl : ∀ (hs : s.Nonempty) (ht : t.Nonempty), Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))
Tactic: obtain ⟨hs, ht⟩ | ⟨rfl, rfl⟩ := hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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))
⊢ Eq (α := Ideal (R × S)) (span (s ×ˢ t)) (prod (span s) (span t))
have inr : Eq (α := Ideal (R × S)) (span (SProd.sprod (α := Set R) (β := Set S) ∅ ∅)) (prod (span ∅) (span ∅))
Tactic: obtain ⟨hs, ht⟩ | ⟨rfl, rfl⟩ := hst
Cleared hypotheses: s, t, hst
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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
| span (s ×ˢ t)
have 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)))
Tactic: rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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 × S)) (span (s ×ˢ t)) (prod (span s) (span t))
have 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))
Tactic: conv_lhs => rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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 × 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))
have inl : Eq (α := Ideal R) (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t))) (span s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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)
⊢ 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))
have inl₁ : Eq (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t))) (span t)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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) (map (F := R × S →+* R) (RingHom.fst R S) (span (s ×ˢ t))) (span s)
have inl : Eq (α := Ideal R) (span ((⇑(RingHom.fst R S) : (a : R × S) → R) '' s ×ˢ t)) (span s)
Tactic: rw [Ideal.map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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) (map (F := R × S →+* S) (RingHom.snd R S) (span (s ×ˢ t))) (span t)
have inl : Eq (α := Ideal S) (span ((⇑(RingHom.snd R S) : (a : R × S) → S) '' s ×ˢ t)) (span t)
Tactic: rw [Ideal.map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ I.prod J = ⊥ ↔ I = ⊥ ∧ J = ⊥
have rw : I.prod J = ⊥ ↔ I.prod J = prod ⊥ ⊥
Tactic: rw [← prod_inj, prod_bot_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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 ⊥ ⊥
⊢ I.prod J = ⊥ ↔ I = ⊥ ∧ J = ⊥
have rw₁ : I.prod J = ⊥ ↔ I.prod J = ⊥
Tactic: rw [← prod_inj, prod_bot_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ I.prod J = ⊤ ↔ I = ⊤ ∧ J = ⊤
have rw : I.prod J = ⊤ ↔ I.prod J = prod ⊤ ⊤
Tactic: rw [← prod_inj, prod_top_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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 ⊤ ⊤
⊢ I.prod J = ⊤ ↔ I = ⊤ ∧ J = ⊤
have rw₁ : I.prod J = ⊤ ↔ I.prod J = ⊤
Tactic: rw [← prod_inj, prod_top_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
⊢ I.IsPrime
have ne_top' : I ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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 ≠ ⊤
⊢ I.IsPrime
have mem_or_mem' : ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : IsPrime (α := R × S) (I.prod ⊤)
⊢ I ≠ ⊤
have ne_top' : ∀ (h : I = ⊤), ¬IsPrime (α := R × S) (I.prod ⊤)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬IsPrime (α := R × S) (I.prod ⊤)
have 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)
Tactic: rw [h, prod_top_top, isPrime_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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))
have rw : (x * y, 1).1 ∈ I ∧ Membership.mem (γ := Ideal S) ⊤ (x * y, 1).2
Tactic: rw [Prod.mk_mul_mk, mul_one, mem_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (hypothesis)
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 ∈ I ∨ y ∈ I
have this : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
h : IsPrime (α := R × S) (prod ⊤ I)
⊢ I.IsPrime
have apply : IsPrime (α := S × R) (I.prod ⊤)
Tactic: apply isPrime_of_isPrime_prod_top (S := R)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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) (I.prod ⊤)
have rw : IsPrime (α := S × R) (map (R := R × S) (F := R × S →+* S × R) (↑RingEquiv.prodComm : R × S →+* S × R) (prod ⊤ I))
Tactic: rw [← map_prodComm_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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) (prod ⊤ I)
have rw : IsPrime (α := R × S) (map (R := S × R) (F := S × R →+* R × S) (↑RingEquiv.prodComm : S × R →+* R × S) (I.prod ⊤))
Tactic: rw [← map_prodComm_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ (I.prod J).IsPrime → I = ⊤ ∨ J = ⊤
have contrapose! : I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime
have 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
Tactic: simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
⊢ I.IsPrime ↔ (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p
have mp : I.IsPrime → (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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
⊢ I.IsPrime ↔ (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p
have mpr : ((∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p) → I.IsPrime
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
⊢ I.IsPrime → (∃ (p : Ideal R), p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ (p : Ideal S), p.IsPrime ∧ I = prod ⊤ p
have 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)
Tactic: rw [ideal_prod_eq I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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))
⊢ (∃ (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)
have 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)
Tactic: rcases ideal_prod_prime_aux hI with (h | h)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: rcases ideal_prod_prime_aux hI with (h | h)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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) ⊤
⊢ (∃ (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)
have 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)
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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) ⊤
⊢ ∃ (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)
have 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)
Tactic: rw [h] at hI ⊢
Cleared hypotheses: hI, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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.{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)
have mp : ∃ (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 ⊤)
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
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.{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 ⊤)
have mp : ∀ (hI : IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤))
  (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) ⊤) (p.prod ⊤)
Tactic: rw [h] at hI ⊢
Cleared hypotheses: hI, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Prod (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J : Ideal S
inst_2 : IsPrincipalIdealRing R
inst_3 : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal I
have rw : Submodule.IsPrincipal (R := R × S)
  (Ideal.span
    {(generator (Ideal.map (F := R × S →+* R) (RingHom.fst R S) I),
        generator (Ideal.map (F := R × S →+* S) (RingHom.snd R S) I))})
Tactic: rw [I.ideal_prod_eq, ← span_singleton_generator (I.map _),
      ← span_singleton_generator (I.map (RingHom.snd R S)), ← Ideal.span, ← Ideal.span,
      ← Ideal.span_prod (iff_of_true (by simp) (by simp)), Set.singleton_prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
⊢ LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
have a : ∀ (x : R ⧸ I) (x_1 : ↥J),
  Eq (α := (R ⧸ I) ⊗[R] R)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) :
                  R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
              x :
            ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
          (a : ↥J) → (R ⧸ I) ⊗[R] R)
        x_1 :
      (R ⧸ I) ⊗[R] R)
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
                      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
                  R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
              x :
            ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
          (a : ↥J) → (R ⧸ I) ⊗[R] R)
        x_1 :
      (R ⧸ I) ⊗[R] R)
Tactic: ext