-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem isSplittingField_iSup {p : ι → K[X]}
    {s : Finset ι} (h0 : ∏ i ∈ s, p i ≠ 0) (h : ∀ i ∈ s, (p i).IsSplittingField K (t i)) :
    (∏ i ∈ s, p i).IsSplittingField K (⨆ i ∈ s, t i : IntermediateField K L)

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
⊢ IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Tactic:
simp only [isSplittingField_iff] at h ⊢

Result:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)
⊢ Splits (algebraMap K ↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i) ∧ ⨆ i ∈ s, t i = adjoin K ((∏ i ∈ s, p i).rootSet L)

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)
F : IntermediateField K L := ⨆ i ∈ s, t i
⊢ IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Tactic:
have hF : ∀ i ∈ s, t i ≤ F := fun i hi ↦ le_iSup_of_le i (le_iSup (fun _ ↦ t i) hi)

Result:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
⊢ IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)
⊢ ⨆ i ∈ s, t i = ⨆ i ∈ s, adjoin K ((p i).rootSet L)

Tactic:
exact iSup_congr fun i ↦ iSup_congr fun hi ↦ (h i hi).2

Result:
no goals

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)
⊢ IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Tactic:
let F : IntermediateField K L := ⨆ i ∈ s, t i

Result:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)
F : IntermediateField K L := ⨆ i ∈ s, t i
⊢ IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)
⊢ Splits (algebraMap K ↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i) ∧ ⨆ i ∈ s, t i = adjoin K ((∏ i ∈ s, p i).rootSet L)

Tactic:
refine
  ⟨splits_prod (algebraMap K F) fun i hi ↦
      splits_comp_of_splits (algebraMap K (t i)) (inclusion (hF i hi)).toRingHom
        (h i hi).1,
    ?_⟩

Result:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)
⊢ ⨆ i ∈ s, t i = adjoin K ((∏ i ∈ s, p i).rootSet L)

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)
⊢ ⨆ i ∈ s, t i = adjoin K ((∏ i ∈ s, p i).rootSet L)

Tactic:
simp only [rootSet_prod p s h0, ← Set.iSup_eq_iUnion, (@gc K _ L _ _).l_iSup₂]

Result:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits (algebraMap K ↥(t i)) (p i) ∧ t i = adjoin K ((p i).rootSet L)
⊢ ⨆ i ∈ s, t i = ⨆ i ∈ s, adjoin K ((p i).rootSet L)