{R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {S : Type u_3} →
            [inst_3 : CommRing S] →
              [inst_4 : Algebra R S] →
                (I : Ideal S) → (A →ₐ[R] S ⧸ I) → [Algebra.FormallySmooth R A] → (m : ℕ) → A →ₐ[R] S ⧸ I ^ m