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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
⊢ ∀ (r : R),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
      ((D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) r) : Ω[S⁄R])

Tactic:
simp
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
⊢ ∀ (x y : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x)
    (hy : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
        Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) (x + y) : Ω[S⁄R])

Tactic:
fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy

Premises used: Eq.rec, KaehlerDifferential.D, Derivation.map_add, AddMemClass.add_mem, Eq.symm
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
⊢ ∀ (x y : S) (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x)
    (hy : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
        Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) (x + y) : Ω[S⁄R])

Tactic:
exact fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x_2 : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x_2
x y : S
refine_4 :
  Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
    ∀ (hy : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y),
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
        Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
            ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
          Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
            ((D R S : (a : S) → Ω[S⁄R]) (x * y) : Ω[S⁄R])
⊢ ∀ (hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x)
    (hy : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
        Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) (x * y) : Ω[S⁄R])

Tactic:
_
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x_2 : S
hx : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x_2
x y : S
hx_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
refine_4 :
  Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y →
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
        Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) (x * y) : Ω[S⁄R])
⊢ ∀ (hy : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y),
    Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) →
        Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
          ((D R S : (a : S) → Ω[S⁄R]) (x * y) : Ω[S⁄R])

Tactic:
_
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x_2 : S
hx_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x_2
x y : S
hx_2 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
hy_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y
hx :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
hy :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R])
refine_4 :
  Membership.mem (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) +
      HSMul.hSMul (β := Ω[S⁄R]) y ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]))
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) (x * y) : Ω[S⁄R])

Tactic:
simp only [Derivation.leibniz]

Premises used: Derivation.leibniz
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x_2 : S
hx_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x_2
x y : S
hx_2 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
hy_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y
hx :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
hy :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R])
⊢ Membership.mem (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) +
      HSMul.hSMul (β := Ω[S⁄R]) y ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]))

Tactic:
add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x_1 x_2 : S
hx_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x_2
x y : S
hx_2 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x
hy_1 : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) y
hx :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
hy :
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R])
⊢ Membership.mem (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) y : Ω[S⁄R]) +
      HSMul.hSMul (β := Ω[S⁄R]) y ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]))

Tactic:
exact add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x : S
⊢ ∀ (x : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])

Tactic:
have : ∀ x ∈ adjoin R (EssFiniteType.finset R S : Set S),
      .D _ _ x ∈ Submodule.span S (s : Set Ω[S⁄R]) := by
    intro x hx
    refine adjoin_induction ?_ ?_ ?_ ?_ hx
    · exact fun x hx ↦ Submodule.subset_span (Finset.mem_image_of_mem _ hx)
    · simp
    · exact fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy
    · intro x y _ _ hx hy
      simp only [Derivation.leibniz]
      exact add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x : S
this :
  ∀ (x : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
obtain :
  ∀ (t : S) (ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t)
    (ht' : IsUnit t)
    (hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)),
    Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])

Tactic:
obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x

Premises used: Exists.choose_spec, Algebra.essFiniteType_cond_iff, Algebra.EssFiniteType.finset, Iff.mp, Algebra.EssFiniteType.cond
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x : S
this :
  ∀ (x : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
t : S
ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t
ht' : IsUnit t
hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)
⊢ (D R S : (a : S) → Ω[S⁄R]) x =
    ht'.unit⁻¹ •
      HSub.hSub (α := Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (x * t) : Ω[S⁄R])
        (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) t : Ω[S⁄R]))

Tactic:
simp [smul_smul, Units.smul_def]

Premises used: smul_smul, Units.smul_def
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x : S
this :
  ∀ (x : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
t : S
ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t
ht' : IsUnit t
hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)
rw :
  ht'.unit⁻¹ •
      HSub.hSub (α := Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (x * t) : Ω[S⁄R])
        (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) t : Ω[S⁄R])) ∈
    (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
⊢ Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])

Tactic:
rw [show D R S x =
    ht'.unit⁻¹ • (D R S (x * t) - x • D R S t) by simp [smul_smul, Units.smul_def]]
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x : S
this :
  ∀ (x : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
t : S
ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t
ht' : IsUnit t
hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)
⊢ ht'.unit⁻¹ •
      HSub.hSub (α := Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (x * t) : Ω[S⁄R])
        (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) t : Ω[S⁄R])) ∈
    (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])

