-- Mathlib/RingTheory/Ideal/IsPrimary.lean
theorem isPrimary_inf {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary)
    (hij : radical I = radical J) : (I ⊓ J).IsPrimary :=
  isPrimary_iff.mpr
  ⟨ne_of_lt <| lt_of_le_of_lt inf_le_left (lt_top_iff_ne_top.2 hi.1),
   fun {x y} ⟨hxyi, hxyj⟩ => by
    rw [radical_inf, hij, inf_idem]
    rcases (isPrimary_iff.mp hi).2 hxyi with hxi | hyi
    · rcases (isPrimary_iff.mp hj).2 hxyj with hxj | hyj
      · exact Or.inl ⟨hxi, hxj⟩
      · exact Or.inr hyj
    · rw [hij] at hyi
      exact Or.inr hyi⟩

Proof state:
case inr
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hyi : y ∈ I.radical
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Tactic:
rw [hij] at hyi

Result:
case inr
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hyi : y ∈ J.radical
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
⊢ x ∈ I ⊓ J ∨ y ∈ (I ⊓ J).radical

Tactic:
rw [radical_inf, hij, inf_idem]

Result:
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Tactic:
rcases (isPrimary_iff.mp hi).2 hxyi with hxi | hyi

Result:
case inl
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hxi : x ∈ I
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

case inr
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hyi : y ∈ I.radical
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Proof state:
case inl.inl
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hxi : x ∈ I
hxj : x ∈ J
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Tactic:
exact Or.inl ⟨hxi, hxj⟩

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hxi : x ∈ I
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Tactic:
rcases (isPrimary_iff.mp hj).2 hxyj with hxj | hyj

Result:
case inl.inl
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hxi : x ∈ I
hxj : x ∈ J
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

case inl.inr
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hxi : x ∈ I
hyj : y ∈ J.radical
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Proof state:
case inr
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hyi : y ∈ J.radical
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Tactic:
exact Or.inr hyi

Result:
no goals

Proof state:
case inl.inr
R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
x y : R
x✝ : x * y ∈ I ⊓ J
hxyi : x * y ∈ ↑I
hxyj : x * y ∈ ↑J
hxi : x ∈ I
hyj : y ∈ J.radical
⊢ x ∈ I ⊓ J ∨ y ∈ J.radical

Tactic:
exact Or.inr hyj

Result:
no goals