awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
y : L
hy : eval₂ (R := ↥Ks) (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)

Tactic:
⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩

Premises used: Membership.mem, Subalgebra.ofRestrictScalars, Subtype, Algebra.adjoin.liftSingleton, Nonempty.intro
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
y : L
hy : eval₂ (R := ↥Ks) (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)

Tactic:
exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra R K
x : L
inst_4 : Algebra R L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R K) (minpoly R x))
f : K →ₐ[R] L
rw :
  Ne (α := L[X]) (Polynomial.map (algebraMap R L) (minpoly R x)) 0 ∧
    Eq.{u_3 + 1} (α := L) ((aeval x : (a : R[X]) → L) (minpoly R x) : L) (0 : L)
⊢ Membership.mem (γ := Set L) ((⇑f : (a : K) → L) '' rootSet (minpoly R x) K) x

Tactic:
rw [h.image_rootSet, mem_rootSet']

Premises used: Polynomial.Splits.image_rootSet, Polynomial.mem_rootSet'
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra R K
x : L
inst_4 : Algebra R L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R K) (minpoly R x))
f : K →ₐ[R] L
⊢ Ne (α := L[X]) (Polynomial.map (algebraMap R L) (minpoly R x)) 0 ∧
    Eq.{u_3 + 1} (α := L) ((aeval x : (a : R[X]) → L) (minpoly R x) : L) (0 : L)

Tactic:
⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩

Premises used: minpoly.monic, minpoly.aeval, And.intro, Polynomial.Monic.map, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra R K
x : L
inst_4 : Algebra R L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R K) (minpoly R x))
f : K →ₐ[R] L
⊢ Ne (α := L[X]) (Polynomial.map (algebraMap R L) (minpoly R x)) 0 ∧
    Eq.{u_3 + 1} (α := L) ((aeval x : (a : R[X]) → L) (minpoly R x) : L) (0 : L)

Tactic:
exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra R K
x : L
inst_4 : Algebra R L
inst_5 : Algebra K L
inst_6 : IsScalarTower R K L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R K) (minpoly R x))
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) x

Tactic:
int.mem_range_algHom_of_minpoly_splits h (IsScalarTower.toAlgHom R K L)

Premises used: Set.Mem, IsScalarTower.toAlgHom, IsIntegral.mem_range_algHom_of_minpoly_splits
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
g : Splits (map (algebraMap K L) (minpoly K x))
rw :
  (HMul.hMul (α := L[X]) (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))
      (map (algebraMap K L) (comp (minpoly K x) (-X)))).Splits
⊢ Splits (map (algebraMap K L) (minpoly K (-x)))

Tactic:
rw [minpoly.neg, Polynomial.map_mul]

Premises used: Polynomial.map_mul, minpoly.neg
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (comp (minpoly K x) (-X)))

Tactic:
simpa [map_comp] using g.comp_neg_X

Premises used: Polynomial.map_comp, Polynomial.Splits.comp_neg_X
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
g : Splits (map (algebraMap K L) (minpoly K x))
apply : Splits (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))
⊢ (HMul.hMul (α := L[X]) (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))
      (map (algebraMap K L) (comp (minpoly K x) (-X)))).Splits

Tactic:
apply Splits.mul _ (by simpa [map_comp] using g.comp_neg_X)

Premises used: Polynomial.Splits.mul
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (HPow.hPow (α := K[X]) (-1) (natDegree (minpoly K x))))

Tactic:
simpa only [map_pow, map_neg, map_one] using
    (map_C (algebraMap K L) ▸ Splits.C (algebraMap K L <| (-1) ^ _) :)

Premises used: map_neg, map_pow, map_one
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
r : K
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (minpoly K (HAdd.hAdd (β := L) x ((algebraMap K L : (a : K) → L) r : L))))

Tactic:
simpa [minpoly.add_algebraMap, map_comp] using g.comp_X_sub_C (algebraMap K L r)

