-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
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))
⊢ 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)
have 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) sorry :
                    { 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) sorry)
                  (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)
Tactic: ext x