K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_1
f : ι → IntermediateField K L
s : Finset ι
h : ∀ (i : ι), i ∈ s → FiniteDimensional K { x // x ∈ f i }
this : ∀ (i : { i // i ∈ s }), FiniteDimensional K { x // x ∈ f ↑i }
⊢ FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_1
f : ι → IntermediateField K L
s : Finset ι
h : ∀ (i : ι), i ∈ s → FiniteDimensional K { x // x ∈ f i }
⊢ FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }
haveI : ∀ i : { i // i ∈ s }, FiniteDimensional K (f i) := fun i => h i i.2
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_1
f : ι → IntermediateField K L
s : Finset ι
h : ∀ (i : ι), i ∈ s → FiniteDimensional K { x // x ∈ f i }
this✝ : ∀ (i : { i // i ∈ s }), FiniteDimensional K { x // x ∈ f ↑i }
this : (⨆ (i : ι) (_ : i ∈ s), f i) = ⨆ (i : { i // i ∈ s }), f ↑i
⊢ FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_1
f : ι → IntermediateField K L
s : Finset ι
h : ∀ (i : ι), i ∈ s → FiniteDimensional K { x // x ∈ f i }
this : ∀ (i : { i // i ∈ s }), FiniteDimensional K { x // x ∈ f ↑i }
⊢ FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }
have : (⨆ i ∈ s, f i) = ⨆ i : { i // i ∈ s }, f i :=
  le_antisymm (iSup_le fun i => iSup_le fun h => le_iSup (fun i : { i // i ∈ s } => f i) ⟨i, h⟩)
    (iSup_le fun i => le_iSup_of_le i (le_iSup_of_le i.2 le_rfl))
no goals
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_1
f : ι → IntermediateField K L
s : Finset ι
h : ∀ (i : ι), i ∈ s → FiniteDimensional K { x // x ∈ f i }
this✝ : ∀ (i : { i // i ∈ s }), FiniteDimensional K { x // x ∈ f ↑i }
this : (⨆ (i : ι) (_ : i ∈ s), f i) = ⨆ (i : { i // i ∈ s }), f ↑i
⊢ FiniteDimensional K { x // x ∈ ⨆ (i : ι) (_ : i ∈ s), f i }
exact this.symm ▸ IntermediateField.finiteDimensional_iSup_of_finite