Premises used: Algebra.algebraMap, Polynomial.Splits.comp_X_sub_C, minpoly.add_algebraMap, Polynomial.map_comp, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
r : K
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (minpoly K (HSub.hSub (β := L) x ((algebraMap K L : (a : K) → L) r : L))))

Tactic:
simpa only [sub_eq_add_neg, map_neg] using minpoly_add_algebraMap_splits (-r) g

Premises used: sub_eq_add_neg, map_neg, minpoly_add_algebraMap_splits, Neg.neg
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
r : K
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (minpoly K (HAdd.hAdd (α := L) ((algebraMap K L : (a : K) → L) r : L) x)))

Tactic:
simpa only [add_comm] using minpoly_add_algebraMap_splits r g

Premises used: add_comm, minpoly_add_algebraMap_splits
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
r : K
g : Splits (map (algebraMap K L) (minpoly K x))
⊢ Splits (map (algebraMap K L) (minpoly K (HSub.hSub (α := L) ((algebraMap K L : (a : K) → L) r : L) x)))

Tactic:
simpa only [neg_sub] using minpoly_neg_splits (minpoly_sub_algebraMap_splits r g)

Premises used: minpoly_sub_algebraMap_splits, neg_sub, minpoly_neg_splits
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
rw : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap R K) (minpoly R x))
⊢ Polynomial.map f (minpoly K x) ∣ Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)

Tactic:
rw [← map_map, map_dvd_map']

Premises used: Polynomial.map_map, Polynomial.map_dvd_map'
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap R K) (minpoly R x))

Tactic:
minpoly.dvd_map_of_isScalarTower R K x

Premises used: minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap R K) (minpoly R x))

Tactic:
exact minpoly.dvd_map_of_isScalarTower R K x

Premises used: minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R K L
int : IsIntegral R x
h : Splits (Polynomial.map (algebraMap R L) (minpoly R x))
⊢ Splits
    (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
      (minpoly R x))

Tactic:
rw [IsScalarTower.algebraMap_eq R K L] at h

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R K L
int : IsIntegral R x
h :
  Splits
    (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
      (minpoly R x))
⊢ Splits (Polynomial.map (algebraMap K L) (minpoly K x))

Tactic:
int.minpoly_splits_tower_top' h

Premises used: IsIntegral.minpoly_splits_tower_top'
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : CommRing M
inst_4 : Algebra R K
inst_5 : Algebra R M
inst_6 : Algebra K M
inst_7 : IsScalarTower R K M
x : M
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R K L
int : IsIntegral R x
h :
  Splits
    (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
      (minpoly R x))
⊢ Splits (Polynomial.map (algebraMap K L) (minpoly K x))

Tactic:
exact int.minpoly_splits_tower_top' h

Premises used: IsIntegral.minpoly_splits_tower_top'
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_5
E : Type u_6
K : Type u_7
inst : CommSemiring F
inst_1 : StrongRankCondition F
inst_2 : CommSemiring E
inst_3 : StrongRankCondition E
inst_4 : Semiring K
inst_5 : SMul F E
inst_6 : Algebra E K
inst_7 : Algebra F K
inst_8 : IsScalarTower F E K
L : Subalgebra F K
inst_9 : Module.Free.{u_5, u_7} F ↥L
rw :
  Module.rank E
      ↥(Submodule.span E
          (Set.range fun (i : Module.Free.ChooseBasisIndex F ↥L) ↦
            (↑((Module.Free.chooseBasis F ↥L : (a : Module.Free.ChooseBasisIndex F ↥L) → ↥L) i) : K))) ≤
    Cardinal.mk (Module.Free.ChooseBasisIndex F ↥L)
⊢ Module.rank E ↥(Algebra.adjoin E (↑L : Set K)) ≤ Module.rank F ↥L

Tactic:
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
    L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]

