-- 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_1 : Membership.mem (γ := Subalgebra K S) K[x] y
hy : Membership.mem (γ := Subalgebra K S) (AlgHom.range (aeval 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_1)
this :
  ∀
    (hy :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy_1 =
          (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_1)
hsp :
  ∀ (f : K[X]) (hy : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S))
    (hy_2 : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)),
    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 :
          ↥K[x]) →
      ∀
        (this :
          ∀
            (hy_3 :
              ∃ (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 :
                    ↥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 :
                ↥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 :
              ↥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])
⊢ ∃ (f : K[X]),
    Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy_1 =
      (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) : (a : K[X]) → ↥K[x])
        f

Tactic:
obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy

Premises used: AlgHom.mem_range, Iff.mp, Polynomial.aeval, rfl