awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 q_1 : R[X]
x : A
x_1 x_2 : ↥R[x]
q : A
hq : Membership.mem (γ := Subalgebra R A) R[x] q
p' : R[X]
hp : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p' : A)
obtain :
  ∀ (q' : R[X])
    (hq : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q' : A)),
    HMul.hMul (α := ↥R[x]) (β := ↥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)
            ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q') hq :
          ↥R[x]) =
      HMul.hMul (α := ↥R[x]) (β := ↥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) q') hq :
          ↥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])
⊢ 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])

Tactic:
obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq

Premises used: rfl
-- 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 q : R[X]
x : A
x_1 x_2 : ↥R[x]
p' : R[X]
hp : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) p' : A)
q' : R[X]
hq : Membership.mem (α := A) (γ := Subalgebra R A) R[x] ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q' : A)
⊢ HMul.hMul (α := ↥R[x]) (β := ↥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)
          ((AlgHom.toRingHom (aeval x) : (a : R[X]) → A) q') hq :
        ↥R[x]) =
    HMul.hMul (α := ↥R[x]) (β := ↥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) q') hq :
        ↥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])

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MulMemClass.mk_mul_mk, ← map_mul,
        mul_comm p' q']

Premises used: RingHom.coe_coe, map_mul, AlgHom.toRingHom_eq_coe, mul_comm, MulMemClass.mk_mul_mk
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
hx : Transcendental R x
p : R[X][Y]
⊢ Eq.{u_2 + 1} (α := (↥R[x])[X]) ((algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) p : (↥R[x])[X])
    ((mapAlgHom (aeval (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_1) x ⋯)) :
          (a : R[X][Y]) → (↥R[x])[X])
        p :
      (↥R[x])[X])

Tactic:
rfl

Premises used: Polynomial.eval₂RingHom', Polynomial.map, rfl
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
hx : Transcendental R x
p : R[X][Y]
⊢ Eq.{u_2 + 1} (α := (↥R[x])[X])
    ((algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) ((swap : (a : R[X][Y]) → R[X][Y]) p) : (↥R[x])[X])
    (((aeval
              ((C : (a : ↥R[x]) → (↥R[x])[X])
                (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) R[x] x_1) x ⋯)) :
            AlgHom.{u_1, u_1, u_2} R[X] R[X][Y] (↥R[x])[X]) :
          (a : R[X][Y]) → (↥R[x])[X])
        p :
      (↥R[x])[X])

Tactic:
simp [algEquivAdjoin, Bivariate.aveal_eq_map_swap]

Premises used: Polynomial.Bivariate.aveal_eq_map_swap, Polynomial.Bivariate.Transcendental.algEquivAdjoin
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
p q : R[X][Y]
hp :
  Eq.{u_3 + 1} (α := B)
    (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
        (((aeval
                  ((C : (a : ↥R[y]) → (↥R[y])[X])
                    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
              (a : R[X][Y]) → (↥R[y])[X])
            p :
          (↥R[y])[X]) :
      B)
    ((aeval y : (a : (↥R[x])[X]) → B) ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) p : (↥R[x])[X]) :
      B)
hq :
  Eq.{u_3 + 1} (α := B)
    (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
        (((aeval
                  ((C : (a : ↥R[y]) → (↥R[y])[X])
                    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
              (a : R[X][Y]) → (↥R[y])[X])
            q :
          (↥R[y])[X]) :
      B)
    ((aeval y : (a : (↥R[x])[X]) → B) ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) q : (↥R[x])[X]) :
      B)
⊢ Eq.{u_3 + 1} (α := B)
    (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
        (((aeval
                  ((C : (a : ↥R[y]) → (↥R[y])[X])
                    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
              (a : R[X][Y]) → (↥R[y])[X])
            (p + q) :
          (↥R[y])[X]) :
      B)
    ((aeval y : (a : (↥R[x])[X]) → B)
        ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) (p + q) : (↥R[x])[X]) :
      B)

Tactic:
simp_all [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
n : ℕ
a : R[X]
⊢ Eq.{u_3 + 1} (α := B)
    (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
        (((aeval
                  ((C : (a : ↥R[y]) → (↥R[y])[X])
                    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) R[y] x) y ⋯)) :
                AlgHom.{u_1, u_1, u_3} R[X] R[X][Y] (↥R[y])[X]) :
              (a : R[X][Y]) → (↥R[y])[X])
            ((monomial n : (a : R[X]) → R[X][Y]) a) :
          (↥R[y])[X]) :
      B)
    ((aeval y : (a : (↥R[x])[X]) → B)
        ((Transcendental.algEquivAdjoin hx : (a : R[X][Y]) → (↥R[x])[X]) ((monomial n : (a : R[X]) → R[X][Y]) a) :
          (↥R[x])[X]) :
      B)

Tactic:
simp_all [aeval_algebraMap_apply, Transcendental.algEquivAdjoin, Subalgebra.algebraMap_def]

Premises used: Polynomial.Bivariate.Transcendental.algEquivAdjoin, Subalgebra.algebraMap_def, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
hy : Transcendental R y
f : (↥R[x])[X]
hnezero : f ≠ 0
halg : Eq.{u_3 + 1} (α := B) ((aeval y : (a : (↥R[x])[X]) → B) f : B) (0 : B)
⊢ Ne.{u_3 + 1} (α := (↥R[y])[X])
    ((Transcendental.algEquivAdjoin hy : (a : R[X][Y]) → (↥R[y])[X])
        ((swap : (a : R[X][Y]) → R[X][Y]) (((Transcendental.algEquivAdjoin hx).symm : (a : (↥R[x])[X]) → R[X][Y]) f)) :
      (↥R[y])[X])
    (0 : (↥R[y])[X])

