-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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
pos :
  ∀
    (ht :
      Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
        (0 : P.ResidueField)),
    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))
neg :
  ∀
    (ht :
      ¬Eq (α := P.ResidueField) ((algebraMap S P.ResidueField : (a : S) → P.ResidueField) (↑t : S) : P.ResidueField)
          (0 : P.ResidueField)),
    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))
⊢ 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))

Tactic:
by_cases ht : algebraMap _ P.ResidueField t.1 = 0

Premises used: Algebra.algebraMap, Ideal.ResidueField, Subtype.val, DFunLike.coe