-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D₁ D₂ : Derivation R A M
⊢ (let __LinearMap : A →ₗ[R] N :=
      (↑R :
            {S : Type u_2} →
              {M : Type u_4} →
                {M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_14 : Semiring S] →
                      [inst_15 : AddCommMonoid M] →
                        [inst_16 : AddCommMonoid M₂] →
                          [inst_17 : Module R M] →
                            [inst_18 : Module R M₂] →
                              [inst_19 : Module S M] →
                                [inst_20 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f ∘ₗ
        (↑(D₁ + D₂) : A →ₗ[R] M);
    { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) =
    HAdd.hAdd (α := Derivation R A N)
      (let __LinearMap : A →ₗ[R] N :=
        (↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_14 : Semiring S] →
                        [inst_15 : AddCommMonoid M] →
                          [inst_16 : AddCommMonoid M₂] →
                            [inst_17 : Module R M] →
                              [inst_18 : Module R M₂] →
                                [inst_19 : Module S M] →
                                  [inst_20 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f ∘ₗ
          (↑D₁ : A →ₗ[R] M);
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ : Derivation R A N })
      (let __LinearMap : A →ₗ[R] N :=
        (↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_14 : Semiring S] →
                        [inst_15 : AddCommMonoid M] →
                          [inst_16 : AddCommMonoid M₂] →
                            [inst_17 : Module R M] →
                              [inst_18 : Module R M₂] →
                                [inst_19 : Module S M] →
                                  [inst_20 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f ∘ₗ
          (↑D₂ : A →ₗ[R] M);
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ : Derivation R A N })
have H : ∀ (a : A),
  Eq.{u_5 + 1} (α := N)
    ((let __LinearMap : A →ₗ[R] N :=
            (↑R :
                  {S : Type u_2} →
                    {M : Type u_4} →
                      {M₂ : Type u_5} →
                        [inst : Semiring R] →
                          [inst_14 : Semiring S] →
                            [inst_15 : AddCommMonoid M] →
                              [inst_16 : AddCommMonoid M₂] →
                                [inst_17 : Module R M] →
                                  [inst_18 : Module R M₂] →
                                    [inst_19 : Module S M] →
                                      [inst_20 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                f ∘ₗ
              (↑(D₁ + D₂) : A →ₗ[R] M);
          { toLinearMap := __LinearMap, map_one_eq_zero' := sorry, leibniz' := sorry } :
          (a : A) → N)
        a :
      N)
    ((HAdd.hAdd (α := Derivation R A N)
            (let __LinearMap : A →ₗ[R] N :=
              (↑R :
                    {S : Type u_2} →
                      {M : Type u_4} →
                        {M₂ : Type u_5} →
                          [inst : Semiring R] →
                            [inst_14 : Semiring S] →
                              [inst_15 : AddCommMonoid M] →
                                [inst_16 : AddCommMonoid M₂] →
                                  [inst_17 : Module R M] →
                                    [inst_18 : Module R M₂] →
                                      [inst_19 : Module S M] →
                                        [inst_20 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  f ∘ₗ
                (↑D₁ : A →ₗ[R] M);
            { toLinearMap := __LinearMap, map_one_eq_zero' := sorry, leibniz' := sorry : Derivation R A N })
            (let __LinearMap : A →ₗ[R] N :=
              (↑R :
                    {S : Type u_2} →
                      {M : Type u_4} →
                        {M₂ : Type u_5} →
                          [inst : Semiring R] →
                            [inst_14 : Semiring S] →
                              [inst_15 : AddCommMonoid M] →
                                [inst_16 : AddCommMonoid M₂] →
                                  [inst_17 : Module R M] →
                                    [inst_18 : Module R M₂] →
                                      [inst_19 : Module S M] →
                                        [inst_20 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  f ∘ₗ
                (↑D₂ : A →ₗ[R] M);
            { toLinearMap := __LinearMap, map_one_eq_zero' := sorry, leibniz' := sorry : Derivation R A N }) :
          (a : A) → N)
        a :
      N)
Tactic: ext