∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (P₁ : Algebra.Extension R A) (P₂ : Algebra.Extension R A) [inst_3 : Algebra.FormallySmooth R P₁.Ring],
  ∀ a ∈ P₁.ker ^ 2,
    (Algebra.FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
          (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯)
        a =
      0