-- 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 ι
rw :
  HMul.hMul (α :=
        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))
        (β :=
        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))
        ((algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
                (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)) :
              (a : P.Ring ⧸ P.ker ^ 2) →
                Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
            ((algebraMap P.Ring (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)) :
          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))
        (IsLocalization.Away.invSelf (R := 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) :
          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)) -
      1 =
    0
⊢ HMul.hMul (α :=
        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))
        (β :=
        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 :
              (a : ((localizationAway T g).comp P).Ring) →
                Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
            ((Hom.toAlgHom (toComp (localizationAway T g) P) : (a : P.Ring) → ((localizationAway T g).comp P).Ring)
              (P.σ g)) :
          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 :
              (a : ((localizationAway T g).comp P).Ring) →
                Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
            (X (Sum.inl ())) :
          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)) -
      1 =
    0

Tactic:
rw [compLocalizationAwayAlgHom_toAlgHom_toComp, compLocalizationAwayAlgHom_X_inl,
    IsScalarTower.algebraMap_apply P.Ring (P.Ring ⧸ P.ker ^ 2) (Localization.Away _)]

Premises used: Algebra.Generators.ker, Algebra.Generators.Ring, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, Localization.Away, HasQuotient.Quotient, HPow.hPow, OfNat.ofNat, IsScalarTower.algebraMap_apply