∀ {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} [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] [inst_5 : SizeOf ι] [inst_6 : SizeOf σ] (f : P.toExtension.Cotangent → ↥P.toExtension.ker)
  (hf : ∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f b) = b) (g : P.Ring) (hgmem : g - 1 ∈ P.ker)
  (hg : g • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f ∘ ⇑b))),
  sizeOf { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg } = 1 + sizeOf g + sizeOf hgmem