Improving proofs about `symmDiff`

Stream: new members

[Bbbbbbbbba]

This is not that bad but I do feel that I am missing something about symmDiff or about parity logic. I am open to changing the definition of Context.boundary to use Odd _ in place of _ % 2 = 1 if it leads to a nicer proof.

import Mathlib

open Set symmDiff

variable {V E : Type*}

structure Context (V E : Type*) where
  incidence : E → Set V
  weight : E → ℝ
  weight_nonneg : ∀ e, 0 ≤ weight e

variable {ctx : Context V E}

def Context.boundary (C : Set E) : Set V := {v | {e ∈ C | v ∈ ctx.incidence e}.ncard % 2 = 1}

variable [Finite E]

lemma boundary_symmDiff (A B : Set E) :
    ctx.boundary (A ∆ B) = (ctx.boundary A) ∆ (ctx.boundary B) := by
  ext v
  simp only [Context.boundary, mem_symmDiff]
  set Av := {e ∈ A | v ∈ ctx.incidence e}
  set Bv := {e ∈ B | v ∈ ctx.incidence e}
  have h_split : {e | (e ∈ A ∧ e ∉ B ∨ e ∈ B ∧ e ∉ A) ∧ v ∈ ctx.incidence e} =
      (Av ∪ Bv) \ (Av ∩ Bv) := by ext e; simp [Av, Bv]; tauto
  have h_symm_diff : ((Av ∪ Bv) \ (Av ∩ Bv)).ncard + 2 * (Av ∩ Bv).ncard = Av.ncard + Bv.ncard := by
    rw [← (ncard_union_add_ncard_inter Av Bv), two_mul, ← add_assoc, ncard_diff_add_ncard_of_subset]
    exact fun e he ↦ Or.inl he.1
  have h_symm_diff : ((Av ∪ Bv) \ (Av ∩ Bv)).ncard % 2 = (Av.ncard + Bv.ncard) % 2 := by
    rw [← h_symm_diff]; simp
  simp [h_split, h_symm_diff, Av, Bv]; omega