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)
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)
suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by
  rw [this]
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)
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)
ext z
no goals
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)
exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩
no goals
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)
rw [this]