-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (hypothesis)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
x : PrimeSpectrum A
ψ : TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    AlgHom.comp
      (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B)) :
        x.asIdeal.ResidueField ⊗[A] (A ⊗[K] B) →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
      (AlgHom.comp (B := TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField B)
        ((↑(AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B)) :
            TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField B →ₐ[A] x.asIdeal.ResidueField ⊗[A] (A ⊗[K] B)) :
          TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField B →ₐ[A] x.asIdeal.ResidueField ⊗[A] (A ⊗[K] B))
        (AlgHom.comp (B := TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField ↥B')
            (Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val :
              TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField ↥B' →ₐ[A]
                TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField B)
            (AlgHom.comp
                ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B') :
                    x.asIdeal.ResidueField ⊗[A] TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A]
                      TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField ↥B') :
                  x.asIdeal.ResidueField ⊗[A] TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A]
                    TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField ↥B')
                ((↑(Algebra.TensorProduct.comm A (TensorProduct.{u_3, u_4, u_5} K A ↥B') x.asIdeal.ResidueField) :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A]
                      x.asIdeal.ResidueField ⊗[A] TensorProduct.{u_3, u_4, u_5} K A ↥B') :
                  TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A]
                    x.asIdeal.ResidueField ⊗[A] TensorProduct.{u_3, u_4, u_5} K A ↥B') :
              TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A]
                TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField ↥B') :
          TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A]
            TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField B))
⊢ IsNilpotent (R := A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
      ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField) :
            (a : A ⊗[K] B) → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
          ((AlgHom.toRingHom
                (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                  TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
              (a : A ⊗[K] ↥B') → A ⊗[K] B)
            f) :
        A ⊗[K] B ⊗[A] x.asIdeal.ResidueField) ↔
    IsNilpotent (R := TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField)
      ((algebraMap (TensorProduct.{u_3, u_4, u_5} K A ↥B')
              (TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField) :
            (a : A ⊗[K] ↥B') → A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)
          f :
        TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField)
have hψ : Injective (α := TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField) (β :=
  A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
  (⇑ψ : (a : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField) → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
Tactic: have hψ : Function.Injective ψ := by
    rw [hψeq]
    dsimp
    simp_rw [EmbeddingLike.comp_injective, ← Function.comp_assoc, EquivLike.injective_comp]
    exact Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective