awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
a b : S
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) (σ (a + b)) : S)
    ((algebraMap P S : (a : P) → S) (σ a + σ b) : S)

Tactic:
simp [hσ]
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
a b : S
⊢ σ (a + b) -
      (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ (a + b)))) :
        P) =
    σ a -
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ a))) :
          P) +
      (σ b -
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ b))) : P))

Tactic:
simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a + b)) (σ a + σ b) (by simp [hσ]),
      map_add, tmul_add, Submodule.coe_add, add_sub_add_comm]

Premises used: Submodule.coe_add, map_add, sectionOfRetractionKerToTensorAux_prop, HAdd.hAdd, TensorProduct.tmul_add, add_sub_add_comm
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
r : R
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) (σ ((algebraMap R S : (a : R) → S) r)) : S)
    ((algebraMap P S : (a : P) → S) ((algebraMap R P : (a : R) → P) r : P) : S)

Tactic:
simp [hσ, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
r : R
⊢ σ ((algebraMap R S : (a : R) → S) r) -
      (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ ((algebraMap R S : (a : R) → S) r)))) :
        P) =
    (algebraMap R P : (a : R) → P) r

Tactic:
simp [sectionOfRetractionKerToTensorAux_prop l hl
      (σ (algebraMap R S r)) (algebraMap R P r) (by simp [hσ, ← IsScalarTower.algebraMap_apply])]

Premises used: Algebra.algebraMap, sectionOfRetractionKerToTensorAux_prop, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
x : P
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) (σ ((algebraMap P S : (a : P) → S) x)) : S)
    ((algebraMap P S : (a : P) → S) x : S)

Tactic:
simp [hσ]
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
H :
  ∀ (x : S),
    Eq (α := S)
      ((AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensorAux l hl σ hσ hf') : (a : S) → S) x :
        S)
      ((AlgHom.id R S : (a : S) → S) x : S)
⊢ Eq (α := S →ₐ[R] S) (AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensorAux l hl σ hσ hf'))
    (AlgHom.id R S)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
x : S
H :
  ∀ (x : P),
    Eq (α := S)
      ((AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensorAux l hl σ hσ hf') : (a : S) → S)
          ((algebraMap P S : (a : P) → S) x : S) :
        S)
      ((AlgHom.id R S : (a : S) → S) ((algebraMap P S : (a : P) → S) x : S) : S)
⊢ Eq (α := S)
    ((AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensorAux l hl σ hσ hf') : (a : S) → S) x : S)
    ((AlgHom.id R S : (a : S) → S) x : S)

Tactic:
obtain ⟨x, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S : (a : P) → S) (σ x) = x
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
x : P
⊢ Eq (α := S)
    ((AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensorAux l hl σ hσ hf') : (a : S) → S)
        ((algebraMap P S : (a : P) → S) x : S) :
      S)
    ((AlgHom.id R S : (a : S) → S) ((algebraMap P S : (a : P) → S) x : S) : S)

Tactic:
simp [sectionOfRetractionKerToTensorAux_algebraMap, RingHom.mem_ker.mp]

Premises used: RingHom.mem_ker, Iff.mp, sectionOfRetractionKerToTensorAux_algebraMap
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
x : P
⊢ (sectionOfRetractionKerToTensor l hl hf' hf : (a : S) → P) ((algebraMap P S : (a : P) → S) x : S) =
    x - (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) x)) : P)

Tactic:
sectionOfRetractionKerToTensorAux_algebraMap l hl _ _ hf' x

Premises used: sectionOfRetractionKerToTensorAux_algebraMap
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
⊢ Eq (α := S →ₐ[R] S) (AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensor l hl hf' hf))
    (AlgHom.id R S)

Tactic:
toAlgHom_comp_sectionOfRetractionKerToTensorAux (hf := hf) ..

Premises used: sectionOfRetractionKerToTensor, toAlgHom_comp_sectionOfRetractionKerToTensorAux
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
rw :
  HMul.hMul (α := P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            x) :
        P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            y) :
        P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ HMul.hMul (α := P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            x) :
        P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            y) :
        P) =
    0

Tactic:
rw [← Ideal.mem_bot, ← hf', pow_two]

Premises used: Ideal.mem_bot, pow_two
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
⊢ HMul.hMul (α := P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            x) :
        P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            y) :
        P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))

Tactic:
Ideal.mul_mem_mul (l.1 x).2 (l.1 y).2

Premises used: Set.Mem, Ideal.mul_mem_mul, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
⊢ HMul.hMul (α := P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            x) :
        P)
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            y) :
        P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))