Tactic:
Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))

Premises used: Set.Mem, sub_mem, Submodule.smul_mem
-- 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
inst_7 : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S)
x : S
this :
  ∀ (x : S),
    Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
      Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
        ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
t : S
ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t
ht' : IsUnit t
hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)
⊢ ht'.unit⁻¹ •
      HSub.hSub (α := Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (x * t) : Ω[S⁄R])
        (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) t : Ω[S⁄R])) ∈
    (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])

Tactic:
exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))

Premises used: sub_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
rw :
  Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HAdd.hAdd (α := S →₀ S) (single x z) (single y z) - single (x + y) z)
⊢ (z𝖣x + y) =
    HAdd.hAdd (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (β :=
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (z𝖣x : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (z𝖣y : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Premises used: map_sub, sub_eq_zero, map_add, Submodule.mkQ_apply, eq_comm, Submodule.mkQ, KaehlerDifferential.kerTotal, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
simp_rw :
  Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (z • (HAdd.hAdd (α := S →₀ S) (single x 1) (single y 1) - single (x + y) 1))
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HAdd.hAdd (α := S →₀ S) (single x z) (single y z) - single (x + y) z)

Tactic:
simp_rw [← Finsupp.smul_single_one _ z, ← smul_add, ← smul_sub]

Premises used: smul_sub, Finsupp.smul_single_one, smul_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (z • (HAdd.hAdd (α := S →₀ S) (single x 1) (single y 1) - single (x + y) 1))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inl <| ⟨⟨_, _⟩, rfl⟩))

Premises used: Set.Mem, Prod.mk, Exists.intro, Or.inl, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (z • (HAdd.hAdd (α := S →₀ S) (single x 1) (single y 1) - single (x + y) 1))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inl <| ⟨⟨_, _⟩, 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
x y z : S
rw :
  Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HAdd.hAdd (α := S →₀ S) (single y (z * x)) (single x (z * y)) - single (x * y) z)
⊢ (z𝖣x * y) =
    HAdd.hAdd (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (β :=
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((z * x)𝖣y : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((z * y)𝖣x : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Premises used: map_sub, sub_eq_zero, map_add, Submodule.mkQ_apply, eq_comm, Submodule.mkQ, KaehlerDifferential.kerTotal, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
simp_rw :
  Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (z • (HAdd.hAdd (α := S →₀ S) (single y x) (single x y) - single (x * y) 1))
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HAdd.hAdd (α := S →₀ S) (single y (z * x)) (single x (z * y)) - single (x * y) z)

Tactic:
simp_rw [← Finsupp.smul_single_one _ z, ← @smul_eq_mul _ _ z, ← Finsupp.smul_single, ← smul_add,
    ← smul_sub]

Premises used: smul_sub, smul_eq_mul, Finsupp.smul_single_one, Finsupp.smul_single, smul_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (z • (HAdd.hAdd (α := S →₀ S) (single y x) (single x y) - single (x * y) 1))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inr <| ⟨⟨_, _⟩, rfl⟩))

Premises used: Set.Mem, Prod.mk, Exists.intro, Or.inl, Submodule.subset_span, Or.inr, rfl, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y z : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (z • (HAdd.hAdd (α := S →₀ S) (single y x) (single x y) - single (x * y) 1))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inr <| ⟨⟨_, _⟩, 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
x : R
y : S
rw :
  Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HSMul.hSMul (β := S →₀ S) y (single ((algebraMap R S : (a : R) → S) x) 1 : S →₀ S))
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (y𝖣(algebraMap R S : (a : R) → S) x : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (0 : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, ← Finsupp.smul_single_one _ y]

Premises used: Submodule.mkQ_apply, Finsupp.smul_single_one, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : R
y : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HSMul.hSMul (β := S →₀ S) y (single ((algebraMap R S : (a : R) → S) x) 1 : S →₀ S))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span (Or.inr <| ⟨_, rfl⟩))

Premises used: Set.Mem, Exists.intro, Submodule.subset_span, Or.inr, rfl, Submodule.smul_mem