-- 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:
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

Tactic:
simpa [hi] using hs

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
⊢ ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary

Tactic:
intro x hx

Result:
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

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
H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical
⊢ a ∈ insert a s

Tactic:
simp

Result:
no goals

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
H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical
x : ι
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
simp [hx]

Result:
no goals

Proof state:
case insert.inr.intro.refine_2
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
⊢ (f a).radical = (s.inf f).radical

Tactic:
rw [radical_finset_inf hy H, hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]

Result:
no goals

Proof state:
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
H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical
⊢ (f a ⊓ s.inf f).IsPrimary

Tactic:
refine isPrimary_inf (hs (by simp)) (IH hy ?_ H) ?_

Result:
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
⊢ ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary

case insert.inr.intro.refine_2
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
⊢ (f a).radical = (s.inf f).radical

Proof state:
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
⊢ (f a ⊓ s.inf f).IsPrimary

Tactic:
have H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical := by
  intro x hx
  rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]

Result:
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
H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical
⊢ (f a ⊓ s.inf f).IsPrimary

Proof state:
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

Tactic:
simp only [inf_insert]

Result:
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
⊢ (f a ⊓ s.inf f).IsPrimary