case mk
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx : x ∈ ⨆ (i : ι), f i
⊢ IsAlgebraic K { val := x, property := hx }
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
⊢ Algebra.IsAlgebraic K { x // x ∈ ⨆ (i : ι), f i }
rintro ⟨x, hx⟩
case mk.intro
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx✝ : x ∈ ⨆ (i : ι), f i
s : Finset ((i : ι) × { x // x ∈ f i })
hx : x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), K⟮↑i.snd⟯
⊢ IsAlgebraic K { val := x, property := hx✝ }
case mk
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx : x ∈ ⨆ (i : ι), f i
⊢ IsAlgebraic K { val := x, property := hx }
obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx
case mk.intro
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx✝ : x ∈ ⨆ (i : ι), f i
s : Finset ((i : ι) × { x // x ∈ f i })
hx : x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), K⟮↑i.snd⟯
⊢ IsAlgebraic K { val := x, property := hx }
case mk.intro
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx✝ : x ∈ ⨆ (i : ι), f i
s : Finset ((i : ι) × { x // x ∈ f i })
hx : x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), K⟮↑i.snd⟯
⊢ IsAlgebraic K { val := x, property := hx✝ }
rw [isAlgebraic_iff, Subtype.coe_mk, ← Subtype.coe_mk (p := fun x => x ∈ _) x hx,
  ← isAlgebraic_iff]
case mk.intro
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx✝ : x ∈ ⨆ (i : ι), f i
s : Finset ((i : ι) × { x // x ∈ f i })
hx : x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), K⟮↑i.snd⟯
this : ∀ (i : (i : ι) × { x // x ∈ f i }), FiniteDimensional K { x // x ∈ K⟮↑i.snd⟯ }
⊢ IsAlgebraic K { val := x, property := hx }
case mk.intro
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx✝ : x ∈ ⨆ (i : ι), f i
s : Finset ((i : ι) × { x // x ∈ f i })
hx : x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), K⟮↑i.snd⟯
⊢ IsAlgebraic K { val := x, property := hx }
haveI : ∀ i : Σ i, f i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ =>
  adjoin.finiteDimensional (isIntegral_iff.1 (isAlgebraic_iff_isIntegral.1 (h i x)))
no goals
case mk.intro
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
h : ∀ (i : ι), Algebra.IsAlgebraic K { x // x ∈ f i }
x : L
hx✝ : x ∈ ⨆ (i : ι), f i
s : Finset ((i : ι) × { x // x ∈ f i })
hx : x ∈ ⨆ (i : (i : ι) × { x // x ∈ f i }) (_ : i ∈ s), K⟮↑i.snd⟯
this : ∀ (i : (i : ι) × { x // x ∈ f i }), FiniteDimensional K { x // x ∈ K⟮↑i.snd⟯ }
⊢ IsAlgebraic K { val := x, property := hx }
apply Algebra.isAlgebraic_of_finite