-- 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)
⊢ 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ψ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))
Tactic: have hψeq : ψ = (Algebra.TensorProduct.comm _ _ _ |>.toAlgHom.comp <|
    Algebra.TensorProduct.cancelBaseChange K A A _ B |>.symm.toAlgHom.comp <|
    Algebra.TensorProduct.map (.id _ _) B'.val |>.comp <|
    Algebra.TensorProduct.cancelBaseChange K A A _ B' |>.toAlgHom.comp <|
    (Algebra.TensorProduct.comm _ _ _).toAlgHom) := by ext; simp [ψ]