awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
        Ω[S⁄R])
have refine_1 : ∀ (x : S ⊗[R] S)
  (h :
    Membership.mem (γ := Set (S ⊗[R] S)) (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x),
  ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
        Ω[S⁄R])
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
-- 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
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
refine_1 :
  ∀ (x : S ⊗[R] S)
    (h :
      Membership.mem (γ := Set (S ⊗[R] S)) (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))
        x),
    ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
        (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
        ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
            (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
          Ω[S⁄R])
⊢ ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
        Ω[S⁄R])
have refine_2 : ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) 0),
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) 0 hx) :
      Ω[S⁄R])
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
-- 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
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
⊢ ∃ (hx :
    Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S)
      ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x)),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
      ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) hx) :
        Ω[S⁄R])
have refine_1 : Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
  (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
  ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
      (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
        ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) sorry) :
    Ω[S⁄R])
Tactic: refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
-- 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
x_1 : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x_1
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x_1
x : S
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) ⋯) :
      Ω[S⁄R])
have refine_1 : Membership.mem (α := Ω[S⁄R]) (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
  ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
      (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
        ((fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) x) sorry) :
    Ω[S⁄R])
Tactic: apply Submodule.subset_span
-- 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
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Subsingleton.{v + 1} Ω[S⁄R]
have suffices : LE.le.{v} (α := Submodule S Ω[S⁄R]) ⊤ ⊥
Tactic: suffices (⊤ : Submodule S Ω[S⁄R]) ≤ ⊥ from
    (subsingleton_iff_forall_eq 0).mpr fun y ↦ this trivial
-- 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
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ LE.le.{v} (α := Submodule S Ω[S⁄R]) ⊤ ⊥
have rw : Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑⊥ : Set Ω[S⁄R])
Tactic: rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
-- 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
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : S
⊢ Membership.mem (α := Ω[S⁄R]) (↑⊥ : Set Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have obtain : ∀ (x : R),
  Membership.mem (α := Ω[S⁄R]) (↑⊥ : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) x) : Ω[S⁄R])
Tactic: obtain ⟨x, rfl⟩ := h x
Cleared hypotheses: x
-- 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
⊢ Ω[S⁄R] →ₗ[S] M
have refine_1 : ↥(KaehlerDifferential.ideal R S) →ₗ[S] M
Tactic: refine LinearMap.comp ((((KaehlerDifferential.ideal R S) •
    (⊤ : Submodule (S ⊗[R] S) (KaehlerDifferential.ideal R S))).restrictScalars S).liftQ ?_ ?_)
    (Submodule.Quotient.restrictScalarsEquiv S _).symm.toLinearMap
-- 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
refine_1 : ↥(KaehlerDifferential.ideal R S) →ₗ[S] M
⊢ Ω[S⁄R] →ₗ[S] M
have refine_2 : LE.le (α := 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) ⊤))
  (LinearMap.ker
    (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))))
Tactic: refine LinearMap.comp ((((KaehlerDifferential.ideal R S) •
    (⊤ : Submodule (S ⊗[R] S) (KaehlerDifferential.ideal R S))).restrictScalars S).liftQ ?_ ?_)
    (Submodule.Quotient.restrictScalarsEquiv S _).symm.toLinearMap
-- 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 : ↥(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
⊢ 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)
have 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)
Tactic: refine Submodule.smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ ?_
-- 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_1 :
  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 : S ⊗[R] S
hx : Membership.mem (γ := Submodule (S ⊗[R] S) (S ⊗[R] S)) (KaehlerDifferential.ideal R S) 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 • y) :
      M)
    (0 : M)
have refine_2 : ∀ (hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S))
  (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 • y) :
      M)
    (0 : M)
Tactic: rw [RingHom.mem_ker] at hx
Cleared hypotheses: hx, y
-- 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_1 :
  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 : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
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 • y) :
      M)
    (0 : M)
have refine_2 : Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
Tactic: dsimp
-- 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_1 :
  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 : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
y : ↥(KaehlerDifferential.ideal R S)
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
have refine_2 : HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
  0
Tactic: rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add]
-- 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_1 :
  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 : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
y : ↥(KaehlerDifferential.ideal R S)
refine_2 :
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
have refine_2₁ : HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
    HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
  0
Tactic: rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add]
-- 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_1 :
  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 : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
y : ↥(KaehlerDifferential.ideal R S)
refine_2 :
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
refine_2₁ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
have refine_2₂ : HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
    HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
  0
Tactic: rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add]
-- 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_1 :
  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 : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
y : ↥(KaehlerDifferential.ideal R S)
refine_2 :
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
refine_2₁ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
refine_2₂ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
have refine_2₃ : 0 + HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) = 0
Tactic: rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add]
-- 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_1 :
  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 : S ⊗[R] S
hx : Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S) (0 : S)
y : ↥(KaehlerDifferential.ideal R S)
refine_2 :
  HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
refine_2₁ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul (α := S) (β := M) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (↑y : S ⊗[R] S) : S)
        ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
refine_2₂ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑y : S ⊗[R] S) : M) +
      HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) =
    0
refine_2₃ : 0 + HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 0 ((D.tensorProductTo : (a : S ⊗[R] S) → M) x : M) = 0
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
have refine_2₄ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add]