awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) y
have refine_1 : Membership.mem (γ := Subalgebra R A) (Subalgebra.restrictScalars R (S := ↥(adjoin R s)) (adjoin (↥(adjoin R s)) t)) y
Tactic: rwa [adjoin_union_eq_adjoin_adjoin]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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 (γ := Submodule R A) (span R (p * q)) r
have hr₁ : Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) r
Tactic: change r ∈ adjoin R (s ∪ t) at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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 (γ := Submodule R A) (span R (p * q)) r
have hr₁ : 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
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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 R A) (span R (p * q)) r
have 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
Tactic: change r ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) r
have 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
Tactic: rw [← hq', ← Set.image_id q, Finsupp.mem_span_image_iff_linearCombination (adjoin R s)] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) r
have 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)
Tactic: rcases hr with ⟨l, hlq, rfl⟩
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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
⊢ 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)
have 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)
Tactic: have := @Finsupp.linearCombination_apply A A (adjoin R s)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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 (α := A) (γ := Submodule R A) (span R (p * q))
    ((Finsupp.linearCombination (↥(adjoin R s)) _root_.id : (a : A →₀ ↥(adjoin R s)) → A) l : A)
have 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))
Tactic: rw [this, Finsupp.sum]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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))
have 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))
Tactic: refine sum_mem ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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) (span R (p * q))
    (HSMul.hSMul (α := ↥(adjoin R s)) ((l : (a : A) → ↥(adjoin R s)) z : ↥(adjoin R s)) (_root_.id z))
have refine_2 : Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
Tactic: change (l z).1 * _ ∈ _
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
have 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)
Tactic: have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
have 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)
Tactic: rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_linearCombination R] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
have 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)
Tactic: rcases this with ⟨l2, hlp, hl⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
have 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)
Tactic: have := @Finsupp.linearCombination_apply A A R