-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst : Algebra P.Ring (Generators.Ring (comp (localizationAway T g) P)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Hom.toAlgHom (toComp (localizationAway T g) P)))
f : P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2 :=
  (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)
π : Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
  Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((lift
            ((↑S :
                {S_1 M : Type u_3} →
                  {M₂ : Type (max u_1 u_4)} →
                    [inst : Semiring S] →
                      [inst_8 : Semiring S_1] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [inst_13 : Module S_1 M] →
                                  [inst_14 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (S := T)
              (((↑(LinearEquiv.symm
                        (LinearMap.ringLmapEquivSelf T T
                          (P.toExtension.Cotangent →ₗ[S] Extension.Cotangent (toExtension (Q.comp P))))) :
                    (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →ₗ[T]
                      T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) :
                  (a : P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →
                    T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)
                (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))) :
          (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
        (((TensorProduct.mk S T P.toExtension.Cotangent :
                (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
              1 :
            (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x)) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (0 : Extension.Cotangent (toExtension (Q.comp P)))
suffices :
  Eq (α := Localization.Away f)
    ((algebraMap P.Ring (Localization.Away f) : (a : P.Ring) → Localization.Away f) (↑x : P.toExtension.Ring) :
      Localization.Away f)
    (0 : Localization.Away f)
⊢ Eq (α := T ⊗[S] P.toExtension.Cotangent)
    (((TensorProduct.mk S T P.toExtension.Cotangent :
              (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
            1 :
          (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x) :
      T ⊗[S] P.toExtension.Cotangent)
    (0 : T ⊗[S] P.toExtension.Cotangent)

Tactic:
suffices h : algebraMap P.Ring (Localization.Away f) x.val = 0 by
    rw [IsScalarTower.algebraMap_apply _ (P.Ring ⧸ P.ker ^ 2) _,
      IsLocalization.map_eq_zero_iff (Submonoid.powers f) (Localization.Away f)] at h
    obtain ⟨⟨m, ⟨n, rfl⟩⟩, hm⟩ := h
    rw [IsLocalizedModule.eq_zero_iff (Submonoid.powers g)]
    use ⟨g ^ n, n, rfl⟩
    dsimp [f] at hm
    rw [← map_pow, ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at hm
    simp only [Submonoid.smul_def]
    rw [show g = algebraMap P.Ring S (P.σ g) by simp, ← map_pow, algebraMap_smul, ← map_smul,
      Extension.Cotangent.mk_eq_zero_iff]
    simpa using hm