case refine_1
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ (i : ι), i ∈ ∅ → x i ∈ I i) → ∏ i in ∅, x i ∈ ∏ i in ∅, I i

case refine_2
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i) →
        (∀ (i : ι), i ∈ insert a s → x i ∈ I i) → ∏ i in insert a s, x i ∈ ∏ i in insert a s, I i
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i
refine Finset.induction_on s ?_ ?_
case refine_1
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ (i : ι), i ∈ ∅ → x i ∈ I i
⊢ ∏ i in ∅, x i ∈ ∏ i in ∅, I i
case refine_1
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ (i : ι), i ∈ ∅ → x i ∈ I i) → ∏ i in ∅, x i ∈ ∏ i in ∅, I i
intro
case refine_1
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ (i : ι), i ∈ ∅ → x i ∈ I i
⊢ 1 ∈ ⊤
case refine_1
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ (i : ι), i ∈ ∅ → x i ∈ I i
⊢ ∏ i in ∅, x i ∈ ∏ i in ∅, I i
rw [Finset.prod_empty, Finset.prod_empty, one_eq_top]
no goals
case refine_1
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
a✝ : ∀ (i : ι), i ∈ ∅ → x i ∈ I i
⊢ 1 ∈ ⊤
exact Submodule.mem_top
case refine_2
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : ¬a ∈ s
IH : (∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i
h : ∀ (i : ι), i ∈ insert a s → x i ∈ I i
⊢ ∏ i in insert a s, x i ∈ ∏ i in insert a s, I i
case refine_2
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i) →
        (∀ (i : ι), i ∈ insert a s → x i ∈ I i) → ∏ i in insert a s, x i ∈ ∏ i in insert a s, I i
intro a s ha IH h
case refine_2
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : ¬a ∈ s
IH : (∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i
h : ∀ (i : ι), i ∈ insert a s → x i ∈ I i
⊢ x a * ∏ x_1 in s, x x_1 ∈ I a * ∏ x in s, I x
case refine_2
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : ¬a ∈ s
IH : (∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i
h : ∀ (i : ι), i ∈ insert a s → x i ∈ I i
⊢ ∏ i in insert a s, x i ∈ ∏ i in insert a s, I i
rw [Finset.prod_insert ha, Finset.prod_insert ha]
no goals
case refine_2
R : Type u
ι✝ : Type ?u.211911
inst✝ : CommSemiring R
I✝ J K L : Ideal R
ι : Type u_1
s✝ : Finset ι
I : ι → Ideal R
x : ι → R
a : ι
s : Finset ι
ha : ¬a ∈ s
IH : (∀ (i : ι), i ∈ s → x i ∈ I i) → ∏ i in s, x i ∈ ∏ i in s, I i
h : ∀ (i : ι), i ∈ insert a s → x i ∈ I i
⊢ x a * ∏ x_1 in s, x x_1 ∈ I a * ∏ x in s, I x
exact
  mul_mem_mul (h a <| Finset.mem_insert_self a s)
    (IH fun i hi => h i <| Finset.mem_insert_of_mem hi)