Premises used: Membership.mem, Subtype, Subalgebra.adjoin_eq_span_basis, Module.Free.rank_eq_card_chooseBasisIndex, Subalgebra.rank_toSubmodule, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_5
E : Type u_6
K : Type u_7
inst : CommSemiring F
inst_1 : StrongRankCondition F
inst_2 : CommSemiring E
inst_3 : StrongRankCondition E
inst_4 : Semiring K
inst_5 : SMul F E
inst_6 : Algebra E K
inst_7 : Algebra F K
inst_8 : IsScalarTower F E K
L : Subalgebra F K
inst_9 : Module.Free.{u_5, u_7} F ↥L
⊢ Module.rank E
      ↥(Submodule.span E
          (Set.range fun (i : Module.Free.ChooseBasisIndex F ↥L) ↦
            (↑((Module.Free.chooseBasis F ↥L : (a : Module.Free.ChooseBasisIndex F ↥L) → ↥L) i) : K))) ≤
    Cardinal.mk (Module.Free.ChooseBasisIndex F ↥L)

Tactic:
rank_span_le _ |>.trans Cardinal.mk_range_le

Premises used: Cardinal.mk_range_le, rank_span_le, LE.le.trans
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_5
E : Type u_6
K : Type u_7
inst : CommSemiring F
inst_1 : StrongRankCondition F
inst_2 : CommSemiring E
inst_3 : StrongRankCondition E
inst_4 : Semiring K
inst_5 : SMul F E
inst_6 : Algebra E K
inst_7 : Algebra F K
inst_8 : IsScalarTower F E K
L : Subalgebra F K
inst_9 : Module.Free.{u_5, u_7} F ↥L
⊢ Module.rank E
      ↥(Submodule.span E
          (Set.range fun (i : Module.Free.ChooseBasisIndex F ↥L) ↦
            (↑((Module.Free.chooseBasis F ↥L : (a : Module.Free.ChooseBasisIndex F ↥L) → ↥L) i) : K))) ≤
    Cardinal.mk (Module.Free.ChooseBasisIndex F ↥L)

Tactic:
exact rank_span_le _ |>.trans Cardinal.mk_range_le

Premises used: Cardinal.mk_range_le, rank_span_le, LE.le.trans
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := Subalgebra R R[X]) R[ X] ⊤

Tactic:
top_unique fun p _hp => ?_

Premises used: top_unique
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
refine :
  ∀ (p : R[X]) (_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p), Membership.mem (γ := Subalgebra R R[X]) R[ X] p
⊢ Eq (α := Subalgebra R R[X]) R[ X] ⊤

Tactic:
refine top_unique fun p _hp => ?_

Premises used: top_unique
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
set :
  let S : Subalgebra R R[X] := R[ X];
  p ∈ S
⊢ Membership.mem (γ := Subalgebra R R[X]) R[ X] p

Tactic:
set S := adjoin R ({X} : Set R[X])

Premises used: Algebra.adjoin, Singleton.singleton, Polynomial.X
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
S : Subalgebra R R[X] := R[ X]
rw : (p.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) ∈ S
⊢ p ∈ S

Tactic:
rw [← sum_monomial_eq p]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
S : Subalgebra R R[X] := R[ X]
simp : (p.sum fun (n : ℕ) (a : R) ↦ a • HPow.hPow (α := R[X]) X n) ∈ S
⊢ (p.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) ∈ S

Tactic:
simp only [← smul_X_eq_monomial]

Premises used: Polynomial.smul_X_eq_monomial
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
S : Subalgebra R R[X] := R[ X]
⊢ (p.sum fun (n : ℕ) (a : R) ↦ a • HPow.hPow (α := R[X]) X n) ∈ S

Tactic:
S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (subset_adjoin rfl) _) _

Premises used: Set.Mem, Polynomial.sum, Algebra.subset_adjoin, Subalgebra.sum_mem, Polynomial.coeff, Subalgebra.smul_mem, Subalgebra.pow_mem, rfl
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
_hp : Membership.mem (γ := Subalgebra R R[X]) ⊤ p
S : Subalgebra R R[X] := R[ X]
⊢ (p.sum fun (n : ℕ) (a : R) ↦ a • HPow.hPow (α := R[X]) X n) ∈ S

