Theorem: Subalgebra.FG.sup (DividedPowers/ForMathlib/DirectLimit.lean)

State before:
R✝ : Type u_1
S✝ : Type u_2
N : Type u_3
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ N
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A A' : Subalgebra R S
hA : A.FG
hA' : A'.FG
s : Set S
hs : s.Finite ∧ Algebra.adjoin R s = A
s' : Set S
hs' : s'.Finite ∧ Algebra.adjoin R s' = A'
⊢ Algebra.adjoin R (s ∪ s') = A ⊔ A'
Tactic:
rw [Algebra.adjoin_union, hs.2, hs'.2]
State after:
no goals