-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
f : A →ₐ[R] B
hf :
  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f) (IsScalarTower.toAlgHom R A (B ⧸ I))
refine_3 :
  ∀ (x : A),
    Eq.{w + 1} (α := B)
      (((↑((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                    (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
                        Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                          (IsScalarTower.toAlgHom R A (B ⧸ I)))
                        (liftOfDerivationToSquareZero I hI d) ⋯ :
                      { f : A →ₐ[R] B //
                        Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                          (IsScalarTower.toAlgHom R A (B ⧸ I)) }))
                  ((fun
                        (f :
                          { f : A →ₐ[R] B //
                            Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                              (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
                      derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
                    (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
                      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                        (IsScalarTower.toAlgHom R A (B ⧸ I)))
                      f hf))) :
              A →ₐ[R] B) :
            (a : A) → B)
          x :
        B)
      (((↑(Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
                  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                    (IsScalarTower.toAlgHom R A (B ⧸ I)))
                  f hf) :
              A →ₐ[R] B) :
            (a : A) → B)
          x :
        B)
⊢ Eq (α :=
    { f : A →ₐ[R] B //
      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
        (IsScalarTower.toAlgHom R A (B ⧸ I)) })
    ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
        (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
            Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
              (IsScalarTower.toAlgHom R A (B ⧸ I)))
            (liftOfDerivationToSquareZero I hI d) ⋯ :
          { f : A →ₐ[R] B //
            Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
              (IsScalarTower.toAlgHom R A (B ⧸ I)) }))
      ((fun
            (f :
              { f : A →ₐ[R] B //
                Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
                  (IsScalarTower.toAlgHom R A (B ⧸ I)) }) ↦
          derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
        (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
          Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
            (IsScalarTower.toAlgHom R A (B ⧸ I)))
          f hf)))
    (Subtype.mk (p := fun (f : A →ₐ[R] B) ↦
      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
        (IsScalarTower.toAlgHom R A (B ⧸ I)))
      f hf)

Tactic:
ext x