-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
M : Submonoid S
inst_7 : IsLocalization M T
inst_8 : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht :
  ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
      (0 : P.ResidueField)
trans :
  Eq (α := P.ResidueField ⊗[S] T)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
    ((s • p) ⊗ₜ[S] 1)
⊢ Eq (α := P.ResidueField ⊗[S] T)
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (((↑S :
              {S_1 M : Type u_2} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_9 : Semiring S_1] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [inst_14 : Module S_1 M] →
                                [inst_15 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Algebra.linearMap P.ResidueField (P.Fiber T)) :
          (a : P.ResidueField) → P.Fiber T)
        (HDiv.hDiv (β := P.ResidueField) (s • p)
          ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField))))
    ((fun (x : P.ResidueField ⊗[S] T) ↦
        HMul.hMul (β := P.ResidueField ⊗[S] T) x
          ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
            P.ResidueField ⊗[S] T))
      (p ⊗ₜ[S] IsLocalization.mk' T s t))
have trans₁ : Eq (α := P.ResidueField ⊗[S] T) ((s • p) ⊗ₜ[S] 1)
  ((fun (x : P.ResidueField ⊗[S] T) ↦
      HMul.hMul (β := P.ResidueField ⊗[S] T) x
        ((TensorProduct.includeRight : (a : T) → P.ResidueField ⊗[S] T) ((algebraMap S T : (a : S) → T) (↑t : S)) :
          P.ResidueField ⊗[S] T))
    (p ⊗ₜ[S] IsLocalization.mk' T s t))
Tactic: trans (s • p) ⊗ₜ[S] 1