F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
ht : ∀ (j : ι), j ∈ insert a t → s j ≠ 0
⊢ Splits i (∏ x in insert a t, s x) ↔ ∀ (j : ι), j ∈ insert a t → Splits i (s j)
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
refine'
  Finset.induction_on t (fun _ =>
      ⟨fun _ _ h => by simp only [Finset.not_mem_empty] at h, fun _ => splits_one i⟩)
    fun a t hat ih ht => _
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
ht : s a ≠ 0 ∧ ∀ (x : ι), x ∈ t → s x ≠ 0
⊢ Splits i (∏ x in insert a t, s x) ↔ Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
ht : ∀ (j : ι), j ∈ insert a t → s j ≠ 0
⊢ Splits i (∏ x in insert a t, s x) ↔ ∀ (j : ι), j ∈ insert a t → Splits i (s j)
rw [Finset.forall_mem_insert] at ht⊢
no goals
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
ht : s a ≠ 0 ∧ ∀ (x : ι), x ∈ t → s x ≠ 0
⊢ Splits i (∏ x in insert a t, s x) ↔ Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
x✝² : ∀ (j : ι), j ∈ ∅ → s j ≠ 0
x✝¹ : Splits i (∏ x in ∅, s x)
x✝ : ι
h : x✝ ∈ ∅
⊢ Splits i (s x✝)
simp only [Finset.not_mem_empty] at h