awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
x y : S
simp_rw :
  HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) =
    HSMul.hSMul (β := S ⊗[R] S) x (1 ⊗ₜ[R] y) - HSMul.hSMul (β := S ⊗[R] S) x (y ⊗ₜ[R] 1)
simp_rw₁ :
  HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) =
    HSub.hSub (α := S ⊗[R] S) (HSMul.hSMul (β := S) x 1 ⊗ₜ[R] y) ((x • y) ⊗ₜ[R] 1)
⊢ HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
have simp_rw₂ : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = HSub.hSub (α := S ⊗[R] S) ((x * 1) ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1)
Tactic: simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- 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
x_1 : S ⊗[R] S
x y : S
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (β := S ⊗[R] S) (x ⊗ₜ[R] y)
      ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 : S ⊗[R] S))
have this : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
Tactic: have : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] (1 : S) = x • ((1 : S) ⊗ₜ y - y ⊗ₜ (1 : S)) := by
        simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
x y : S
this : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (β := S ⊗[R] S) (x ⊗ₜ[R] y)
      ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 : S ⊗[R] S))
have a : Membership.mem (γ := Submodule S (S ⊗[R] S))
  (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1))
Tactic: rw [TensorProduct.lmul'_apply_tmul, 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
x_1 : S ⊗[R] S
x y : S
this : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1))
have a : Membership.mem (γ := Submodule S (S ⊗[R] S))
  (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1))
Tactic: refine Submodule.smul_mem _ x ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 : S ⊗[R] S
x y : S
this : HSub.hSub (α := S ⊗[R] S) (x ⊗ₜ[R] y) ((x * y) ⊗ₜ[R] 1) = x • HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1))
have a : Membership.mem (γ := Set (S ⊗[R] S)) (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))
  (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1))
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x_1 x y : S ⊗[R] S
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S))
hy :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (β := S ⊗[R] S) y ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y ⊗ₜ[R] 1 : S ⊗[R] S))
⊢ Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (β := S ⊗[R] S) (x + y) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (x + y) ⊗ₜ[R] 1 : S ⊗[R] S))
have a : Membership.mem (γ := Submodule S (S ⊗[R] S))
  (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (HSub.hSub (β := S ⊗[R] S) x ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x ⊗ₜ[R] 1 : S ⊗[R] S) +
    HSub.hSub (β := S ⊗[R] S) y ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) y ⊗ₜ[R] 1 : S ⊗[R] S))
Tactic: rw [map_add, TensorProduct.add_tmul, ← sub_add_sub_comm]
-- 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
⊢ Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (ideal R S)
have a : LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (ideal R S)
Tactic: apply le_antisymm
-- 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
a :
  LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (ideal R S)
⊢ Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (ideal R S)
have a₁ : LE.le (α := Ideal (S ⊗[R] S)) (ideal R S)
  (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
Tactic: apply le_antisymm
-- 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
⊢ LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (ideal R S)
have a : (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) ⊆ (↑(ideal R S) : Set (S ⊗[R] S))
Tactic: rw [Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ LE.le (α := Submodule S (S ⊗[R] S)) (Submodule.restrictScalars S (ideal R S))
    (Submodule.restrictScalars S
      (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))))
have a : LE.le (α := Submodule S (S ⊗[R] S))
  (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (Submodule.restrictScalars S (R := S ⊗[R] S)
    (Submodule.span (S ⊗[R] S) (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))))
Tactic: rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
| Submodule.restrictScalars S (R := S ⊗[R] S)
    (Submodule.span (S ⊗[R] S) (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
have rw : Submodule.restrictScalars S (R := S ⊗[R] S)
  (Submodule.span (S ⊗[R] S)
    (↑(Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) : Set (S ⊗[R] S)))
Tactic: rw [← Submodule.span_span_of_tower S]
-- 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
⊢ LE.le (α := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Submodule.restrictScalars S (R := S ⊗[R] S)
      (Submodule.span (S ⊗[R] S) (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))))
have a : LE.le (α := Submodule S (S ⊗[R] S))
  (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
  (Submodule.restrictScalars S (R := S ⊗[R] S)
    (Submodule.span (S ⊗[R] S)
      (↑(Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) :
        Set (S ⊗[R] S))))
Tactic: conv_rhs => rw [← Submodule.span_span_of_tower S]
-- 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
⊢ Eq (α := Ω[S⁄R]) ((DLinearMap R S : (a : S) → Ω[S⁄R]) 1) 0
have dsimp : Eq (α := Ω[S⁄R])
  (Submodule.Quotient.mk
    (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
      (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1)) sorry))
  0
Tactic: dsimp [KaehlerDifferential.DLinearMap_apply, Ideal.toCotangent_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
⊢ Eq (α := Ω[S⁄R])
    (Submodule.Quotient.mk
      (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
        (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1)) ⋯))
    0
have e_a : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1) = 0
Tactic: congr
-- 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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1) = 0
have e_a : Eq.{v + 1} (α := S ⊗[R] S) 0 0
Tactic: rw [sub_self]
-- 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
a b : S
⊢ (DLinearMap R S : (a : S) → Ω[S⁄R]) (a * b) =
    HSMul.hSMul (β := Ω[S⁄R]) a ((DLinearMap R S : (a : S) → Ω[S⁄R]) b : Ω[S⁄R]) +
      HSMul.hSMul (β := Ω[S⁄R]) b ((DLinearMap R S : (a : S) → Ω[S⁄R]) a : Ω[S⁄R])
