case intro
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
⊢ FiniteType A B
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
⊢ FiniteType A B
obtain ⟨S, hS⟩ := hB.out
case intro
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ b ∈ adjoin A ↑S
case intro
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
⊢ FiniteType A B
refine' ⟨⟨S, eq_top_iff.2 fun b => _⟩⟩
case intro
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
le : adjoin R ↑S ≤ Subalgebra.restrictScalars R (adjoin A ↑S)
⊢ b ∈ adjoin A ↑S
case intro
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ b ∈ adjoin A ↑S
have le : adjoin R (S : Set B) ≤ Subalgebra.restrictScalars R (adjoin A S) := by
  apply (Algebra.adjoin_le _ : adjoin R (S : Set B) ≤ Subalgebra.restrictScalars R (adjoin A ↑S))
  simp only [Subalgebra.coe_restrictScalars]
  exact Algebra.subset_adjoin
no goals
case intro
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
le : adjoin R ↑S ≤ Subalgebra.restrictScalars R (adjoin A ↑S)
⊢ b ∈ adjoin A ↑S
exact le (eq_top_iff.1 hS b)
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ ↑S ⊆ ↑(Subalgebra.restrictScalars R (adjoin A ↑S))
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ adjoin R ↑S ≤ Subalgebra.restrictScalars R (adjoin A ↑S)
apply (Algebra.adjoin_le _ : adjoin R (S : Set B) ≤ Subalgebra.restrictScalars R (adjoin A ↑S))
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ ↑S ⊆ ↑(adjoin A ↑S)
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ ↑S ⊆ ↑(Subalgebra.restrictScalars R (adjoin A ↑S))
simp only [Subalgebra.coe_restrictScalars]
no goals
R : Type u_2
A : Type u
B : Type u_1
M : Type ?u.14580
N : Type ?u.14583
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ ↑S ⊆ ↑(adjoin A ↑S)
exact Algebra.subset_adjoin