-- 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_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)
⊢ ∃ (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
have 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 sorry) :
                      (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 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)
                ((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 sorry) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])
Tactic: obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
Cleared hypotheses: y, hy_1, hy, h, this