awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Submodule (↥(adjoin R s)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
        (adjoin (↥(adjoin R s)) t) :
      Submodule (↥(adjoin R s)) A)
    y

Tactic:
have : y ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) := by
      rw [← hq']
      exact subset_span hy
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
this :
  Membership.mem (γ := Submodule (↥(adjoin R s)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
        (adjoin (↥(adjoin R s)) t) :
      Submodule (↥(adjoin R s)) A)
    y
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  Membership.mem (γ := Subalgebra R A) (Subalgebra.restrictScalars R (S := ↥(adjoin R s)) (adjoin (↥(adjoin R s)) t)) y
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) y

Tactic:
rwa [adjoin_union_eq_adjoin_adjoin]

Premises used: Algebra.adjoin_union_eq_adjoin_adjoin
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
r : A
hr :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)) : Submodule R A) r
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) r

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

Premises used: Algebra.adjoin, Union.union
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
r : A
hr : Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) r
⊢ Membership.mem (γ := Subalgebra R A) (Subalgebra.restrictScalars R (S := ↥(adjoin R s)) (adjoin (↥(adjoin R s)) t)) r

Tactic:
rw [adjoin_union_eq_adjoin_adjoin] at hr

Premises used: Algebra.adjoin_union_eq_adjoin_adjoin
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
r : A
hr :
  Membership.mem (γ := Subalgebra R A) (Subalgebra.restrictScalars R (S := ↥(adjoin R s)) (adjoin (↥(adjoin R s)) t)) r
⊢ Membership.mem (γ := Submodule (↥(adjoin R s)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
        (adjoin (↥(adjoin R s)) t) :
      Submodule (↥(adjoin R s)) A)
    r

Tactic:
change r ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) at hr

Premises used: Algebra.adjoin, Membership.mem, Subtype, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
r : A
hr :
  Membership.mem (γ := Submodule (↥(adjoin R s)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
        (adjoin (↥(adjoin R s)) t) :
      Submodule (↥(adjoin R s)) A)
    r
⊢ ∃ (l : A →₀ ↥(adjoin R s)),
    Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
        (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l ∧
      (Finsupp.linearCombination (↥(adjoin R s)) _root_.id : (a : A →₀ ↥(adjoin R s)) → A) l = r

Tactic:
rw [← hq', ← Set.image_id q, Finsupp.mem_span_image_iff_linearCombination (adjoin R s)] at hr

Premises used: Algebra.adjoin, Membership.mem, Subtype, Finsupp.mem_span_image_iff_linearCombination, Set.image_id
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
r : A
hr :
  ∃ (l : A →₀ ↥(adjoin R s)),
    Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
        (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l ∧
      (Finsupp.linearCombination (↥(adjoin R s)) _root_.id : (a : A →₀ ↥(adjoin R s)) → A) l = r
refine_2 :
  ∀ (l : A →₀ ↥(adjoin R s))
    (hlq :
      Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
        (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l),
    Membership.mem (α := A) (γ := Submodule R A) (span R (p * q))
      ((Finsupp.linearCombination (↥(adjoin R s)) _root_.id : (a : A →₀ ↥(adjoin R s)) → A) l : A)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) r

Tactic:
rcases hr with ⟨l, hlq, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
⊢ ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)

Tactic:
have := @Finsupp.linearCombination_apply A A (adjoin R s)
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
refine_2 :
  Membership.mem (γ := Submodule R A) (span R (p * q))
    (∑ a ∈ l.support, HSMul.hSMul (α := ↥(adjoin R s)) ((l : (a : A) → ↥(adjoin R s)) a : ↥(adjoin R s)) (_root_.id a))
⊢ Membership.mem (α := A) (γ := Submodule R A) (span R (p * q))
    ((Finsupp.linearCombination (↥(adjoin R s)) _root_.id : (a : A →₀ ↥(adjoin R s)) → A) l : A)

Tactic:
rw [this, Finsupp.sum]

Premises used: Finsupp.sum
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q))
    (∑ a ∈ l.support, HSMul.hSMul (α := ↥(adjoin R s)) ((l : (a : A) → ↥(adjoin R s)) a : ↥(adjoin R s)) (_root_.id a))

Tactic:
sum_mem ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
refine_2 :
  ∀ c ∈ l.support,
    Membership.mem (γ := Submodule R A) (span R (p * q))
      (HSMul.hSMul (α := ↥(adjoin R s)) ((l : (a : A) → ↥(adjoin R s)) c : ↥(adjoin R s)) (_root_.id c))
⊢ Membership.mem (γ := Submodule R A) (span R (p * q))
    (∑ a ∈ l.support, HSMul.hSMul (α := ↥(adjoin R s)) ((l : (a : A) → ↥(adjoin R s)) a : ↥(adjoin R s)) (_root_.id a))

Tactic:
refine sum_mem ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
z : A
hz : z ∈ l.support
refine_2 : Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q))
    (HSMul.hSMul (α := ↥(adjoin R s)) ((l : (a : A) → ↥(adjoin R s)) z : ↥(adjoin R s)) (_root_.id z))

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

Premises used: Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
z : A
hz : z ∈ l.support
⊢ Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
    (↑((l : (a : A) → ↥(adjoin R s)) z) : A)

Tactic:
have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this_1 :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
z : A
hz : z ∈ l.support
this :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
    (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
⊢ ∃ (l_1 : A →₀ R),
    Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l_1 ∧
      Eq.{v + 1} (α := A) ((Finsupp.linearCombination R _root_.id : (a : A →₀ R) → A) l_1 : A)
        ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) : A)

Tactic:
rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_linearCombination R] at this

Premises used: Finsupp.mem_span_image_iff_linearCombination, Set.image_id
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this_1 :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
z : A
hz : z ∈ l.support
this :
  ∃ (l_1 : A →₀ R),
    Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l_1 ∧
      Eq.{v + 1} (α := A) ((Finsupp.linearCombination R _root_.id : (a : A →₀ R) → A) l_1 : A)
        ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) : A)
refine_2 :
  ∀ (l2 : A →₀ R) (hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2)
    (hl :
      Eq.{v + 1} (α := A) ((Finsupp.linearCombination R _root_.id : (a : A →₀ R) → A) l2 : A)
        ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) : A)),
    Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)

Tactic:
rcases this with ⟨l2, hlp, hl⟩
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
l : A →₀ ↥(adjoin R s)
hlq :
  Membership.mem (γ := Submodule (↥(adjoin R s)) (A →₀ ↥(adjoin R s)))
    (Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q) l
this :
  ∀ [inst_3 : Semiring ↥(adjoin R s)] [inst_4 : AddCommMonoid A] [inst_5 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)),
    Eq (α := A) ((Finsupp.linearCombination (↥(adjoin R s)) v : (a : A →₀ ↥(adjoin R s)) → A) l : A)
      (l.sum fun (i : A) (a : ↥(adjoin R s)) ↦ a • v i : A)
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl :
  Eq.{v + 1} (α := A) ((Finsupp.linearCombination R _root_.id : (a : A →₀ R) → A) l2 : A)
    ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) : A)
⊢ ∀ [inst : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Module R A] {v : A → A} (l : A →₀ R),
    Eq (α := A) ((Finsupp.linearCombination R v : (a : A →₀ R) → A) l : A) (l.sum fun (i : A) (a : R) ↦ a • v i : A)

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