Tactic:
simpa only [map_ne_zero_iff _ (AlgEquiv.injective _)]

Premises used: AlgEquiv.injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
hy : Transcendental R y
f : (↥R[x])[X]
hnezero : f ≠ 0
halg : Eq.{u_3 + 1} (α := B) ((aeval y : (a : (↥R[x])[X]) → B) f : B) (0 : B)
refine :
  Eq.{u_3 + 1} (α := B)
    (((aeval ((algebraMap A B : (a : A) → B) x) : (↥R[y])[X] →ₐ[↥R[y]] B) : (a : (↥R[y])[X]) → B)
        ((Transcendental.algEquivAdjoin hy : (a : R[X][Y]) → (↥R[y])[X])
            ((swap : (a : R[X][Y]) → R[X][Y])
              (((Transcendental.algEquivAdjoin hx).symm : (a : (↥R[x])[X]) → R[X][Y]) f)) :
          (↥R[y])[X]) :
      B)
    (0 : B)
⊢ IsAlgebraic.{u_3, u_3} ↥R[y] (A := B) ((algebraMap A B : (a : A) → B) x : B)

Tactic:
refine ⟨hy.algEquivAdjoin (swap (hx.algEquivAdjoin.symm f)),
    by simpa only [map_ne_zero_iff _ (AlgEquiv.injective _)], ?_⟩
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
⊢ Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)

Tactic:
have hST : Function.Injective (algebraMap (K[(x : S)]) S) := Subtype.coe_injective
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
apply :
  IsIntegral K (A := S)
    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
      S)
⊢ IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)

Tactic:
apply (isIntegral_algebraMap_iff hST).mp

Premises used: isIntegral_algebraMap_iff, Iff.mp
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
⊢ IsIntegral K x

Tactic:
hx
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
⊢ IsIntegral K (A := S)
    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
      S)

Tactic:
convert! hx
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
⊢ IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)

Tactic:
have hx' :
    IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : K[(x : S)]) := by
    apply (isIntegral_algebraMap_iff hST).mp
    convert! hx
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
hli :
  LinearIndependent.{0, u_1, u_2} K (M := ↥K[x]) fun (i : Fin (natDegree (minpoly K x))) ↦
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)
hsp :
  LE.le.{u_2} (α := Submodule K ↥K[x]) ⊤
    (Submodule.span K
      (Set.range fun (i : Fin (natDegree (minpoly K x))) ↦
        HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
          (↑i : ℕ)))
⊢ Basis.{0, u_1, u_2} (Fin (natDegree (minpoly K x))) K ↥K[x]

Tactic:
apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))

Premises used: Module.Basis.mk
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
⊢ LinearIndependent.{0, u_1, u_2} K (M := ↥K[x])
    fun
      (i :
        Fin
          (natDegree
            (minpoly K (B := ↥K[x])
              (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)))) ↦
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)

Tactic:
have : LinearIndependent K _ := linearIndependent_pow
      (⟨x, self_mem_adjoin_singleton _ _⟩ : K[x])
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
this :
  LinearIndependent.{0, u_1, u_2} K (M := ↥K[x])
    fun
      (i :
        Fin
          (natDegree
            (minpoly K (B := ↥K[x])
              (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)))) ↦
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)
hli hli₁ hli₂ hli₃ :
  ∀
    (this :
      LinearIndependent.{0, u_1, u_2} K (M := ↥K[x])
        fun
          (i :
            Fin
              (natDegree
                (minpoly K (B := S)
                  ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                    S)))) ↦
        HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
          (↑i : ℕ)),
    LinearIndependent.{0, u_1, u_2} K (M := ↥K[x]) fun (i : Fin (natDegree (minpoly K x))) ↦
      HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
        (↑i : ℕ)
⊢ LinearIndependent.{0, u_1, u_2} K (M := ↥K[x]) fun (i : Fin (natDegree (minpoly K x))) ↦
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)

Tactic:
rwa [← minpoly.algebraMap_eq hST] at this

Premises used: minpoly.algebraMap_eq
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
y : S
hy : Membership.mem (γ := Subalgebra K S) K[x] y
h :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
⊢ ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := ↥K[x])
                    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)

Tactic:
have := hx'.mem_span_pow (y := ⟨y, hy⟩)
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
y : S
hy : Membership.mem (γ := Subalgebra K S) K[x] y
h :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
this :
  ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := ↥K[x])
                    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
⊢ ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)

Tactic:
rw [← minpoly.algebraMap_eq hST] at this

Premises used: minpoly.algebraMap_eq
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
y : S
hy : Membership.mem (γ := Subalgebra K S) K[x] y
h :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
this :
  ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
hsp :
  ∃ (f : K[X]),
    Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
      (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) : (a : K[X]) → ↥K[x])
        f
⊢ Membership.mem (γ := Submodule K ↥K[x])
    (Submodule.span K
      (Set.range fun (i : Fin (natDegree (minpoly K x))) ↦
        HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
          (↑i : ℕ)))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)

Tactic:
apply this
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
y : S
hy : Membership.mem (γ := Subalgebra K S) K[x] y
h :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
this :
  ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
⊢ Membership.mem (γ := Subalgebra K S) (AlgHom.range (aeval x)) y

Tactic:
rw [adjoin_singleton_eq_range_aeval] at hy

Premises used: Algebra.adjoin_singleton_eq_range_aeval