awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
x : R[X]
⊢ AddHom.toFun (LinearMap.toAddHom (Derivation.liftKaehlerDifferential derivative'))
      (((((LinearMap.flip (AlgHom.toLinearMap (lsmul R R Ω[R[X]⁄R]) : R[X] →ₗ[R] End R Ω[R[X]⁄R]) :
                  Ω[R[X]⁄R] →ₗ[R] R[X] →ₗ[R] Ω[R[X]⁄R]) :
                (a : Ω[R[X]⁄R]) → R[X] →ₗ[R] Ω[R[X]⁄R])
              ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X) :
            R[X] →ₗ[R] Ω[R[X]⁄R]) :
          (a : R[X]) → Ω[R[X]⁄R])
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α := Derivation R R[X] R[X])
    (((LinearEquiv.compDer (polynomialEquiv R) : Derivation R R[X] Ω[R[X]⁄R] ≃ₗ[R[X]] Derivation R R[X] R[X]) :
          (a : Derivation R R[X] Ω[R[X]⁄R]) → Derivation R R[X] R[X])
        (D R R[X]) :
      Derivation R R[X] R[X])
    (derivative' : Derivation R R[X] R[X])

Tactic:
Derivation.liftKaehlerDifferential_comp _

Premises used: Derivation.liftKaehlerDifferential, Derivation.liftKaehlerDifferential_comp
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
P : R[X]
⊢ Eq (α := R[X]) ((polynomialEquiv R : (a : Ω[R[X]⁄R]) → R[X]) ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) P) : R[X])
    ((derivative : (a : R[X]) → R[X]) P : R[X])

Tactic:
Derivation.congr_fun (polynomialEquiv_comp_D R) P

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, KaehlerDifferential.polynomialEquiv_comp_D, Polynomial.sum, List.foldl, Derivation.congr_fun, FreeAddMonoid.sumAux, Finset.sum
-- Module: Mathlib.RingTheory.Kaehler.Polynomial
Goal:
R : Type u
inst : CommRing R
P : R[X]
⊢ (LinearEquiv.symm (polynomialEquiv R) : (a : R[X]) → Ω[R[X]⁄R]) P =
    HSMul.hSMul (β := Ω[R[X]⁄R]) P ((D R R[X] : (a : R[X]) → Ω[R[X]⁄R]) X : Ω[R[X]⁄R])

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
s : S
x : Ω[A⁄R]
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (s ⊗ₜ[R] x) = s ⊗ₜ[R] (a • x)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
rw : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (0 ⊗ₜ[R] 0) = 0 ⊗ₜ[R] 0
rw₁ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (0 ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) a 0) (0 ⊗ₜ[R] 0)
rw₂ rw₃ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (0 ⊗ₜ[R] 0) (0 ⊗ₜ[R] 0)
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 = 0

Tactic:
rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]

Premises used: smul_zero, TensorProduct.zero_tmul, OfNat.ofNat, KaehlerDifferential.mulActionBaseChange_smul_tmul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
change :
  (LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
      (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
        ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) (x + y) :
          TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) =
    a • x + a • y
⊢ a • (x + y) = a • x + a • y

Tactic:
change (TensorProduct.comm R S Ω[A⁄R]).symm (a • (TensorProduct.comm R S Ω[A⁄R]) (x + y)) = _