Tactic:
exact Ideal.mul_mem_mul (l.1 x).2 (l.1 y).2

Premises used: Ideal.mul_mem_mul, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
⊢ ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              x) :
          P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              y) :
          P) =
      0

Tactic:
have (x y : _) : (l.1 x).1 * (l.1 y).1 = 0 := by
      rw [← Ideal.mem_bot, ← hf', pow_two]; exact Ideal.mul_mem_mul (l.1 x).2 (l.1 y).2
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
this :
  ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              x) :
          P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              y) :
          P) =
      0
a :
  s *
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
          P) -
      HMul.hMul (α := P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) s)) :
          P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
          P) =
    (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
            (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
          ((algebraMap P S : (a : P) → S) s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
      P)
⊢ (s -
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) s)) :
          P)) *
      (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
              (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
            (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
        P) =
    (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
            (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
          ((algebraMap P S : (a : P) → S) s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
      P)

Tactic:
rw [sub_mul]

Premises used: sub_mul
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
l : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
this :
  ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              x) :
          P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              y) :
          P) =
      0
⊢ s *
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
          P) -
      HMul.hMul (α := P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) s)) :
          P)
        (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
                (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
              (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
          P) =
    (↑(((↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) :
            (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S)))
          ((algebraMap P S : (a : P) → S) s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) p)) :
      P)

Tactic:
simp only [this, Algebra.algebraMap_eq_smul_one, ← smul_tmul', LinearMapClass.map_smul,
      SetLike.val_smul, smul_eq_mul, sub_zero]

Premises used: sub_zero, Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul', SetLike.val_smul, LinearMapClass.map_smul, smul_eq_mul
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
g : { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }
a :
  ∀ (s : S),
    Eq.{u_2 + 1} (α := P)
      (((↑((fun
                      (l :
                        { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
                          l ∘ₗ kerToTensor R P S = LinearMap.id }) ↦
                    (Subtype.mk (p := fun (g : S →ₐ[R] P) ↦
                        AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S)
                        (sectionOfRetractionKerToTensor (↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) ⋯ hf'
                          hf)
                        ⋯ :
                      { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }))
                  ((fun (g : { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }) ↦
                      (Subtype.mk (p := fun (l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) ↦
                          l ∘ₗ kerToTensor R P S = LinearMap.id) (retractionOfSectionOfKerSqZero (↑g : S →ₐ[R] P) hf' ⋯)
                          ⋯ :
                        { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
                          l ∘ₗ kerToTensor R P S = LinearMap.id }))
                    g)) :
              S →ₐ[R] P) :
            (a : S) → P)
          s :
        P)
      (((↑g : S →ₐ[R] P) : (a : S) → P) s : P)
⊢ (fun
          (l :
            { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
              l ∘ₗ kerToTensor R P S = LinearMap.id }) ↦
        (Subtype.mk (p := fun (g : S →ₐ[R] P) ↦ AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S)
            (sectionOfRetractionKerToTensor (↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) ⋯ hf' hf) ⋯ :
          { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }))
      ((fun (g : { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }) ↦
          (Subtype.mk (p := fun (l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) ↦
              l ∘ₗ kerToTensor R P S = LinearMap.id) (retractionOfSectionOfKerSqZero (↑g : S →ₐ[R] P) hf' ⋯) ⋯ :
            { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
              l ∘ₗ kerToTensor R P S = LinearMap.id }))
        g) =
    g

Tactic:
ext s
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
g : { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }
s : P
⊢ Eq.{u_2 + 1} (α := P)
    (((↑((fun
                    (l :
                      { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
                        l ∘ₗ kerToTensor R P S = LinearMap.id }) ↦
                  (Subtype.mk (p := fun (g : S →ₐ[R] P) ↦ AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S)
                      (sectionOfRetractionKerToTensor (↑l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) ⋯ hf'
                        hf)
                      ⋯ :
                    { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }))
                ((fun (g : { g : S →ₐ[R] P // AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S }) ↦
                    (Subtype.mk (p := fun (l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) ↦
                        l ∘ₗ kerToTensor R P S = LinearMap.id) (retractionOfSectionOfKerSqZero (↑g : S →ₐ[R] P) hf' ⋯)
                        ⋯ :
                      { l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) //
                        l ∘ₗ kerToTensor R P S = LinearMap.id }))
                  g)) :
            S →ₐ[R] P) :
          (a : S) → P)
        ((algebraMap P S : (a : P) → S) s : S) :
      P)
    (((↑g : S →ₐ[R] P) : (a : S) → P) ((algebraMap P S : (a : P) → S) s : S) : P)

Tactic:
simp