-- 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 : (Finsupp.linearCombination R _root_.id) l2 = ↑(l z)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
have := @Finsupp.linearCombination_apply A A R

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 : (Finsupp.linearCombination R _root_.id) l2 = ↑(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
⊢ ↑(l z) * _root_.id z ∈ 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 : (Finsupp.linearCombination R _root_.id) l2 = ↑(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
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
rw [this] at hl

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
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Proof state:
case intro.intro.intro.intro.refine_2.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
⊢ l z • _root_.id z ∈ span R (p * q)

Tactic:
change (l z).1 * _ ∈ _

Result:
case intro.intro.intro.intro.refine_2.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
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)