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
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
refine_1 :
  ∀ (x : S) (hx : x ∈ (↑(EssFiniteType.finset R S) : Set S)),
    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])
refine_2 :
  ∀ (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])
refine_3 :
  ∀ (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])
⊢ 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])
have refine_4 : ∀ (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: refine adjoin_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
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 (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
    ((D R S : (a : S) → Ω[S⁄R]) (x * y) : Ω[S⁄R])
have 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]))
Tactic: simp only [Derivation.leibniz]
-- 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
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
⊢ Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have 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])
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)
-- 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
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])
⊢ Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have 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])
Tactic: obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec 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
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)
⊢ Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
have 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])
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]]
-- 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
inst_7 : EssFiniteType R S
let let₁ let₂ : Module.Finite S Ω[S⁄R]
⊢ Module.Finite S Ω[S⁄R]
have let₃ : let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
Tactic: classical
  let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  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)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  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]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))
-- 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
inst_7 : EssFiniteType R S
let let₁ let₂ : Module.Finite S Ω[S⁄R]
let₃ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
⊢ Module.Finite S Ω[S⁄R]
have let₄ : let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
Tactic: classical
  let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  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)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  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]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))
-- 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
inst_7 : EssFiniteType R S
let let₁ let₂ : Module.Finite S Ω[S⁄R]
let₃ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
let₄ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
⊢ Module.Finite S Ω[S⁄R]
have let₅ : let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
∀ (x : S),
  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: classical
  let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  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)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  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]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))
-- 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
inst_7 : EssFiniteType R S
let let₁ let₂ : Module.Finite S Ω[S⁄R]
let₃ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
let₄ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
let₅ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  ∀ (x : S),
    Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
⊢ Module.Finite S Ω[S⁄R]
have let₆ : let 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])),
  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: classical
  let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  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)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  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]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))
-- 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 y z : S
⊢ (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))
have rw : Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
  (HAdd.hAdd (α := S →₀ S) (single x z) (single y z) - single (x + y) z)
Tactic: rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_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
x y z : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HAdd.hAdd (α := S →₀ S) (single x z) (single y z) - single (x + y) z)
have 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))
Tactic: simp_rw [← Finsupp.smul_single_one _ z, ← smul_add, ← smul_sub]
-- 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 y z : S
⊢ (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))
have 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)
Tactic: rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_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
x y z : S
⊢ 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)
have 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))
Tactic: simp_rw [← Finsupp.smul_single_one _ z, ← @smul_eq_mul _ _ z, ← Finsupp.smul_single, ← smul_add,
    ← smul_sub]
-- 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 : R
y : 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))
have 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))
Tactic: rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, ← Finsupp.smul_single_one _ 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
x : S
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (x𝖣1 : 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))
have rw : Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
  (x𝖣(algebraMap R S : (a : R) → S) 1 : 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 [← (algebraMap R S).map_one, KaehlerDifferential.kerTotal_mkQ_single_algebraMap]
-- 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
rw :
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (x𝖣(algebraMap R S : (a : R) → S) 1 : 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))
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (x𝖣1 : 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))
have rw₁ : Eq.{v + 1} (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) 0 0
Tactic: rw [← (algebraMap R S).map_one, KaehlerDifferential.kerTotal_mkQ_single_algebraMap]
-- 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
a b : S
⊢ 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))
      ((1 * a)𝖣b : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((1 * b)𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) =
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) a
        (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := ⋯, map_smul' := ⋯ :
                S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
              (a : S) → (S →₀ S) ⧸ kerTotal R S)
            b :
          HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) +
      HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
        (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := ⋯, map_smul' := ⋯ :
                S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
              (a : S) → (S →₀ S) ⧸ kerTotal R S)
            a :
          HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
have simp_rw : 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))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        (HSMul.hSMul (β := S →₀ S) (1 * a) (single b 1)) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        (HSMul.hSMul (β := S →₀ S) (1 * b) (single a 1)) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) =
  HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) a
      (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := sorry, map_smul' := sorry :
              S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
            (a : S) → (S →₀ S) ⧸ kerTotal R S)
          b :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) +
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
      (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := sorry, map_smul' := sorry :
              S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
            (a : S) → (S →₀ S) ⧸ kerTotal R S)
          a :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
Tactic: simp_rw [← Finsupp.smul_single_one _ (1 * _ : S)]