-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
e₁ :
  Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x :
          S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x) :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
      ((IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
                Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
                (Ideal.cotangentIdeal (ideal R S))) :
            (a : S) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
          x :
        HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
          Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
          (Ideal.cotangentIdeal (ideal R S)))
e :
  Eq (α :=
    HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
      Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2)) (Ideal.cotangentIdeal (ideal R S)))
    ((AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.cotangentIdeal (ideal R S))) f :
          (a : S) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
        x :
      HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
        Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2)) (Ideal.cotangentIdeal (ideal R S)))
    ((IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
              Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
              (Ideal.cotangentIdeal (ideal R S))) :
          (a : S) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
        x :
      HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
        Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2)) (Ideal.cotangentIdeal (ideal R S)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (e₁.trans (@RingEquiv.congr_arg _ _ _ _ _ _
      (KaehlerDifferential.quotientCotangentIdealRingEquiv R S) _ _ e)).trans e₂.symm

Premises used: RingEquiv.congr_arg, Eq.symm, Eq.trans