∀ {R : Type u_4} {ι : Type u_5} {A : Type u_1} {B : Type u_2} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {C : Type u_3} [inst_10 : Ring C] [inst_11 : Algebra R C]
  (fg : { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) }),
  (fun F => ⟨(F.comp (GradedTensorProduct.includeLeft 𝒜 ℬ), F.comp (GradedTensorProduct.includeRight 𝒜 ℬ)), ⋯⟩)
      ((fun fg => GradedTensorProduct.lift 𝒜 ℬ (↑fg).1 (↑fg).2 ⋯) fg) =
    fg