∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  {σ : Type u_4} {κ : Type u_5} (P : Algebra.Generators R S ι) {u : σ → ι} (hu : Function.Injective u) {v : κ → ι},
  IsCompl (Set.range v) (Set.range u) →
    Submodule.span S (Set.range fun i => (KaehlerDifferential.D R S) (P.val (v i))) = ⊤ →
      Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x => P.cotangentSpaceBasis (v x))) →
        ∀ [Subsingleton (Algebra.H1Cotangent R S)], Function.Bijective ⇑(P.cotangentRestrict hu)