-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
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)
ha :
  ∀ (x_1 : ↥B'),
    Eq (α := A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
      ((AlgHom.comp (AlgHom.restrictScalars K (ψ.comp Algebra.TensorProduct.includeLeft))
              Algebra.TensorProduct.includeRight :
            (a : ↥B') → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
          x_1 :
        A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
      ((AlgHom.comp (B := TensorProduct.{u_3, u_4, u_5} K A ↥B')
              (AlgHom.restrictScalars K
                (AlgHom.comp
                  (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)))
                  Algebra.TensorProduct.includeLeft))
              Algebra.TensorProduct.includeRight :
            (a : ↥B') → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
          x_1 :
        A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
⊢ ψ =
    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:
ext