no goals
F : Type u_1
inst✝¹ : Field F
ι : Type ?u.84878
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = 1
classical rw [
  ← sum_basis (Set.injOn_of_injective Function.injective_id _) ⟨x, mem_insert_self _ {y}⟩,
  sum_insert (not_mem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
  basis_pair_right hxy, id, id]
no goals
F : Type u_1
inst✝¹ : Field F
ι : Type ?u.84878
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = 1
rw [
← sum_basis (Set.injOn_of_injective Function.injective_id _) ⟨x, mem_insert_self _ {y}⟩,
sum_insert (not_mem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
basis_pair_right hxy, id, id]