∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  P.toInfinitesimal =
    { toRingHom := Ideal.Quotient.mk (P.ker ^ 2), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }