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))
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
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)
this :
  ∀ [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)
⊢ Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)

Tactic:
rw [this] at 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_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
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)
this :
  ∀ [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)
hl₁ : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : 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:
rw [this] at 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_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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
refine_2 :
  Membership.mem (γ := Submodule R A) (span R (p * q)) (l2.sum fun (a : A) (c : R) ↦ c • _root_.id 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:
rw [← hl, Finsupp.sum_mul]

Premises used: Finsupp.sum_mul
-- 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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) (l2.sum fun (a : A) (c : R) ↦ c • _root_.id a * _root_.id z)

Tactic:
sum_mem ?_

Premises used: Set.Mem, Finsupp.sum, 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_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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
refine_2 :
  ∀ c ∈ l2.support,
    Membership.mem (γ := Submodule R A) (span R (p * q))
      ((fun (a : A) (c : R) ↦ c • _root_.id a * _root_.id z) c ((l2 : (a : A) → R) c))
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) (l2.sum fun (a : A) (c : R) ↦ c • _root_.id a * _root_.id z)

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_1 : 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_1))
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_1))
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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
t : A
ht : t ∈ l2.support
refine_2 :
  Membership.mem (γ := Submodule R A) (span R (p * q))
    (HSMul.hSMul.{u, v, v} (α := R) ((l2 : (a : A) → R) t : R) (_root_.id t * _root_.id z))
⊢ Membership.mem (γ := Submodule R A) (span R (p * q))
    (HSMul.hSMul.{u, v, v} (α := R) ((l2 : (a : A) → R) t : R) (_root_.id t) * _root_.id z)

Tactic:
rw [smul_mul_assoc]

Premises used: smul_mul_assoc
-- 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_1 : 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_1))
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_1))
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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
t : A
ht : t ∈ l2.support
⊢ Membership.mem (γ := Submodule R A) (span R (p * q))
    (HSMul.hSMul.{u, v, v} (α := R) ((l2 : (a : A) → R) t : R) (_root_.id t * _root_.id z))

Tactic:
smul_mem _ _ ?_

Premises used: Submodule.smul_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_1 : 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_1))
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_1))
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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
t : A
ht : t ∈ l2.support
refine_2 : Membership.mem (γ := Submodule R A) (span R (p * q)) (_root_.id t * _root_.id z)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q))
    (HSMul.hSMul.{u, v, v} (α := R) ((l2 : (a : A) → R) t : R) (_root_.id t * _root_.id z))

Tactic:
refine smul_mem _ _ ?_

Premises used: Submodule.smul_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_1 : 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_1))
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_1))
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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
t : A
ht : t ∈ l2.support
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) (_root_.id t * _root_.id z)

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

Premises used: And.intro, Exists.intro, Submodule.subset_span, 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_1 : 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_1))
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_1))
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
l2 : A →₀ R
hlp : Membership.mem (γ := Submodule R (A →₀ R)) (Finsupp.supported R R p) l2
hl : Eq (α := A) (l2.sum fun (i : A) (a : R) ↦ a • _root_.id i) (↑((l : (a : A) → ↥(adjoin R s)) z) : A)
this :
  ∀ [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)
t : A
ht : t ∈ l2.support
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) (_root_.id t * _root_.id z)

Tactic:
exact subset_span ⟨t, hlp ht, z, hlq hz, rfl⟩
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
⊢ FG (Algebra.adjoin R (↑s : Set A))

Tactic:
⟨s, rfl⟩

Premises used: Subalgebra.FG, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.FG ↔ ∃ (t : Set A), t.Finite ∧ Algebra.adjoin R t = S

Tactic:
Iff.symm Set.exists_finite_iff_finset

Premises used: Set.exists_finite_iff_finset, Iff.symm
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ FG.{u, v} (R := R) (A := A) ⊥

Tactic:
⟨∅, Finset.coe_empty ▸ Algebra.adjoin_empty R A⟩

Premises used: Subalgebra.FG, Finset.coe_empty, Eq.rec, Exists.intro, EmptyCollection.emptyCollection, Eq.symm, Algebra.adjoin_empty
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : Submodule.FG.{u, v} (R := R) (M := A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
t : Finset A
ht : Eq (α := Submodule R A) (span R (↑t : Set A)) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
x : A
hx rw : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑t : Set A)) x

Tactic:
rw [ht]
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : Submodule.FG.{u, v} (R := R) (M := A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
t : Finset A
ht : Eq (α := Submodule R A) (span R (↑t : Set A)) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
x : A
hx : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x

Tactic:
hx
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : Submodule.FG.{u, v} (R := R) (M := A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
t : Finset A
ht : Eq (α := Submodule R A) (span R (↑t : Set A)) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
x : A
hx : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x

Tactic:
exact hx
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
S : Subalgebra R A
⊢ S.FG

Tactic:
fg_of_fg_toSubmodule (IsNoetherian.noetherian (Subalgebra.toSubmodule S))

Premises used: Subalgebra.fg_of_fg_toSubmodule, IsNoetherian.noetherian, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Submodule.FG.{u, v} (R := R) (M := A) ⊤
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
rw :
  (↑s : Set A) ⊆
    (↑((toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (↑s : Set A)) : Submodule R A) : Set A)
⊢ Eq (α := Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (↑s : Set A)) : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊤ : Submodule R A)

Tactic:
rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]

Premises used: eq_top_iff, Algebra.top_toSubmodule, Submodule.span_le
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Submodule.FG.{u, v} (R := R) (M := A) ⊤
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
⊢ (↑s : Set A) ⊆
    (↑((toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (↑s : Set A)) : Submodule R A) : Set A)

Tactic:
Algebra.subset_adjoin

Premises used: iInf, Set.iInter, Algebra.subset_adjoin, setOf