R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h2 : Separable (f a) ∧ ∀ (x : ι), x ∈ s → Separable (f x)
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ (x : ι), x ∈ s → a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι), x ∈ s → x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ Separable (∏ x in insert a s, f x)
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h1 : ∀ (x : ι), x ∈ insert a s → ∀ (y : ι), y ∈ insert a s → x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ (x : ι), x ∈ insert a s → Separable (f x)
⊢ Separable (∏ x in insert a s, f x)
simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h2 : Separable (f a) ∧ ∀ (x : ι), x ∈ s → Separable (f x)
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ (x : ι), x ∈ s → a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι), x ∈ s → x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ Separable (f a * ∏ x in s, f x)
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h2 : Separable (f a) ∧ ∀ (x : ι), x ∈ s → Separable (f x)
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ (x : ι), x ∈ s → a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι), x ∈ s → x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ Separable (∏ x in insert a s, f x)
rw [prod_insert has]
no goals
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h2 : Separable (f a) ∧ ∀ (x : ι), x ∈ s → Separable (f x)
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ (x : ι), x ∈ s → a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι), x ∈ s → x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ Separable (f a * ∏ x in s, f x)
exact
  h2.1.mul (ih h1.2.2 h2.2)
    (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)