awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Bivariate (goal)
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 : R[X][Y]
⊢ 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)
have add : ∀ (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 sorry)) :
                  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 sorry)) :
                  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 sorry)) :
                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: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp_all [map_add]
  | monomial n a =>
    simp_all [aeval_algebraMap_apply, Transcendental.algEquivAdjoin, Subalgebra.algebraMap_def]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Polynomial.Bivariate (goal)
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)
⊢ IsAlgebraic.{u_3, u_3} ↥R[y] (A := B) ((algebraMap A B : (a : A) → B) x : B)
have 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)
Tactic: refine ⟨hy.algEquivAdjoin (swap (hx.algEquivAdjoin.symm f)),
    by simpa only [map_ne_zero_iff _ (AlgEquiv.injective _)], ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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
⊢ Basis.{0, u_1, u_2} (Fin (natDegree (minpoly K x))) K ↥K[x]
have hST : 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
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 ⋯)
have 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 sorry) :
    S)
Tactic: apply (isIntegral_algebraMap_iff hST).mp
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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)
⊢ Basis.{0, u_1, u_2} (Fin (natDegree (minpoly K x))) K ↥K[x]
have hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry)
Tactic: have hx' :
    IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : K[(x : S)]) := by
    apply (isIntegral_algebraMap_iff hST).mp
    convert! hx
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 ⋯)
⊢ Basis.{0, u_1, u_2} (Fin (natDegree (minpoly K x))) K ↥K[x]
have 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 sorry) (↑i : ℕ)
Tactic: apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 : ℕ)
⊢ Basis.{0, u_1, u_2} (Fin (natDegree (minpoly K x))) K ↥K[x]
have 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 sorry)
        (↑i : ℕ)))
Tactic: apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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 x))) ↦
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)
have 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 sorry)))) ↦
  HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry) (↑i : ℕ)
Tactic: have : LinearIndependent K _ := linearIndependent_pow
      (⟨x, self_mem_adjoin_singleton _ _⟩ : K[x])
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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 sorry) :
                  S)))) ↦
      HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry)
        (↑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 sorry)
      (↑i : ℕ)
Tactic: rwa [← minpoly.algebraMap_eq hST] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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)
⊢ 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)
have 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 sorry) :
            (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 sorry)))) ↦
        HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry)
          (↑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⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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)
⊢ 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)
have 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 sorry) :
            (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 sorry) :
                    S)))) ↦
        HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry)
          (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 (γ := 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)
have 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 sorry) : (a : K[X]) → ↥K[x]) f
Tactic: apply this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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)
⊢ ∃ (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
have hy₁ : Membership.mem (γ := Subalgebra K S) (AlgHom.range (aeval x)) y
Tactic: rw [adjoin_singleton_eq_range_aeval] at hy
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 ⋯)
f : K[X]
hy_1 : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S)
hy : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)
h :
  Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
this :
  ∀
    (hy :
      ∃ (f_1 : K[X]),
        Eq.{u_2 + 1} (α := ↥K[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1)
              ((aeval x : (a : K[X]) → S) f) hy_1 :
            ↥K[x])
          ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])),
    Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := 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) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
⊢ ∃ (f_1 : K[X]),
    Eq.{u_2 + 1} (α := ↥K[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
      ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
            (a : K[X]) → ↥K[x])
          f_1 :
        ↥K[x])
have h : Eq.{u_2 + 1} (α := ↥K[x])
  (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f) hy_1 :
    ↥K[x])
  ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry) : (a : K[X]) → ↥K[x])
      f :
    ↥K[x])
Tactic: use f
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 ⋯)
f : K[X]
hy_1 : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S)
hy : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)
h :
  Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
this :
  ∀
    (hy :
      ∃ (f_1 : K[X]),
        Eq.{u_2 + 1} (α := ↥K[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1)
              ((aeval x : (a : K[X]) → S) f) hy_1 :
            ↥K[x])
          ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])),
    Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := 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) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
⊢ Eq.{u_2 + 1} (α := ↥K[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
    ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) : (a : K[X]) → ↥K[x])
        f :
      ↥K[x])
have h : Eq.{u_2 + 1} (α := S)
  ((↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1) :
      S) :
    S)
  ((↑((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry) : (a : K[X]) → ↥K[x])
          f) :
      S) :
    S)
Tactic: ext