-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
D : Derivation R S M
x_1 : ↥(KaehlerDifferential.ideal R S)
hx :
  Membership.mem (γ := Submodule S ↥(KaehlerDifferential.ideal R S))
    (Submodule.restrictScalars S
      (HSMul.hSMul (α := Ideal (S ⊗[R] S)) (β := Submodule (S ⊗[R] S) ↥(KaehlerDifferential.ideal R S))
        (KaehlerDifferential.ideal R S) ⊤))
    x_1
x y : ↥(KaehlerDifferential.ideal R S)
ex :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo ∘ₗ
            (↑S :
                {S_1 M M₂ : Type v} →
                  [inst : Semiring S] →
                    [inst_7 : Semiring S_1] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module S M] →
                            [inst_11 : Module S M₂] →
                              [inst_12 : Module S_1 M] →
                                [inst_13 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (Submodule.subtype (KaehlerDifferential.ideal R S)) :
          (a : ↥(KaehlerDifferential.ideal R S)) → M)
        x :
      M)
    (0 : M)
ey :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo ∘ₗ
            (↑S :
                {S_1 M M₂ : Type v} →
                  [inst : Semiring S] →
                    [inst_7 : Semiring S_1] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module S M] →
                            [inst_11 : Module S M₂] →
                              [inst_12 : Module S_1 M] →
                                [inst_13 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (Submodule.subtype (KaehlerDifferential.ideal R S)) :
          (a : ↥(KaehlerDifferential.ideal R S)) → M)
        y :
      M)
    (0 : M)
refine_2 :
  HAdd.hAdd (α := M) (β := M)
      ((D.tensorProductTo ∘ₗ
              (↑S :
                  {S_1 M M₂ : Type v} →
                    [inst : Semiring S] →
                      [inst_7 : Semiring S_1] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [inst_12 : Module S_1 M] →
                                  [inst_13 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (Submodule.subtype (KaehlerDifferential.ideal R S)) :
            (a : ↥(KaehlerDifferential.ideal R S)) → M)
          x :
        M)
      ((D.tensorProductTo ∘ₗ
              (↑S :
                  {S_1 M M₂ : Type v} →
                    [inst : Semiring S] →
                      [inst_7 : Semiring S_1] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [inst_12 : Module S_1 M] →
                                  [inst_13 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (Submodule.subtype (KaehlerDifferential.ideal R S)) :
            (a : ↥(KaehlerDifferential.ideal R S)) → M)
          y :
        M) =
    0
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo ∘ₗ
            (↑S :
                {S_1 M M₂ : Type v} →
                  [inst : Semiring S] →
                    [inst_7 : Semiring S_1] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module S M] →
                            [inst_11 : Module S M₂] →
                              [inst_12 : Module S_1 M] →
                                [inst_13 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (Submodule.subtype (KaehlerDifferential.ideal R S)) :
          (a : ↥(KaehlerDifferential.ideal R S)) → M)
        (x + y) :
      M)
    (0 : M)
have refine_2₁ : HAdd.hAdd (α := M) (β := M) (0 : M)
    ((D.tensorProductTo ∘ₗ
            (↑S :
                {S_1 M M₂ : Type v} →
                  [inst : Semiring S] →
                    [inst_7 : Semiring S_1] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module S M] →
                            [inst_11 : Module S M₂] →
                              [inst_12 : Module S_1 M] →
                                [inst_13 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (Submodule.subtype (KaehlerDifferential.ideal R S)) :
          (a : ↥(KaehlerDifferential.ideal R S)) → M)
        y :
      M) =
  0
Tactic: rw [map_add, ex, ey, zero_add]