awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ Membership.mem (γ := Submodule R A) (span R (p * q)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
have hl₁ : 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
Cleared hypotheses: hl, 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
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)) ((↑((l : (a : A) → ↥(adjoin R s)) z) : A) * _root_.id z)
have 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)
Tactic: rw [← hl, Finsupp.sum_mul]
-- 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
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)
have 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))
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_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)
have 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))
Tactic: rw [smul_mul_assoc]
-- 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_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))
have refine_2 : Membership.mem (γ := Submodule R A) (span R (p * q)) (_root_.id t * _root_.id z)
Tactic: refine smul_mem _ _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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)) ⊤
⊢ 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)
have rw : (↑s : Set A) ⊆
  (↑((toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (↑s : Set A)) : Submodule R A) : Set A)
Tactic: rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
⊢ (S.prod T).FG
have obtain : ∀ (s : Set A) (hs : s.Finite ∧ Algebra.adjoin R s = S), (S.prod T).FG
Tactic: obtain ⟨s, hs⟩ := fg_def.1 hS
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
⊢ (S.prod T).FG
have obtain : ∀ (t : Set B) (ht : t.Finite ∧ Algebra.adjoin R t = T), (S.prod T).FG
Tactic: obtain ⟨t, ht⟩ := fg_def.1 hT
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ (S.prod T).FG
have rw : FG (Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t))
Tactic: rw [← hs.2, ← ht.2]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs : S.FG
⊢ (Subalgebra.map f S).FG
have let : ∀ (s : Finset A) (hs : Algebra.adjoin R (↑s : Set A) = S), (Subalgebra.map f S).FG
Tactic: let ⟨s, hs⟩ := hs
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs_1 : S.FG
s : Finset A
hs : Algebra.adjoin R (↑s : Set A) = S
⊢ Algebra.adjoin R (↑(Finset.image (⇑f : (a : A) → B) s) : Set B) = Subalgebra.map f S
have rw : Algebra.adjoin R ((⇑f : (a : A) → B) '' (↑s : Set A)) = Subalgebra.map f S
Tactic: rw [Finset.coe_image, Algebra.adjoin_image, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs_1 : S.FG
s : Finset A
hs : Algebra.adjoin R (↑s : Set A) = S
rw : Algebra.adjoin R ((⇑f : (a : A) → B) '' (↑s : Set A)) = Subalgebra.map f S
⊢ Algebra.adjoin R (↑(Finset.image (⇑f : (a : A) → B) s) : Set B) = Subalgebra.map f S
have rw₁ : Subalgebra.map f (Algebra.adjoin R (↑s : Set A)) = Subalgebra.map f S
Tactic: rw [Finset.coe_image, Algebra.adjoin_image, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs_1 : S.FG
s : Finset A
hs : Algebra.adjoin R (↑s : Set A) = S
rw : Algebra.adjoin R ((⇑f : (a : A) → B) '' (↑s : Set A)) = Subalgebra.map f S
rw₁ : Subalgebra.map f (Algebra.adjoin R (↑s : Set A)) = Subalgebra.map f S
⊢ Algebra.adjoin R (↑(Finset.image (⇑f : (a : A) → B) s) : Set B) = Subalgebra.map f S
have rw₂ : Subalgebra.map f S = Subalgebra.map f S
Tactic: rw [Finset.coe_image, Algebra.adjoin_image, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hs_1 : (map f S).FG
s : Finset B
hs : Algebra.adjoin R (↑s : Set B) = map f S
⊢ map f (Algebra.adjoin R (↑(s.preimage (⇑f : (a : A) → B) ⋯) : Set A)) = map f S
have rw : (↑s : Set B) ⊆ Set.range.{w, v + 1} (ι := A) (⇑f : (a : A) → B)
Tactic: rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hs_1 : (map f S).FG
s : Finset B
hs : Algebra.adjoin R (↑s : Set B) = map f S
⊢ (↑s : Set B) ⊆ Set.range.{w, v + 1} (ι := A) (⇑f : (a : A) → B)
have rw : map f S ≤ map f ⊤
Tactic: rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : FG.{u, v} (R := R) (A := ↥S) ⊤
⊢ S.FG
have rw : (map S.val ⊤).FG
Tactic: rw [← S.range_val, ← Algebra.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
⊢ P S
have obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
Tactic: obtain ⟨t, rfl⟩ := S.fg_of_noetherian
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t : Finset A
⊢ P (Algebra.adjoin R (↑t : Set A))
have refine_1 : P (Algebra.adjoin R (↑∅ : Set A))
Tactic: refine Finset.induction_on t ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t : Finset A
refine_1 : P (Algebra.adjoin R (↑∅ : Set A))
⊢ P (Algebra.adjoin R (↑t : Set A))
have refine_2 : ∀ (a : A) (s : Finset A), a ∉ s → P (Algebra.adjoin R (↑s : Set A)) → P (Algebra.adjoin R (↑(insert a s) : Set A))
Tactic: refine Finset.induction_on t ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t_1 : Finset A
x : A
t : Finset A
h_1 : x ∉ t
h : P (Algebra.adjoin R (↑t : Set A))
⊢ P (Algebra.adjoin R (↑(insert x t) : Set A))
have refine_2 : P (Algebra.adjoin R (insert x (↑t : Set A)))
Tactic: rw [Finset.coe_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
⊢ P S
have obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
Tactic: classical
  obtain ⟨t, rfl⟩ := S.fg_of_noetherian
  refine Finset.induction_on t ?_ ?_
  · simpa using base
  intro x t _ h
  rw [Finset.coe_insert]
  simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
⊢ P S
have refine_1 : ∀ (t : Finset A), P (Algebra.adjoin R (↑∅ : Set A))
Tactic: classical
  obtain ⟨t, rfl⟩ := S.fg_of_noetherian
  refine Finset.induction_on t ?_ ?_
  · simpa using base
  intro x t _ h
  rw [Finset.coe_insert]
  simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
refine_1 : ∀ (t : Finset A), P (Algebra.adjoin R (↑∅ : Set A))
⊢ P S
have refine_2 : ∀ (t : Finset A) (a : A) (s : Finset A),
  a ∉ s → P (Algebra.adjoin R (↑s : Set A)) → P (Algebra.adjoin R (↑(insert a s) : Set A))
Tactic: classical
  obtain ⟨t, rfl⟩ := S.fg_of_noetherian
  refine Finset.induction_on t ?_ ?_
  · simpa using base
  intro x t _ h
  rw [Finset.coe_insert]
  simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
refine_1 : ∀ (t : Finset A), P (Algebra.adjoin R (↑∅ : Set A))
refine_2 refine_2₁ refine_2₂ :
  ∀ (t : Finset A) (x : A) (t : Finset A),
    x ∉ t → ∀ (h : P (Algebra.adjoin R (↑t : Set A))), P (Algebra.adjoin R (↑(insert x t) : Set A))
⊢ P S
have refine_2₃ : ∀ (t : Finset A) (x : A) (t : Finset A),
  x ∉ t → ∀ (h : P (Algebra.adjoin R (↑t : Set A))), P (Algebra.adjoin R (insert x (↑t : Set A)))
Tactic: classical
  obtain ⟨t, rfl⟩ := S.fg_of_noetherian
  refine Finset.induction_on t ?_ ?_
  · simpa using base
  intro x t _ h
  rw [Finset.coe_insert]
  simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
⊢ Algebra.adjoin R (s ∪ s') = S ⊔ S'
have rw : Algebra.adjoin R s ⊔ Algebra.adjoin R s' = S ⊔ S'
Tactic: rw [Algebra.adjoin_union, hs.2, hs'.2]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
rw : Algebra.adjoin R s ⊔ Algebra.adjoin R s' = S ⊔ S'
⊢ Algebra.adjoin R (s ∪ s') = S ⊔ S'
have rw₁ : S ⊔ Algebra.adjoin R s' = S ⊔ S'
Tactic: rw [Algebra.adjoin_union, hs.2, hs'.2]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
rw : Algebra.adjoin R s ⊔ Algebra.adjoin R s' = S ⊔ S'
rw₁ : S ⊔ Algebra.adjoin R s' = S ⊔ S'
⊢ Algebra.adjoin R (s ∪ s') = S ⊔ S'
have rw₂ : S ⊔ S' = S ⊔ S'
Tactic: rw [Algebra.adjoin_union, hs.2, hs'.2]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FGBaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
have obtain : ∀ (S : Finset (A × B)) (hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2),
  ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
Tactic: obtain ⟨S, hS⟩ := TensorProduct.exists_finset x
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FGBaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
have refine_1 : Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))
Tactic: refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