-- Mathlib/RingTheory/Ideal/Operations.lean
theorem prod_mem_prod {ι : Type*} {s : Finset ι} {I : ι → Ideal R} {x : ι → R} :
    (∀ i ∈ s, x i ∈ I i) → (∏ i ∈ s, x i) ∈ ∏ i ∈ s, I i

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ i ∈ ∅, x i ∈ I i
⊢ ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

Tactic:
rw [Finset.prod_empty, Finset.prod_empty, one_eq_top]

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ i ∈ ∅, x i ∈ I i
⊢ 1 ∈ ⊤

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

Tactic:
intro

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ i ∈ ∅, x i ∈ I i
⊢ ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ i ∈ ∅, x i ∈ I i
⊢ 1 ∈ ⊤

Tactic:
exact Submodule.mem_top

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Tactic:
intro a s ha IH h

Result:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : a ∉ s
IH : (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
h : ∀ i ∈ insert a s, x i ∈ I i
⊢ ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : a ∉ s
IH : (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
h : ∀ i ∈ insert a s, x i ∈ I i
⊢ ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Tactic:
rw [Finset.prod_insert ha, Finset.prod_insert ha]

Result:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : a ∉ s
IH : (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
h : ∀ i ∈ insert a s, x i ∈ I i
⊢ x a * ∏ x_1 ∈ s, x x_1 ∈ I a * ∏ x ∈ s, I x

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : a ∉ s
IH : (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
h : ∀ i ∈ insert a s, x i ∈ I i
⊢ x a * ∏ x_1 ∈ s, x x_1 ∈ I a * ∏ x ∈ s, I x

Tactic:
exact
  mul_mem_mul (h a <| Finset.mem_insert_self a s)
    (IH fun i hi => h i <| Finset.mem_insert_of_mem hi)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i

Tactic:
refine Finset.induction_on s ?_ ?_

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i