-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 ((_fe.1 : (a : A) → B) a) }
a : A
ad : A[ε]
rw :
  (((lift :
              (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                A[ε] →ₐ[R] B)
            fe :
          AlgHom.{u_1, u_4, u_3} R A[ε] B) :
        (a : A[ε]) → B)
      (ad * inl a) =
    HMul.hMul (α := B) (β := B)
      ((((lift :
                  (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                    A[ε] →ₐ[R] B)
                fe :
              AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          ad :
        B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
rw₁ :
  HMul.hMul (α := B) (β := B)
      ((((lift :
                  (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                    A[ε] →ₐ[R] B)
                fe :
              AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          ad :
        B)
      ((((lift :
                  (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                    A[ε] →ₐ[R] B)
                fe :
              AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          (inl a) :
        B) =
    HMul.hMul (α := B) (β := B)
      ((((lift :
                  (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                    A[ε] →ₐ[R] B)
                fe :
              AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          ad :
        B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
⊢ (((lift :
              (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                A[ε] →ₐ[R] B)
            fe :
          AlgHom.{u_1, u_4, u_3} R A[ε] B) :
        (a : A[ε]) → B)
      (MulOpposite.op a • ad) =
    HMul.hMul (α := B) (β := B)
      ((((lift :
                  (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                    A[ε] →ₐ[R] B)
                fe :
              AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          ad :
        B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
have rw₂ : HMul.hMul (α := B) (β := B)
    ((((lift :
                (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                  A[ε] →ₐ[R] B)
              fe :
            AlgHom.{u_1, u_4, u_3} R A[ε] B) :
          (a : A[ε]) → B)
        ad :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) =
  HMul.hMul (α := B) (β := B)
    ((((lift :
                (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                  A[ε] →ₐ[R] B)
              fe :
            AlgHom.{u_1, u_4, u_3} R A[ε] B) :
          (a : A[ε]) → B)
        ad :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
Tactic: rw [← mul_inl_eq_op_smul, map_mul, lift_apply_inl]