[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ ↑(algebraMap R A) x ∈ U.carrier
[PROOFSTEP]
rw [algebraMap_apply R S A]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ ↑(algebraMap S A) (↑(algebraMap R S) x) ∈ U.carrier
[PROOFSTEP]
exact U.algebraMap_mem _
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
⊢ ↑(restrictScalars R ⊤) = ↑⊤
[PROOFSTEP]
dsimp
  -- porting note: why does `rfl` not work instead of `by dsimp`?
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ U ↔ x ∈ V
[PROOFSTEP]
rw [← mem_restrictScalars R, H, mem_restrictScalars]
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ LinearMap.range (toAlgHom R { x // x ∈ S } A) = ↑toSubmodule S
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ LinearMap.range (toAlgHom R { x // x ∈ S } A) ↔ x✝ ∈ ↑toSubmodule S
[PROOFSTEP]
simp only [← Submodule.range_subtype (Subalgebra.toSubmodule S), LinearMap.mem_range, IsScalarTower.coe_toAlgHom',
  Subalgebra.mem_toSubmodule]
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ (∃ y, ↑(algebraMap { x // x ∈ S } A) y = x✝) ↔ ∃ y, ↑(Submodule.subtype (↑toSubmodule S)) y = x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
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
t : Set A
z : A
⊢ z ∈ Subsemiring.closure (Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ↑(algebraMap S A) ∪ t)
[PROOFSTEP]
suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by rw [this]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
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
t : Set A
z : A
this : Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) = Set.range ↑(algebraMap S A)
⊢ z ∈ Subsemiring.closure (Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ↑(algebraMap S A) ∪ t)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
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
t : Set A
z : A
⊢ Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) = Set.range ↑(algebraMap S A)
[PROOFSTEP]
ext z
[GOAL]
case h
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
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
t : Set A
z✝ z : A
⊢ z ∈ Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) ↔ z ∈ Set.range ↑(algebraMap S A)
[PROOFSTEP]
exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩
