no goals
R : Type ?u.871187
S : Type ?u.871190
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
hKL : Algebra.IsAlgebraic K L
⊢ Nontrivial { x // x ∈ A }
infer_instance