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
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
refine_2₄ : HAdd.hAdd (α := M) 0 0 = 0
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)
have refine_2₅ : Eq.{u_1 + 1} (α := M) 0 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
⊢ ((D.liftKaehlerDifferential.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) :
        (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
      (KaehlerDifferential.D R S) =
    D
have H : ∀ (a : S),
  Eq.{u_1 + 1} (α := M)
    (((((D.liftKaehlerDifferential.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) :
                (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
              (KaehlerDifferential.D R S) :
            Derivation R S M) :
          (a : S) → M)
        a :
      M)
    ((D : (a : S) → M) a : M)
Tactic: ext a
-- 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
a : S
⊢ Eq.{u_1 + 1} (α := M)
    (((((D.liftKaehlerDifferential.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) :
                (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
              (KaehlerDifferential.D R S) :
            Derivation R S M) :
          (a : S) → M)
        a :
      M)
    ((D : (a : S) → M) a : M)
have H : Eq.{u_1 + 1} (α := M)
  ((D.liftKaehlerDifferential : (a : Ω[S⁄R]) → M)
      ((Ideal.toCotangent (KaehlerDifferential.ideal R S) :
            (a : ↥(KaehlerDifferential.ideal R S)) → (KaehlerDifferential.ideal R S).Cotangent)
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦
            Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) sorry) :
        Ideal.Cotangent (R := S ⊗[R] S) (KaehlerDifferential.ideal R S)) :
    M)
  ((D : (a : S) → M) a : M)
Tactic: dsimp [KaehlerDifferential.D_apply]
-- 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
a : S
⊢ Eq.{u_1 + 1} (α := M)
    ((D.liftKaehlerDifferential : (a : Ω[S⁄R]) → M)
        ((Ideal.toCotangent (KaehlerDifferential.ideal R S) :
              (a : ↥(KaehlerDifferential.ideal R S)) → (KaehlerDifferential.ideal R S).Cotangent)
            (Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          Ideal.Cotangent (R := S ⊗[R] S) (KaehlerDifferential.ideal R S)) :
      M)
    ((D : (a : S) → M) a : M)
have H : Eq.{u_1 + 1} (α := M)
  ((D.tensorProductTo : (a : S ⊗[R] S) → M)
      (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) sorry) :
        S ⊗[R] S) :
    M)
  ((D : (a : S) → M) a : M)
Tactic: refine (D.liftKaehlerDifferential_apply _).trans ?_
-- 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
a : S
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H : Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
  ((D : (a : S) → M) a : M)
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₁ : HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
  (D : (a : S) → M) a
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
H₁ :
  HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₂ : HSub.hSub (β := M) (HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M))
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
  (D : (a : S) → M) a
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
H₁ :
  HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₂ :
  HSub.hSub (β := M) (HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M))
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₃ : HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M) -
    HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M) =
  (D : (a : S) → M) a
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
H₁ :
  HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₂ :
  HSub.hSub (β := M) (HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M))
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₃ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M) -
      HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M) =
    (D : (a : S) → M) a
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₄ : HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M)) = (D : (a : S) → M) a
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
H₁ :
  HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₂ :
  HSub.hSub (β := M) (HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M))
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₃ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M) -
      HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M) =
    (D : (a : S) → M) a
H₄ :
  HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M)) = (D : (a : S) → M) a
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₅ : HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a 0) = (D : (a : S) → M) a
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
H₁ :
  HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₂ :
  HSub.hSub (β := M) (HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M))
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₃ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M) -
      HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M) =
    (D : (a : S) → M) a
H₄ :
  HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M)) = (D : (a : S) → M) a
H₅ : HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a 0) = (D : (a : S) → M) a
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₆ : HSub.hSub (α := M) (β := M) ((D : (a : S) → M) a : M) (0 : M) = (D : (a : S) → M) a
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
a : S
H :
  Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) : M)
    ((D : (a : S) → M) a : M)
H₁ :
  HSub.hSub (α := M) (β := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (1 ⊗ₜ[R] a) : M)
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₂ :
  HSub.hSub (β := M) (HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M))
      ((D.tensorProductTo : (a : S ⊗[R] S) → M) (a ⊗ₜ[R] 1) : M) =
    (D : (a : S) → M) a
H₃ :
  HSMul.hSMul.{v, u_1, u_1} (α := S) (β := M) 1 ((D : (a : S) → M) a : M) -
      HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M) =
    (D : (a : S) → M) a
H₄ :
  HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a ((D : (a : S) → M) 1 : M)) = (D : (a : S) → M) a
H₅ : HSub.hSub (α := M) ((D : (a : S) → M) a : M) (HSMul.hSMul (β := M) a 0) = (D : (a : S) → M) a
H₆ : HSub.hSub (α := M) (β := M) ((D : (a : S) → M) a : M) (0 : M) = (D : (a : S) → M) a
⊢ Eq.{u_1 + 1} (α := M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M)
        (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦
              Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
have H₇ : Eq.{u_1 + 1} (α := M) ((D : (a : S) → M) a : M) ((D : (a : S) → M) a : M)
Tactic: rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]
-- 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
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
⊢ f = f'
have h : ∀ (x : Ω[S⁄R]), Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
Tactic: apply LinearMap.ext
-- 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
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
⊢ Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
have rw : Membership.mem (γ := Submodule S Ω[S⁄R]) ⊤ x
Tactic: rw [KaehlerDifferential.span_range_derivation]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
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
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
have this : Membership.mem (γ := Submodule S Ω[S⁄R])
  (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
Tactic: have : x ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) := by
    rw [KaehlerDifferential.span_range_derivation]; 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
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
have h : ∀ (x : Ω[S⁄R])
  (h : Membership.mem (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R])) x),
  Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ this
-- 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
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
h :
  ∀ (x : Ω[S⁄R])
    (h : Membership.mem (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R])) x),
    Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
have h₁ : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) 0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ this
-- 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
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
h :
  ∀ (x : Ω[S⁄R])
    (h : Membership.mem (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R])) x),
    Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
h₁ : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) 0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
have h₂ : ∀ (x y : Ω[S⁄R])
  (hx :
    Membership.mem (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x)
  (hy :
    Membership.mem (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) y),
  Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M) →
    Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) y : M) ((f' : (a : Ω[S⁄R]) → M) y : M) →
      Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (x + y) : M) ((f' : (a : Ω[S⁄R]) → M) (x + y) : M)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ this