-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
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))
⊢ Injective (α := TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField) (β :=
    A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
    (Function.comp (β := x.asIdeal.ResidueField ⊗[A] (A ⊗[K] B))
      (⇑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B)) :
        (a : x.asIdeal.ResidueField ⊗[A] (A ⊗[K] B)) → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
      (Function.comp (β := 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)) :
          (a : x.asIdeal.ResidueField ⊗[K] B) → x.asIdeal.ResidueField ⊗[A] (A ⊗[K] B))
        (Function.comp (β := 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) :
            (a : x.asIdeal.ResidueField ⊗[K] ↥B') → x.asIdeal.ResidueField ⊗[K] B)
          (Function.comp (β := x.asIdeal.ResidueField ⊗[A] TensorProduct.{u_3, u_4, u_5} K A ↥B')
            (⇑(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') :
              (a : x.asIdeal.ResidueField ⊗[A] (A ⊗[K] ↥B')) → x.asIdeal.ResidueField ⊗[K] ↥B')
            (⇑(Algebra.TensorProduct.comm A (TensorProduct.{u_3, u_4, u_5} K A ↥B') x.asIdeal.ResidueField) :
              (a : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField) → x.asIdeal.ResidueField ⊗[A] (A ⊗[K] ↥B'))))))
have simp_rw : Injective (α := TensorProduct.{u_3, u_4, u_5} K x.asIdeal.ResidueField ↥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) :
    (a : x.asIdeal.ResidueField ⊗[K] ↥B') → x.asIdeal.ResidueField ⊗[K] B)
Tactic: simp_rw [EmbeddingLike.comp_injective, ← Function.comp_assoc, EquivLike.injective_comp]