Tactic:
exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (subset_adjoin rfl) _) _

Premises used: Algebra.subset_adjoin, Subalgebra.sum_mem, Subalgebra.smul_mem, Subalgebra.pow_mem, rfl
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
rw : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) ⊤)
rw₁ : Eq (α := Subalgebra R A) R[x] (Subalgebra.map (aeval x) R[ X])
rw₂ : Eq (α := Subalgebra R A) R[x] (adjoin R (Set.image (α := R[X]) (⇑(aeval x) : (a : R[X]) → A) {X}))
rw₃ : Eq (α := Subalgebra R A) R[x] R[((aeval x : (a : R[X]) → A) X : A)]
rw₄ rw₅ : Eq (α := Subalgebra R A) R[x] R[x]
⊢ Eq (α := Subalgebra R A) R[x] (AlgHom.range (aeval x))

Tactic:
rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]

Premises used: Set.image_singleton, AlgHom.map_adjoin, Algebra.map_top, Polynomial.adjoin_X, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
x : A
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((aeval x : (a : R[X]) → A) p : A)

Tactic:
simp [adjoin_singleton_eq_range_aeval]

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x a : A
h : Membership.mem (γ := Subalgebra R A) R[x] a
⊢ Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) a

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval] at h

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x a : A
h : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) a
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = a

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
⊢ Membership.mem (γ := Subalgebra R A) R[x] (↑a : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
⊢ Membership.mem (γ := Subalgebra R A) R[x] (↑a : A)

Tactic:
have : (a : A) ∈ R[x] := by simp
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
this : Membership.mem (γ := Subalgebra R A) R[x] (↑a : A)
set :
  let y := (↑a : A);
  ∀ (this : Membership.mem (γ := Subalgebra R A) R[x] y) (h : y = (↑a : A)),
    ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = y
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = (↑a : A)

Tactic:
set y := (a : A) with h

Premises used: Subtype.val
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
y : A := (↑a : A)
this : Membership.mem (γ := Subalgebra R A) R[x] y
h : y = (↑a : A)
⊢ Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) y

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval] at this

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
y : A := (↑a : A)
this : Membership.mem (γ := Subalgebra R A) R[x] y
h : y = (↑a : A)
this₁ : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) y
⊢ y = (↑a : A)

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval] at this

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
a : ↥R[x]
y : A := (↑a : A)
this : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) y
h : y = (↑a : A)
⊢ ∃ (p : R[X]), (aeval x : (a : R[X]) → A) p = y

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
M : ↥R[x] → Prop
a : ↥R[x]
f :
  ∀ (p : R[X]),
    M (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_1) ((aeval x : (a : R[X]) → A) p) ⋯)
obtain : ∀ (p : R[X]) (hp : (aeval x : (a : R[X]) → A) p = (↑a : A)), M a
⊢ M a

Tactic:
obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a

Premises used: Algebra.adjoin_eq_exists_aeval
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
M : ↥R[x] → Prop
a : ↥R[x]
f :
  ∀ (p : R[X]),
    M (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_1) ((aeval x : (a : R[X]) → A) p) ⋯)
p : R[X]
hp : (aeval x : (a : R[X]) → A) p = (↑a : A)
⊢ M a

Tactic:
grind
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
p_1 q_1 : R[X]
x : A
x_1 x_2 : ↥R[x]
p : A
hp : Membership.mem (γ := Subalgebra R A) R[x] p
q : A
hq : Membership.mem (γ := Subalgebra R A) R[x] q
obtain :
  ∀ (p' : R[X])
    (hp : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p' : A)),
    HMul.hMul (α := ↥R[x])
        (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
            ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
          ↥R[x])
        (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq) =
      HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq)
        (Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3)
            ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p') hp :
          ↥R[x])
⊢ Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) p hp *
      Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq =
    Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) q hq *
      Subtype.mk (p := fun (x_3 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_3) p hp

Tactic:
obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp

Premises used: rfl