awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
mp :
  Eq.{uA + 1} (α := Set A)
    (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
      (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
            FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
        (a : FreeAlgebra R ↥s) → A))
    Set.univ
mp₁ :
  (↑(AlgHom.range (A := FreeAlgebra.{uR, uA} R ↥s)
          ((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) :
      Set A) =
    Set.univ
mp₂ : (↑(adjoin R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) : Set A) = Set.univ
mp₃ : (↑(adjoin R {x : A | x ∈ s}) : Set A) = Set.univ
mp₄ : (↑(adjoin R (↑s : Set A)) : Set A) = Set.univ
mp₅ : (↑⊤ : Set A) = Set.univ
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp₆ : Eq.{uA + 1} (α := Set A) Set.univ Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ FiniteType R S ↔
    ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
have mp : FiniteType R S →
  ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
    Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  FiniteType R S →
    ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
⊢ FiniteType R S ↔
    ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
have mpr : (∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
    Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)) →
  FiniteType R S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
    Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
have h : Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S)
  (⇑(MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))) : (a : MvPolynomial (↥s) R) → S)
Tactic: use s, MvPolynomial.aeval (↑)
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
x : S
⊢ ∃ (a : MvPolynomial.{uS, uR} (↥s) R),
    (MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → S) a = x
have h : Membership.mem (γ := Subalgebra R S) ⊤ x
Tactic: rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, SetLike.mem_coe, hs]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ FiniteType R A ↔
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
have mp : FiniteType R A →
  ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
    Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
mp :
  FiniteType R A →
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
⊢ FiniteType R A ↔
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
have mpr : (∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
    Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)) →
  FiniteType R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ FiniteType R A →
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
have mp : (∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
    Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)) →
  ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
    Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
Tactic: rw [iff_quotient_freeAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A
hsur : Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
w : Type uA
⊢ ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
    Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
have w₁ : Fintype ↥s
Tactic: use { x : A // x ∈ s }, inferInstance, f
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ FiniteType R S ↔
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
have mp : FiniteType R S →
  ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
    Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  FiniteType R S →
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ FiniteType R S ↔
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
have mpr : (∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
    Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)) →
  FiniteType R S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ FiniteType R S →
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
have mp : (∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
    Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)) →
  ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
    Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
Tactic: rw [iff_quotient_mvPolynomial]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S
hsur : Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
w : Type uS
⊢ ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
    Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
