-- Mathlib/RingTheory/Adjoin/FG.lean
theorem fg_trans (h1 : (adjoin R s).toSubmodule.FG) (h2 : (adjoin (adjoin R s) t).toSubmodule.FG) :
    (adjoin R (s ∪ t)).toSubmodule.FG

Proof state:
case intro.intro.intro.intro.refine_2.intro.intro.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a => a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a => a • v i
⊢ ∀ c ∈ l2.support, (fun a c => c • _root_.id a * _root_.id z) c (l2 c) ∈ span R (p * q)

Tactic:
intro t ht

Result:
case intro.intro.intro.intro.refine_2.intro.intro.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a => a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ (fun a c => c • _root_.id a * _root_.id z) t (l2 t) ∈ span R (p * q)

Proof state:
case intro.intro.intro.intro.refine_2.intro.intro.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a => a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ _root_.id t * _root_.id z ∈ span R (p * q)

Tactic:
exact subset_span ⟨t, hlp ht, z, hlq hz, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ y ∈ adjoin R (s ∪ t)

Tactic:
have : y ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) := by
  rw [← hq']
  exact subset_span hy

Result:
case intro.intro.intro.intro.refine_1.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
this : y ∈ Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ y ∈ adjoin R (s ∪ t)

Proof state:
case intro.intro.intro.intro.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin R (s ∪ t))
⊢ r ∈ span R (p * q)

Tactic:
change r ∈ adjoin R (s ∪ t) at hr

Result:
case intro.intro.intro.intro.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr : r ∈ adjoin R (s ∪ t)
⊢ r ∈ span R (p * q)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
⊢ (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG

Tactic:
rcases fg_def.1 h1 with ⟨p, hp, hp'⟩

Result:
case intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
⊢ (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG