R : Type u_1
S : Type u_2
T : Type ?u.717680
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.717983
B✝ : Type ?u.717986
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.718408
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {B.gen} ≤ adjoin R {x}
R : Type u_1
S : Type u_2
T : Type ?u.717680
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.717983
B✝ : Type ?u.717986
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.718408
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {x} = ⊤
rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]
R : Type u_1
S : Type u_2
T : Type ?u.717680
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.717983
B✝ : Type ?u.717986
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.718408
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ {B.gen} ⊆ ↑(adjoin R {x})
R : Type u_1
S : Type u_2
T : Type ?u.717680
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.717983
B✝ : Type ?u.717986
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.718408
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {B.gen} ≤ adjoin R {x}
refine' adjoin_le _
no goals
R : Type u_1
S : Type u_2
T : Type ?u.717680
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.717983
B✝ : Type ?u.717986
inst✝⁴ : CommRing A
inst✝³ : CommRing B✝
inst✝² : IsDomain B✝
inst✝¹ : Algebra A B✝
K : Type ?u.718408
inst✝ : Field K
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ {B.gen} ⊆ ↑(adjoin R {x})
simp [hx]