awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ (↑(({
                toFun := fun (x : P) ↦
                  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                    (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
              (a : P) → ↥(RingHom.ker f))
            (a * b)) :
        P) -
      (↑(HSMul.hSMul (β := ↥(RingHom.ker f)) a
              (({
                      toFun := fun (x : P) ↦
                        Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                          (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                    (a : P) → ↥(RingHom.ker f))
                  b :
                ↥(RingHom.ker f)) +
            HSMul.hSMul (β := ↥(RingHom.ker f)) b
              (({
                      toFun := fun (x : P) ↦
                        Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                          (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                    (a : P) → ↥(RingHom.ker f))
                  a :
                ↥(RingHom.ker f))) :
        P) =
    -(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))
have a₁ : 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: simp only [LinearMap.coe_mk, AddHom.coe_mk, map_mul, SetLike.mk_smul_mk, smul_eq_mul, mul_sub,
      AddMemClass.mk_add_mk, sub_mul, neg_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ IsScalarTower P S ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
have smul_assoc : ∀ (x : P) (y : S) (z : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))), (x • y) • z = x • y • z
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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))
⊢ (p • s) • m = p • s • m
have smul_assoc : (↑((p • s) • m) : P) = (↑(p • s • m) : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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))
⊢ (↑((p • s) • m) : P) = (↑(p • s • m) : P)
have 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)
Tactic: change g (p • s) * m = p * (g s * m)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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))
⊢ HMul.hMul (α := P) ((g : (a : S) → P) (p • s) : P) (↑m : P) =
    p * HMul.hMul (α := P) ((g : (a : S) → P) s : P) (↑m : P)
have 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))
Tactic: simp only [Algebra.smul_def, map_mul, mul_assoc, mul_left_comm _ (g s)]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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))
⊢ 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))
have smul_assoc : HMul.hMul (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) (↑m : P) = p * (↑m : P)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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))
⊢ HMul.hMul (α := P) ((g : (a : S) → P) ((algebraMap P S : (a : P) → S) p : S) : P) (↑m : P) = p * (↑m : P)
have 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))
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← hf', pow_two, ← sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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))
have 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)
Tactic: refine Ideal.mul_mem_mul ?_ m.2
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S = LinearMap.id
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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 - (↑((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)
have 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)
Tactic: rw [sub_eq_iff_eq_add, sub_add_comm, ← sub_eq_iff_eq_add, ← Submodule.coe_sub,
    ← map_sub, ← tmul_sub, ← map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
have 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))
Tactic: rw [← Ideal.mem_bot, ← hf', pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
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))
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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) -
      (↑((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))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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)
⊢ Eq (α := S →ₐ[R] S) (AlgHom.comp (IsScalarTower.toAlgHom R P S) (sectionOfRetractionKerToTensorAux l hl σ hσ hf'))
    (AlgHom.id R S)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨x, rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
have 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))
Tactic: rw [← Ideal.mem_bot, ← hf', pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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]) 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)
have 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)
Tactic: rw [sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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 }
⊢ (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
have 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))) sorry hf'
                        hf)
                      sorry :
                    { 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' sorry)
                        sorry :
                      { 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)
Tactic: ext s