-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_adjoin_of_tower (s : Set A) : adjoin S (adjoin R s : Set A) = adjoin S s

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin S ↑(adjoin R s) = adjoin S s

Tactic:
apply le_antisymm (adjoin_le _)

Result:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin S s ≤ adjoin S ↑(adjoin R s)

R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ ↑(adjoin R s) ⊆ ↑(adjoin S s)

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
this : ↑(Subalgebra.restrictScalars R (adjoin S s)) = ↑(adjoin S s)
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin S s))

Tactic:
rw [this]

Result:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
this : ↑(Subalgebra.restrictScalars R (adjoin S s)) = ↑(adjoin S s)
⊢ s ⊆ ↑(adjoin S s)

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ ↑(adjoin R s) ⊆ ↑(adjoin S s)

Tactic:
change adjoin R s ≤ (adjoin S s).restrictScalars R

Result:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin R s ≤ Subalgebra.restrictScalars R (adjoin S s)

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin S s))

Tactic:
have : (Subalgebra.restrictScalars R (adjoin S s) : Set A) = adjoin S s := rfl

Result:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
this : ↑(Subalgebra.restrictScalars R (adjoin S s)) = ↑(adjoin S s)
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin S s))

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
this : ↑(Subalgebra.restrictScalars R (adjoin S s)) = ↑(adjoin S s)
⊢ s ⊆ ↑(adjoin S s)

Tactic:
exact subset_adjoin

Result:
no goals

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin R s ≤ Subalgebra.restrictScalars R (adjoin S s)

Tactic:
refine adjoin_le ?_

Result:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin S s))

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin S s ≤ adjoin S ↑(adjoin R s)

Tactic:
exact adjoin_mono subset_adjoin

Result:
no goals