Theorem: Subalgebra.fg_sup (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hA : A.FG
hB : B.FG
⊢ (A ⊔ B).FG
Tactic:
classical
obtain ⟨s, hs⟩ := hA
obtain ⟨t, ht⟩ := hB
rw [← hs, ← ht, ← Algebra.adjoin_union, ← Finset.coe_union]
exact ⟨s ∪ t, rfl⟩
State after:
no goals

State before:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hA : A.FG
hB : B.FG
⊢ (A ⊔ B).FG
Tactic:
obtain ⟨s, hs⟩ := hA
State after:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hB : B.FG
s : Finset S
hs : Algebra.adjoin R ↑s = A
⊢ (A ⊔ B).FG

State before:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hB : B.FG
s : Finset S
hs : Algebra.adjoin R ↑s = A
⊢ (A ⊔ B).FG
Tactic:
obtain ⟨t, ht⟩ := hB
State after:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (A ⊔ B).FG

State before:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (A ⊔ B).FG
Tactic:
rw [← hs, ← ht, ← Algebra.adjoin_union, ← Finset.coe_union]
State after:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (Algebra.adjoin R ↑(s ∪ t)).FG

State before:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (Algebra.adjoin R ↑(s ∪ t)).FG
Tactic:
exact ⟨s ∪ t, rfl⟩
State after:
no goals