[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
⊢ Subalgebra.restrictScalars C (adjoin D S) =
    Subalgebra.restrictScalars C (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } S)
[PROOFSTEP]
suffices Set.range (algebraMap D E) = Set.range (algebraMap ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) E)
  by
  ext x
  change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
  rw [this]
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this :
  Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
⊢ Subalgebra.restrictScalars C (adjoin D S) =
    Subalgebra.restrictScalars C (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } S)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this :
  Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
x : E
⊢ x ∈ Subalgebra.restrictScalars C (adjoin D S) ↔
    x ∈ Subalgebra.restrictScalars C (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } S)
[PROOFSTEP]
change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this :
  Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
x : E
⊢ x ∈ Subsemiring.closure (Set.range ↑(algebraMap D E) ∪ S) ↔
    x ∈ Subsemiring.closure (Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E) ∪ S)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
⊢ Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ↑(algebraMap D E) ↔
    x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ↑(algebraMap D E) →
    x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
y : D
hy : ↑(algebraMap D E) y = x
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
exact ⟨⟨algebraMap D E y, ⟨y, ⟨Algebra.mem_top, rfl⟩⟩⟩, hy⟩
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E) →
    x ∈ Set.range ↑(algebraMap D E)
[PROOFSTEP]
rintro ⟨⟨y, ⟨z, ⟨h0, h1⟩⟩⟩, h2⟩
[GOAL]
case h.mpr.intro.mk.intro.intro
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x y : E
z : D
h0 : z ∈ ↑⊤.toSubsemiring
h1 : ↑↑(IsScalarTower.toAlgHom C D E) z = y
h2 :
  ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
      { val := y, property := (_ : ∃ a, a ∈ ↑⊤.toSubsemiring ∧ ↑↑(IsScalarTower.toAlgHom C D E) a = y) } =
    x
⊢ x ∈ Set.range ↑(algebraMap D E)
[PROOFSTEP]
exact ⟨z, Eq.trans h1 h2⟩
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin E (↑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin D (↑(algebraMap E F) '' T))
[PROOFSTEP]
rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image, ← Algebra.adjoin_image,
  ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom, IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ←
  adjoin_union_eq_adjoin_adjoin, ← adjoin_union_eq_adjoin_adjoin, Set.union_comm]
[GOAL]
R✝ : Type u
S✝ : Type v
A✝ : Type w
B : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hRS : Subalgebra.FG ⊤
hSA : Subalgebra.FG ⊤
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R ↑(Finset.image (↑(algebraMap S A)) s ∪ t) = ⊤
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union_eq_adjoin_adjoin, Algebra.adjoin_algebraMap, hs,
  Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ht, Subalgebra.restrictScalars_top]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
hAC : Subalgebra.FG ⊤
hBC : FG ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
cases' hAC with x hx
[GOAL]
case intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
hBC : FG ⊤
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
cases' hBC with y hy
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
have := hy
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy this : span B ↑y = ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
simp_rw [eq_top_iff', mem_span_finset] at this 
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), ∃ f, (Finset.sum y fun i => f i • i) = x
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
choose f hf using this
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
let s : Finset B := Finset.image₂ f (x ∪ y * y) y
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
have hxy : ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := fun xi hxi =>
  hf xi ▸
    sum_mem fun yj hyj =>
      smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
        ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
        (subset_span <| mem_insert_of_mem hyj)
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
have hyy :
  span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
  by
  rw [span_mul_span, span_le, coe_insert]
  rintro _ ⟨yi, yj, rfl | hyi, rfl | hyj, rfl⟩ <;> dsimp
  · rw [mul_one]
    exact subset_span (Set.mem_insert _ _)
  · rw [one_mul]
    exact subset_span (Set.mem_insert_of_mem _ hyj)
  · rw [mul_one]
    exact subset_span (Set.mem_insert_of_mem _ hyi)
  · rw [← hf (yi * yj)]
    exact
      SetLike.mem_coe.2
        (sum_mem fun yk hyk =>
          smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
            ⟨f (yi * yj) yk, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
            (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
[PROOFSTEP]
rw [span_mul_span, span_le, coe_insert]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ insert 1 ↑y * insert 1 ↑y ⊆ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
rintro _ ⟨yi, yj, rfl | hyi, rfl | hyj, rfl⟩
[GOAL]
case intro.intro.intro.inl.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ (fun x x_1 => x * x_1) 1 1 ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inl.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ (fun x x_1 => x * x_1) 1 yj ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inr.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
⊢ (fun x x_1 => x * x_1) yi 1 ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inr.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi yj : C
hyi : yi ∈ ↑y
hyj : yj ∈ ↑y
⊢ (fun x x_1 => x * x_1) yi yj ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inl.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ 1 * 1 ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [mul_one]
[GOAL]
case intro.intro.intro.inl.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ 1 ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact subset_span (Set.mem_insert _ _)
[GOAL]
case intro.intro.intro.inl.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [one_mul]
[GOAL]
case intro.intro.intro.inl.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ yj ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact subset_span (Set.mem_insert_of_mem _ hyj)
[GOAL]
case intro.intro.intro.inr.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [mul_one]
[GOAL]
case intro.intro.intro.inr.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
⊢ yi ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact subset_span (Set.mem_insert_of_mem _ hyi)
[GOAL]
case intro.intro.intro.inr.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi yj : C
hyi : yi ∈ ↑y
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [← hf (yi * yj)]
[GOAL]
case intro.intro.intro.inr.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi yj : C
hyi : yi ∈ ↑y
hyj : yj ∈ ↑y
⊢ (Finset.sum y fun i => f (yi * yj) i • i) ∈
    ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact
  SetLike.mem_coe.2
    (sum_mem fun yk hyk =>
      smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
        ⟨f (yi * yj) yk, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
        (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
refine' ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, _⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) = ⊤
[PROOFSTEP]
refine' restrictScalars_injective A (Algebra.adjoin A s) C _
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ restrictScalars A (span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)) = restrictScalars A ⊤
[PROOFSTEP]
rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span, span_le]
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ ↑(Submonoid.closure ↑x) ⊆ ↑(restrictScalars A (span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)))
[PROOFSTEP]
refine' fun r hr =>
  Submonoid.closure_induction hr (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _) fun p q hp hq =>
    hyy <| Submodule.mul_mem_mul hp hq
