-- Module: Mathlib.RingTheory.Kaehler.Basic
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 : ↥(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
refine_2 :
  ∀ (r : S ⊗[R] S),
    Membership.mem (γ := Submodule (S ⊗[R] S) (S ⊗[R] S)) (KaehlerDifferential.ideal R S) r →
      ∀ (n : ↥(KaehlerDifferential.ideal R S)),
        Membership.mem (γ := Submodule (S ⊗[R] S) ↥(KaehlerDifferential.ideal R S)) ⊤ n →
          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)
                (r • n) :
              M)
            (0 : M)
refine_2₁ :
  ∀ (x y : ↥(KaehlerDifferential.ideal R S)),
    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) →
      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) →
        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)
⊢ 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)

Tactic:
refine Submodule.smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ ?_