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
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this :
  HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0
⊢ a * b -
        HMul.hMul (α := P) (β := P) ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P)
          ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) -
      (a * b - HMul.hMul (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) +
        (b * a - HMul.hMul (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P))) =
    HMul.hMul (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) -
        HMul.hMul (α := P) (β := P) ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P)
          ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) -
      (a * b - HMul.hMul (α := P) ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) b)

Tactic:
ring
-- 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
smul_assoc : ∀ (x : P) (y : S) (z : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))), (x • y) • z = x • y • z
⊢ IsScalarTower P S ↥(RingHom.ker (F := P →+* S) (algebraMap P S))

Tactic:
constructor
-- 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
smul_assoc : (↑((p • s) • m) : P) = (↑(p • s • m) : P)
⊢ (p • s) • m = p • s • m

Tactic:
ext
-- 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
smul_assoc :
  HMul.hMul (α := P) ((g : (a : S) → P) (p • s) : P) (↑m : P) =
    p * HMul.hMul (α := P) ((g : (a : S) → P) s : P) (↑m : P)
⊢ (↑((p • s) • m) : P) = (↑(p • s • m) : P)

Tactic:
change g (p • s) * m = p * (g s * m)

Premises used: HMul.hMul, HSMul.hSMul, Subtype.val, 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
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
smul_assoc :
  HMul.hMul (α := P) ((g : (a : S) → P) s : P)
      (HMul.hMul (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) (↑m : P)) =
    HMul.hMul (α := P) ((g : (a : S) → P) s : P) (p * (↑m : P))
⊢ HMul.hMul (α := P) ((g : (a : S) → P) (p • s) : P) (↑m : P) =
    p * HMul.hMul (α := P) ((g : (a : S) → P) s : P) (↑m : P)

Tactic:
simp only [Algebra.smul_def, map_mul, mul_assoc, mul_left_comm _ (g s)]

Premises used: mul_assoc, mul_left_comm, map_mul, Algebra.smul_def, 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
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
smul_assoc : HMul.hMul (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) (↑m : P) = p * (↑m : P)
⊢ HMul.hMul (α := P) ((g : (a : S) → P) s : P)
      (HMul.hMul (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) (↑m : P)) =
    HMul.hMul (α := P) ((g : (a : S) → P) s : P) (p * (↑m : P))

Tactic:
congr 1
-- 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
smul_assoc :
  HSub.hSub (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) p * (↑m : P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ HMul.hMul (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) (↑m : P) = p * (↑m : P)

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

Premises used: Ideal.mem_bot, pow_two, sub_eq_zero, 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ HSub.hSub (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) p * (↑m : 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 ?_ m.2

Premises used: Set.Mem, Ideal.mul_mem_mul, 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
smul_assoc :
  Membership.mem (γ := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S))
    (HSub.hSub (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) p)
⊢ HSub.hSub (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) p * (↑m : P) ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))

Tactic:
refine Ideal.mul_mem_mul ?_ m.2

Premises used: Ideal.mul_mem_mul, 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
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Membership.mem (γ := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S))
    (HSub.hSub (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) p)

Tactic:
simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg (algebraMap P S p)

Premises used: Algebra.algebraMap, sub_eq_zero, RingHom.mem_ker, AlgHom.congr_fun, 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
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
h :
  ∀ (x : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))),
    Eq.{u_2 + 1} (α := P)
      (↑((retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S :
              (a : ↥(RingHom.ker (algebraMap P S))) → ↥(RingHom.ker (algebraMap P S)))
            x) :
        P)
      (↑((LinearMap.id : (a : ↥(RingHom.ker (algebraMap P S))) → ↥(RingHom.ker (algebraMap P S))) x) : P)
⊢ retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S = LinearMap.id

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
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
g : S →ₐ[R] P
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hg : AlgHom.comp (IsScalarTower.toAlgHom R P S) g = AlgHom.id R S
x : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Eq.{u_2 + 1} (α := P)
    (↑((retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S :
            (a : ↥(RingHom.ker (algebraMap P S))) → ↥(RingHom.ker (algebraMap P S)))
          x) :
      P)
    (↑((LinearMap.id : (a : ↥(RingHom.ker (algebraMap P S))) → ↥(RingHom.ker (algebraMap P S))) x) : P)

Tactic:
simp [RingHom.mem_ker.mp x.2]

