{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (f : P.toExtension.Cotangent → ↥P.toExtension.ker) →
                    (∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f b) = b) →
                      (g : P.Ring) →
                        g - 1 ∈ P.ker →
                          g • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f ∘ ⇑b)) →
                            Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b