-- Mathlib/RingTheory/Ideal/IsPrimary.lean
lemma isPrimary_finset_inf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
    (hs : ∀ ⦃y⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y⦄, y ∈ s → (f y).radical = (f i).radical) :
    IsPrimary (s.inf f)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).radical = (f i).radical
y : ι
hy : y ∈ s
⊢ ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).radical = (f i).radical
y : ι
hy : y ∈ s
x : ι
hx : x ∈ s
⊢ (f x).radical = (f y).radical

Proof state:
case insert
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).radical = (f i).radical
⊢ ((insert a s).inf f).IsPrimary

Tactic:
rcases s.eq_empty_or_nonempty with rfl|⟨y, hy⟩

Result:
case insert.inl
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι},
    i ∈ ∅ →
      (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).radical = (f i).radical) → (∅.inf f).IsPrimary
hi : i ∈ insert a ∅
hs : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).radical = (f i).radical
⊢ ((insert a ∅).inf f).IsPrimary

case insert.inr.intro
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).radical = (f i).radical
y : ι
hy : y ∈ s
⊢ ((insert a s).inf f).IsPrimary

Proof state:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).radical = (f i).radical
y : ι
hy : y ∈ s
x : ι
hx : x ∈ s
⊢ (f x).radical = (f y).radical

Tactic:
rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]

Result:
no goals

Proof state:
case insert.inr.intro.refine_1
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).radical = (f i).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical
x : ι
hx : x ∈ s
⊢ (f x).IsPrimary

Tactic:
exact hs (by simp [hx])

Result:
no goals

Proof state:
case insert.inl
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι},
    i ∈ ∅ →
      (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).radical = (f i).radical) → (∅.inf f).IsPrimary
hi : i ∈ insert a ∅
hs : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).radical = (f i).radical
⊢ ((insert a ∅).inf f).IsPrimary

Tactic:
simp only [insert_emptyc_eq, mem_singleton] at hi

Result:
case insert.inl
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
a i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι},
    i ∈ ∅ →
      (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).radical = (f i).radical) → (∅.inf f).IsPrimary
hs : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).radical = (f i).radical
hi : i = a
⊢ ((insert a ∅).inf f).IsPrimary

Proof state:
case empty
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → Ideal R
i : ι
hi : i ∈ ∅
hs : ∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ ∅ → (f y).radical = (f i).radical
⊢ (∅.inf f).IsPrimary

Tactic:
simp at hi

Result:
no goals