Premises used: RingHom.mem_ker, Iff.mp, 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
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) x : S) ((algebraMap P S : (a : P) → S) y : S)
rw :
  x - y =
    (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (x - y))) : P)
⊢ x - (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) x)) : P) =
    y - (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) y)) : P)

Tactic:
rw [sub_eq_iff_eq_add, sub_add_comm, ← sub_eq_iff_eq_add, ← Submodule.coe_sub,
    ← map_sub, ← tmul_sub, ← map_sub]

Premises used: map_sub, TensorProduct.tmul_sub, Submodule.coe_sub, sub_eq_iff_eq_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
x y : P
h : Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) x : S) ((algebraMap P S : (a : P) → S) y : S)
⊢ Membership.mem (γ := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (x - y)

Tactic:
simp [RingHom.mem_ker, h]

Premises used: RingHom.mem_ker
-- 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
x y : P
h : Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) x : S) ((algebraMap P S : (a : P) → S) y : S)
⊢ x - y =
    (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (x - y))) : P)

Tactic:
exact congr_arg Subtype.val (LinearMap.congr_fun hl.symm ⟨x - y, by simp [RingHom.mem_ker, h]⟩)

Premises used: HSub.hSub, Subtype.mk, congr_arg, LinearMap.congr_fun, Eq.symm, Subtype.val
-- 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 = ⊥
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) (σ 1) : S) ((algebraMap P S : (a : P) → S) 1 : 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 = ⊥
⊢ σ 1 -
      (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ 1))) : P) =
    1

Tactic:
simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 1) 1 (by simp [hσ])]

Premises used: sectionOfRetractionKerToTensorAux_prop, OfNat.ofNat
-- 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
x y : S ⊗[P] Ω[P⁄R]
rw :
  HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
      (↑((l : (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 : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
      (↑((l : (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
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
x y : S ⊗[P] Ω[P⁄R]
⊢ HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
      (↑((l : (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 x).2 (l y).2

Premises used: Set.Mem, Ideal.mul_mem_mul, 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
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
x y : S ⊗[P] Ω[P⁄R]
⊢ HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
      (↑((l : (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 x).2 (l y).2

Premises used: Ideal.mul_mem_mul, 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
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
⊢ ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) y) : P) =
      0

Tactic:
have (x y : _) : (l x).1 * (l y).1 = 0 := by
      rw [← Ideal.mem_bot, ← hf', pow_two]; exact Ideal.mul_mem_mul (l x).2 (l 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
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
this :
  ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) y) : P) =
      0
⊢ 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
this :
  ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) y) : P) =
      0
simp :
  σ a * σ b -
      (σ a *
          (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ b))) :
            P) +
        σ b *
          (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ a))) :
            P)) =
    σ a * σ b -
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ a))) :
            P) *
          σ b -
      σ a *
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ b))) : P)
⊢ σ (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σ]),
      Derivation.leibniz, tmul_add, tmul_smul, map_add, map_smul, Submodule.coe_add,
      SetLike.val_smul, smul_eq_mul, mul_sub, sub_mul, this, sub_zero]

Premises used: Submodule.coe_add, HMul.hMul, mul_sub, sub_zero, TensorProduct.tmul_smul, map_add, sectionOfRetractionKerToTensorAux_prop, Derivation.leibniz, sub_mul, SetLike.val_smul, TensorProduct.tmul_add, smul_eq_mul, map_smul
-- 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
this :
  ∀ (x y : S ⊗[P] Ω[P⁄R]),
    HMul.hMul (α := P) (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) x) : P)
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) y) : P) =
      0
⊢ σ a * σ b -
      (σ a *
          (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ b))) :
            P) +
        σ b *
          (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ a))) :
            P)) =
    σ a * σ b -
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ a))) :
            P) *
          σ b -
      σ a *
        (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ b))) : P)

Tactic:
ring
-- 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 = ⊥
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap P S : (a : P) → S) (σ 0) : S) ((algebraMap P S : (a : P) → S) 0 : 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 = ⊥
⊢ σ 0 -
      (↑((l : (a : S ⊗[P] Ω[P⁄R]) → ↥(RingHom.ker (algebraMap P S))) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (σ 0))) : P) =
    0

Tactic:
simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 0) 0 (by simp [hσ])]

Premises used: sectionOfRetractionKerToTensorAux_prop, OfNat.ofNat