have w₁ : Fintype ↥s
Tactic: use { x : S // x ∈ s }, inferInstance, f
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ FiniteType R S ↔
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
have mp : FiniteType R S →
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  FiniteType R S →
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ FiniteType R S ↔
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
have mpr : (∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)) →
  FiniteType R S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ FiniteType R S →
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
have mp : (∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
    Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)) →
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
Tactic: rw [iff_quotient_mvPolynomial']
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
have mp : ∀ (equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R),
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
Tactic: have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ Subalgebra.FG (R := R) (A := A × B) ⊤
have rw : Subalgebra.FG (R := R) (A := A × B) (Subalgebra.prod ⊤ ⊤)
Tactic: rw [← Subalgebra.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
⊢ IsNoetherianRing S
have obtain : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), IsNoetherianRing S
Tactic: obtain ⟨s, hs⟩ := h.1
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ IsNoetherianRing S
have hf : Surjective (α := MvPolynomial.{u_2, u_1} (↥s) R) (β := S)
  (⇑(AlgHom.toRingHom (MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) : (a : MvPolynomial (↥s) R) → S)
Tactic: apply
    isNoetherianRing_of_surjective (MvPolynomial s R) S
      (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ Surjective (α := MvPolynomial.{u_2, u_1} (↥s) R) (β := S)
    (⇑(AlgHom.toRingHom (MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) : (a : MvPolynomial (↥s) R) → S)
have hf : (↑⊤ : Set S) = Set.univ
Tactic: rw [← Set.range_eq_univ, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, ← AlgHom.coe_range,
    ← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOf_mem, hs]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
inst : CommSemiring R
A : Type u_1
inst_1 : CommSemiring A
inst_2 : Algebra R A
t : Set A
h : t.Finite
⊢ FiniteType.{uR, u_1} R ↥(adjoin R t)
have rw : Subalgebra.FG (adjoin R t)
Tactic: rw [← Subalgebra.fg_iff_finiteType]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ FiniteType (algebraMap A B) ↔ Algebra.FiniteType A B
have rw : Algebra.FiniteType A B ↔ Algebra.FiniteType A B
Tactic: rw [FiniteType, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : Algebra.FiniteType A B ↔ Algebra.FiniteType A B
⊢ FiniteType (algebraMap A B) ↔ Algebra.FiniteType A B
have rw₁ : Algebra.FiniteType A B ↔ Algebra.FiniteType A B
Tactic: rw [FiniteType, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ f.FiniteType
have rw : (f.comp (RingHom.id A)).FiniteType
Tactic: rw [← f.comp_id]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
⊢ g.FiniteType
have algebraizeInst : Algebra.FiniteType A C
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
⊢ Membership.mem (γ := Subalgebra R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))) f
have suffices : LE.le (α := Submodule R R[M]) (span R (of' R M '' (↑f.support : Set M)))
  ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))))
Tactic: suffices span R (of' R M '' f.support) ≤
      Subalgebra.toSubmodule (adjoin R (of' R M '' f.support)) by
    exact this (mem_span_support f)
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
f : R[M]
⊢ LE.le (α := Submodule R R[M]) (span R (of' R M '' (↑f.support : Set M)))
    ((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M]) (adjoin R (of' R M '' (↑f.support : Set M))))
have rw : of' R M '' (↑f.support : Set M) ⊆
  (↑((Subalgebra.toSubmodule : (a : Subalgebra R R[M]) → Submodule R R[M])
          (adjoin R (of' R M '' (↑f.support : Set M))) :
        Submodule R R[M]) :
    Set R[M])
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤
have refine : LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M)))
Tactic: refine le_antisymm le_top ?_
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ LE.le (α := Subalgebra R R[M]) ⊤ (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M)))
have rw : S ⊆ (↑(adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) : Set R[M])
Tactic: rw [← hS, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ (↑(adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) : Set R[M])
have hincl : Subset (α := Set R[M]) (of' R M '' (↑f.support : Set M)) (⋃ g ∈ S, of' R M '' (↑g.support : Set M))
Tactic: have hincl :
    of' R M '' f.support ⊆ ⋃ (g : R[M]) (_ : g ∈ S), of' R M '' g.support := by
    intro s hs
    exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
this : Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤
have rw : Eq (α := Subalgebra R R[M]) (adjoin R (⋃ f ∈ S, of' R M '' (↑f.support : Set M))) ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddMonoid M
S : Set R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R S) ⊤
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤
have suffices : Eq (α := Set R[M]) (of' R M '' ⋃ f ∈ S, (↑f.support : Set M)) (⋃ f ∈ S, of' R M '' (↑f.support : Set M))
Tactic: suffices (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of' R M '' (f.support : Set M) by
    rw [this]
    exact support_gen_of_gen hS
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
h : FiniteType R R[M]
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑G : Set M))) ⊤
have obtain : ∀ (S : Finset R[M]) (hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤),
  ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑G : Set M))) ⊤
Tactic: obtain ⟨S, hS⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ (G : Finset M), Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑G : Set M))) ⊤
have h : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
Tactic: use Finset.biUnion S fun f => f.support
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this : DecidableEq M := Classical.decEq M
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
have this₁ : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
Tactic: have : (Finset.biUnion S fun f => f.support : Set M) = ⋃ f ∈ S, (f.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddMonoid M
S : Finset R[M]
hS : Eq (α := Subalgebra R R[M]) (adjoin R (↑S : Set R[M])) ⊤
this_1 : DecidableEq M := Classical.decEq M
this : (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M) = ⋃ f ∈ S, (↑f.support : Set M)
⊢ Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' (↑(S.biUnion fun (f : R[M]) ↦ f.support) : Set M))) ⊤
have h : Eq (α := Subalgebra R R[M]) (adjoin R (of' R M '' ⋃ f ∈ S, (↑f.support : Set M))) ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])
have this : Membership.mem (γ := AddSubmonoid M) (closure S) m
Tactic: have : m ∈ closure S := hS.symm ▸ mem_top _
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := AddSubmonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := AddSubmonoid M) (closure S) m
⊢ ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])
have hM : ∀ (m : M) (hm : m ∈ S),
  ∃ (a : MvPolynomial.{u_2, u_1} (↑S : Type u_2) R),
    Eq (α := R[M])
      (((MvPolynomial.aeval (R := R) (S₁ := R[M]) fun (s : (↑S : Type u_2)) ↦ of' R M (↑s : M) :
              MvPolynomial.{u_2, u_1} (↑S : Type u_2) R →ₐ[R] R[M]) :
            (a : MvPolynomial (↑S : Type u_2) R) → R[M])
          a :
        R[M])
      ((of R M : (a : Multiplicative M) → R[M]) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m) : R[M])
Tactic: refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this