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
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)
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)
⊢ 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:
simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Premises used: smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- 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_1 : S ⊗[R] S
x y : S
⊢ 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]
-- 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_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)
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))
⊢ 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))

Tactic:
rw [TensorProduct.lmul'_apply_tmul, this]

Premises used: Algebra.TensorProduct.lmul'_apply_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
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))

Tactic:
Submodule.smul_mem _ x ?_

Premises used: Set.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_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)
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))
⊢ 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:
refine Submodule.smul_mem _ x ?_

Premises used: 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_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)
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))
⊢ 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:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- 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_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 (γ := 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:
Set.mem_range_self y

Premises used: Set.mem_range_self
-- 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_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 (γ := 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:
exact Set.mem_range_self y

Premises used: Set.mem_range_self
-- 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_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))
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))
⊢ 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))

Tactic:
rw [map_add, TensorProduct.add_tmul, ← sub_add_sub_comm]

Premises used: map_add, sub_add_sub_comm, TensorProduct.add_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
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 ((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:
add_mem hx hy

Premises used: AddMemClass.add_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_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 ((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:
exact add_mem hx hy

Premises used: AddMemClass.add_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
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)
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)))
⊢ 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)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a : (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) ⊆ (↑(ideal R S) : Set (S ⊗[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)

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) s ∈ (↑(ideal R S) : Set (S ⊗[R] S))

Tactic:
KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

Premises used: Set.Mem, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ (fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)) s ∈ (↑(ideal R S) : Set (S ⊗[R] S))

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

Premises used: KaehlerDifferential.one_smul_sub_smul_one_mem_ideal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
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))))
⊢ 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))))

Tactic:
rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]

Premises used: KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
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)))
| 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 [← Submodule.span_span_of_tower S]

Premises used: Submodule.span_span_of_tower
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
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))))
⊢ 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:
conv_rhs => rw [← Submodule.span_span_of_tower S]

Premises used: Submodule.span_span_of_tower
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
        (↑(Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) :
          Set (S ⊗[R] S))))

Tactic:
Submodule.subset_span

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.Subset, Submodule.subset_span
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
        (↑(Submodule.span S (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) :
          Set (S ⊗[R] S))))

Tactic:
exact Submodule.subset_span

Premises used: Submodule.subset_span
-- 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
R₁ : Type u_2
R₂ : Type u_3
inst_7 : CommRing R₁
inst_8 : CommRing R₂
inst_9 : Algebra R₁ S
inst_10 : Algebra R₂ S
inst_11 : SMul R₁ R₂
inst_12 : SMulCommClass R R₁ S
inst_13 : SMulCommClass R R₂ S
inst_14 : IsScalarTower R₁ R₂ S
⊢ IsScalarTower.{u_2, u_3, v} R₁ R₂ Ω[S⁄R]

Tactic:
Submodule.Quotient.isScalarTower _ _

Premises used: Ideal.Cotangent, Submodule.Quotient.isScalarTower, KaehlerDifferential
-- 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
⊢ IsScalarTower.{u, v, v} R (S ⊗[R] S) Ω[S⁄R]

Tactic:
Submodule.Quotient.isScalarTower _ _

Premises used: Ideal.Cotangent, Submodule.Quotient.isScalarTower, KaehlerDifferential
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Function.Surjective (α := ↥(ideal R S)) (β := Ω[S⁄R]) (⇑(fromIdeal R S) : (a : ↥(ideal R S)) → Ω[S⁄R])

Tactic:
Ideal.toCotangent_surjective _

Premises used: Set.Mem, KaehlerDifferential, Ideal.toCotangent_surjective
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ Eq (α := Ω[S⁄R]) ((DLinearMap R S : (a : S) → Ω[S⁄R]) s : Ω[S⁄R])
    ((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] s) (s ⊗ₜ[R] 1)) ⋯) :
      Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))

Tactic:
rfl

Premises used: Set.Mem, Submodule.Quotient.mk, setOf, Set.preimage, Set.singleton, TensorProduct.tmul, AddCon.toQuotient, 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
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)) ⋯))
    0
⊢ Eq (α := Ω[S⁄R]) ((DLinearMap R S : (a : S) → Ω[S⁄R]) 1) 0

Tactic:
dsimp [KaehlerDifferential.DLinearMap_apply, Ideal.toCotangent_apply]

Premises used: Ideal.toCotangent_apply, KaehlerDifferential.DLinearMap_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
e_a : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1) = 0
⊢ 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

Tactic:
congr
-- 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
e_a e_a₁ : Eq.{v + 1} (α := S ⊗[R] S) 0 0
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1) = 0

Tactic:
rw [sub_self]

Premises used: sub_self
-- 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
a b : S
⊢ 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
-- 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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
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)) ⋯) =
    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))
⊢ (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])

Tactic:
dsimp [KaehlerDifferential.DLinearMap_apply]

Premises used: KaehlerDifferential.DLinearMap_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
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)
rw₁ rw₂ : LinearMap.CompatibleSMul (↥(ideal R S)) (Ideal.Cotangent (R := S ⊗[R] S) (ideal R S)) 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))

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]

Premises used: Ideal.toCotangent_eq, pow_two, KaehlerDifferential.ideal, map_add, LinearMap.map_smul_of_tower, Ideal.toCotangent
-- 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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (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) ∈
    HMul.hMul (α := Submodule (S ⊗[R] S) (S ⊗[R] S)) (ideal R S) (ideal R S)

Tactic:
Submodule.mul_mem_mul (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R a :)
          (KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R b :)

Premises used: Submodule.mul_mem_mul, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal