∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (toFun : ι → P) (ind' : AffineIndependent k toFun)
  (tot' : affineSpan k (Set.range toFun) = ⊤) (toFun_1 : ι → P) (ind'_1 : AffineIndependent k toFun_1)
  (tot'_1 : affineSpan k (Set.range toFun_1) = ⊤),
  ({ toFun := toFun, ind' := ind', tot' := tot' } = { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 }) =
    (toFun = toFun_1)