have this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
Tactic: have : LinearMap.CompatibleSMul { x // x ∈ ideal R S } Ω[S⁄R] S (S ⊗[R] S) := inferInstance
-- 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
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ (DLinearMap R S : (a : S) → Ω[S⁄R]) (a * b) =
    HSMul.hSMul (β := Ω[S⁄R]) a ((DLinearMap R S : (a : S) → Ω[S⁄R]) b : Ω[S⁄R]) +
      HSMul.hSMul (β := Ω[S⁄R]) b ((DLinearMap R S : (a : S) → Ω[S⁄R]) a : Ω[S⁄R])
have dsimp : (Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
    (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
      (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) sorry) =
  HSMul.hSMul (β := Ω[S⁄R]) a
      ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) sorry) :
        Ideal.Cotangent (R := S ⊗[R] S) (ideal R S)) +
    HSMul.hSMul (β := Ω[S⁄R]) b
      ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
          (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) sorry) :
        Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))
Tactic: dsimp [KaehlerDifferential.DLinearMap_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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ (Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
      (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
        (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) =
    HSMul.hSMul (β := Ω[S⁄R]) a
        ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
            (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯) :
          Ideal.Cotangent (R := S ⊗[R] S) (ideal R S)) +
      HSMul.hSMul (β := Ω[S⁄R]) b
        ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
            (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))
have rw : (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) sorry) :
      S ⊗[R] S) -
    (↑(a •
            Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) sorry +
          b •
            Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) sorry) :
      S ⊗[R] S) ∈
  HMul.hMul (α := Ideal (S ⊗[R] S)) (ideal R S) (ideal R S)
Tactic: rw [← LinearMap.map_smul_of_tower (ideal R S).toCotangent,
        ← LinearMap.map_smul_of_tower (ideal R S).toCotangent,
        ← map_add (ideal R S).toCotangent, Ideal.toCotangent_eq, pow_two]
-- 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
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
rw :
  (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) -
      (↑(a •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯ +
            b •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) ∈
    HMul.hMul (α := Ideal (S ⊗[R] S)) (ideal R S) (ideal R S)
⊢ (Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
      (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
        (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) =
    HSMul.hSMul (β := Ω[S⁄R]) a
        ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
            (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯) :
          Ideal.Cotangent (R := S ⊗[R] S) (ideal R S)) +
      HSMul.hSMul (β := Ω[S⁄R]) b
        ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent)
            (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
          Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))
have rw₁ : LinearMap.CompatibleSMul (↥(ideal R S)) (Ideal.Cotangent (R := S ⊗[R] S) (ideal R S)) S (S ⊗[R] S)
Tactic: rw [← LinearMap.map_smul_of_tower (ideal R S).toCotangent,
        ← LinearMap.map_smul_of_tower (ideal R S).toCotangent,
        ← map_add (ideal R S).toCotangent, Ideal.toCotangent_eq, pow_two]
-- 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
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) -
      (↑(a •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯ +
            b •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) ∈
    HMul.hMul (α := Ideal (S ⊗[R] S)) (ideal R S) (ideal R S)
have h : (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
          (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) sorry) :
      S ⊗[R] S) -
    (↑(a •
            Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) sorry +
          b •
            Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
              (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) sorry) :
      S ⊗[R] S) =
  HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1) * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)
Tactic: convert!
        Submodule.mul_mem_mul (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R a :)
          (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R b :) using 1
-- 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
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ (↑(Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
            (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) -
      (↑(a •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)) ⋯ +
            b •
              Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x)
                (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) ⋯) :
        S ⊗[R] S) =
    HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1) * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] b) (b ⊗ₜ[R] 1)
have h : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) ((a * b) ⊗ₜ[R] 1) -
    (HSub.hSub (α := S ⊗[R] S) (a ⊗ₜ[R] b) ((a * b) ⊗ₜ[R] 1) +
      HSub.hSub (α := S ⊗[R] S) ((1 * b) ⊗ₜ[R] a) ((a * b) ⊗ₜ[R] 1)) =
  HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] (a * b)) (a ⊗ₜ[R] (1 * b)) -
    HSub.hSub (α := S ⊗[R] S) ((1 * b) ⊗ₜ[R] a) ((a * b) ⊗ₜ[R] 1)
Tactic: simp only [Submodule.coe_add,
        TensorProduct.tmul_mul_tmul, mul_sub, sub_mul, mul_comm b, Submodule.coe_smul_of_tower,
        smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- 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
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
have rw : LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
Tactic: rw [_root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : Ω[S⁄R]
⊢ Membership.mem (γ := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) x
have obtain : ∀ (x : S ⊗[R] S) (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
      Ω[S⁄R])
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := fromIdeal_surjective R S x
Cleared hypotheses: x
-- 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
x : S ⊗[R] S
hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
      Ω[S⁄R])
have hx₁ : Membership.mem (γ := Submodule S (S ⊗[R] S))
  (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
Tactic: rw [← Submodule.restrictScalars_mem S, ← KaehlerDifferential.submodule_span_range_eq_ideal] at hx
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S ⊗[R] S
hx_1 : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] S))
    (Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) x
⊢ Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx_1) :
      Ω[S⁄R])
have suffices : ∃ (hx : Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x),
  Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    ((fromIdeal R S : (a : ↥(ideal R S)) → Ω[S⁄R])
        (Subtype.mk (p := fun (x : S ⊗[R] S) ↦ Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x) x hx) :
      Ω[S⁄R])
Tactic: suffices ∃ hx,
      fromIdeal R S ⟨x, hx⟩ ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) from
    this.snd