Premises used: LinearEquiv.symm, TensorProduct.comm, HAdd.hAdd, KaehlerDifferential, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
rw :
  HAdd.hAdd (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      ((LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
          (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
            ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) x :
              TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      ((LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
          (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
            ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) y :
              TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    a • x + a • y
⊢ (LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
      (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
        ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) (x + y) :
          TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) =
    a • x + a • y

Tactic:
rw [map_add, smul_add, map_add]

Premises used: map_add, smul_add
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
a : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ HAdd.hAdd (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      ((LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
          (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
            ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) x :
              TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      ((LinearEquiv.symm (TensorProduct.comm R S Ω[A⁄R]) : (a : Ω[A⁄R] ⊗[R] S) → S ⊗[R] Ω[A⁄R])
          (HSMul.hSMul (β := TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S) a
            ((TensorProduct.comm R S Ω[A⁄R] : (a : S ⊗[R] Ω[A⁄R]) → Ω[A⁄R] ⊗[R] S) y :
              TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S)) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    a • x + a • y

Tactic:
rfl
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
⊢ ∀ (a : A), HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
⊢ ∀ (a : A) (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]), a • (x + y) = a • x + a • y

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r s : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0 +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
tmul :
  ∀ (x : S) (y : Ω[A⁄R]),
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) (x ⊗ₜ[R] y) =
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y) +
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
add :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    (r + s) • x = r • x + s • x → (r + s) • y = r • y + s • y → (r + s) • (x + y) = r • (x + y) + s • (x + y)
⊢ (r + s) • x = r • x + s • x

Tactic:
induction x
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r s : A
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0 +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0

Tactic:
simp [add_smul, tmul_add, *, add_add_add_comm]

Premises used: add_smul, TensorProduct.tmul_add, add_add_add_comm
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r s : A
x : S
y : Ω[A⁄R]
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)

Tactic:
simp [add_smul, tmul_add, *, add_add_add_comm]

Premises used: add_smul, TensorProduct.tmul_add, add_add_add_comm
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r s : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h : (r + s) • x = r • x + s • x
h_1 : (r + s) • y = r • y + s • y
⊢ (r + s) • (x + y) = r • (x + y) + s • (x + y)

Tactic:
simp [add_smul, tmul_add, *, add_add_add_comm]

Premises used: add_smul, TensorProduct.tmul_add, add_add_add_comm
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero : HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 0 = 0
tmul : ∀ (x : S) (y : Ω[A⁄R]), HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 (x ⊗ₜ[R] y) = 0
add :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    HSMul.hSMul (α := A) 0 x = 0 → HSMul.hSMul (α := A) 0 y = 0 → HSMul.hSMul (α := A) 0 (x + y) = 0
⊢ HSMul.hSMul (α := A) 0 x = 0

Tactic:
induction x
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 0 = 0

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
x : S
y : Ω[A⁄R]
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 (x ⊗ₜ[R] y) = 0

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h : HSMul.hSMul (α := A) 0 x = 0
h_1 : HSMul.hSMul (α := A) 0 y = 0
⊢ HSMul.hSMul (α := A) 0 (x + y) = 0

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h :
  ∀ (r : R) (x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
⊢ IsScalarTower R A (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
apply IsScalarTower.of_algebraMap_smul

Premises used: IsScalarTower.of_algebraMap_smul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r : R
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h :
  HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0
h₁ :
  ∀ (x : S) (y : Ω[A⁄R]),
    HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
        (x ⊗ₜ[R] y) =
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
h₂ :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x →
      HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y = r • y →
        HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x + y) = r • (x + y)
⊢ HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x

Tactic:
induction x
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r : R
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0

Tactic:
simp only [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r : R
x : S
y : Ω[A⁄R]
h :
  x ⊗ₜ[R] HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
h₁ : x ⊗ₜ[R] (r • y) = HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
h₂ h₃ :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)

Tactic:
rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_smul]

Premises used: TensorProduct.tmul_smul, algebraMap_smul, KaehlerDifferential.mulActionBaseChange_smul_tmul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
r : R
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h : HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
h_1 : HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y = r • y
⊢ HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x + y) = r • (x + y)

Tactic:
simp only [smul_add, *]

Premises used: smul_add
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
s : S
a : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
tmul :
  ∀ (x : S) (y : Ω[A⁄R]),
    s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
      a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
add :
  ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    s • a • x = a • s • x → s • a • y = a • s • y → s • a • (x + y) = a • s • (x + y)
⊢ s • a • x = a • s • x

Tactic:
induction x
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
s : S
a : A
⊢ s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0

Tactic:
simp only [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
s : S
a : A
x : S
y : Ω[A⁄R]
tmul :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] (a • y)) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
tmul₁ : (s • x) ⊗ₜ[R] (a • y) = a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
tmul₂ : (s • x) ⊗ₜ[R] (a • y) = HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a ((s • x) ⊗ₜ[R] y)
tmul₃ tmul₄ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((s • x) ⊗ₜ[R] (a • y)) ((s • x) ⊗ₜ[R] (a • y))
⊢ s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)

Tactic:
rw [mulActionBaseChange_smul_tmul, smul_tmul', smul_tmul', mulActionBaseChange_smul_tmul]

Premises used: TensorProduct.smul_tmul', KaehlerDifferential.mulActionBaseChange_smul_tmul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
s : S
a : A
x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h : s • a • x = a • s • x
h_1 : s • a • y = a • s • y
⊢ s • a • (x + y) = a • s • (x + y)

Tactic:
simp only [smul_add, *]

Premises used: smul_add
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
s : A
a : S
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
rw rw₁ : a • s • x = a • s • x
⊢ s • a • x = a • s • x

Tactic:
rw [← smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
h :
  ∀ (r : A) (x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    HSMul.hSMul (α := B) ((algebraMap A B : (a : A) → B) r : B) x = r • x
⊢ IsScalarTower A B (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
apply IsScalarTower.of_algebraMap_smul

Premises used: IsScalarTower.of_algebraMap_smul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
r : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ HSMul.hSMul (α := Module.End S (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]))
      ((Algebra.pushoutDesc B (Algebra.lsmul R S (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]))
              (Algebra.lsmul R S (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])) ⋯ :
            (a : B) → Module.End S (S ⊗[R] Ω[A⁄R]))
          ((algebraMap A B : (a : A) → B) r) :
        Module.End S (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]))
      x =
    r • x

Tactic:
simp only [Algebra.pushoutDesc_right, Module.End.smul_def, Algebra.lsmul_coe]

Premises used: Module.End.smul_def, Algebra.pushoutDesc_right, Algebra.lsmul_coe
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
h :
  ∀ (r : S) (x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
    HSMul.hSMul (α := B) ((algebraMap S B : (a : S) → B) r : B) x = r • x
⊢ IsScalarTower S B (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
apply IsScalarTower.of_algebraMap_smul

Premises used: IsScalarTower.of_algebraMap_smul