awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : ↥(KaehlerDifferential.ideal R S) →ₗ[S] M
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))))
⊢ Ω[S⁄R] →ₗ[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

Premises used: LinearEquiv.symm, Submodule.restrictScalars, KaehlerDifferential.ideal, LinearMap.comp, LinearEquiv.toLinearMap, Submodule.Quotient.restrictScalarsEquiv, HSMul.hSMul, Submodule.liftQ, Top.top
-- 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
⊢ ↥(KaehlerDifferential.ideal R S) →ₗ[S] M

Tactic:
exact D.tensorProductTo.comp ((KaehlerDifferential.ideal R S).subtype.restrictScalars S)

Premises used: LinearMap.restrictScalars, KaehlerDifferential.ideal, Derivation.tensorProductTo, LinearMap.comp, Submodule.subtype
-- 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
⊢ 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:
Submodule.smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ ?_

Premises used: KaehlerDifferential.ideal, Submodule.smul_induction_on, Submodule.restrictScalars_mem, Iff.mp, HSMul.hSMul, Top.top
-- 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_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)
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)
⊢ 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

Premises used: RingHom.mem_ker
-- 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_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 : Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : 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)

Tactic:
dsimp
-- 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_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
refine_2₅ refine_2₆ : Eq.{u_1 + 1} (α := M) 0 0
⊢ Eq.{u_1 + 1} (α := M) ((D.tensorProductTo : (a : S ⊗[R] S) → M) (x * (↑y : S ⊗[R] S)) : M) (0 : M)

Tactic:
rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add]

Premises used: zero_add, zero_smul, Derivation.tensorProductTo_mul, Subtype.prop
-- 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)
⊢ 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)
            x :
          Ideal.Cotangent (R := S ⊗[R] S) (KaehlerDifferential.ideal R S)) :
      M)
    ((D.tensorProductTo : (a : S ⊗[R] S) → M) (↑x : S ⊗[R] S) : M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- 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
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)
⊢ ((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

Tactic:
ext a
-- 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
a : S
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)) ⋯) :
          Ideal.Cotangent (R := S ⊗[R] S) (KaehlerDifferential.ideal R S)) :
      M)
    ((D : (a : S) → M) a : M)
⊢ 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:
dsimp [KaehlerDifferential.D_apply]

Premises used: KaehlerDifferential.D_apply
-- 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
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)

Tactic:
(D.liftKaehlerDifferential_apply _).trans ?_

Premises used: Derivation.liftKaehlerDifferential_apply, Eq.trans
-- 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
a : S
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)) ⋯) :
          S ⊗[R] S) :
      M)
    ((D : (a : S) → M) a : M)
⊢ 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)

Tactic:
refine (D.liftKaehlerDifferential_apply _).trans ?_

Premises used: Derivation.liftKaehlerDifferential_apply, Eq.trans
-- 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
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
H₇ H₈ : Eq.{u_1 + 1} (α := M) ((D : (a : S) → M) a : 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)

Tactic:
rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
    one_smul, D.map_one_eq_zero, smul_zero, sub_zero]

Premises used: Subtype.coe_mk, map_sub, sub_zero, Derivation.map_one_eq_zero, smul_zero, one_smul, Derivation.tensorProductTo_tmul
-- 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 : S
⊢ Eq.{u_1 + 1} (α := M)
    ((D'.liftKaehlerDifferential : (a : Ω[S⁄R]) → M) ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) : M)
    ((D' : (a : S) → M) x : M)

Tactic:
Derivation.congr_fun D'.liftKaehlerDifferential_comp x

Premises used: Quotient.liftOn', AddCon.liftOn, Derivation.liftKaehlerDifferential_comp, List.foldl, Derivation.congr_fun, FreeAddMonoid.sumAux
-- 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
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)
h : ∀ (x : Ω[S⁄R]), Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
⊢ f = f'

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- 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
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]
rw : Membership.mem (γ := Submodule S Ω[S⁄R]) ⊤ x
⊢ Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x

Tactic:
rw [KaehlerDifferential.span_range_derivation]

Premises used: KaehlerDifferential.span_range_derivation
-- 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
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]) ⊤ x

Tactic:
trivial
-- 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
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

Tactic:
have : x ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) := by
    rw [KaehlerDifferential.span_range_derivation]; trivial
-- 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
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)

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ this

Premises used: Submodule.span_induction
-- 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
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)
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)
h₃ :
  ∀ (a : S) (x : Ω[S⁄R])
    (hx :
      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) →
      Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (a • x) : M) ((f' : (a : Ω[S⁄R]) → M) (a • x) : M)
⊢ 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