feat(order/symm_diff): The symmetric difference is involutive (#14959)

`a ∆ (a ∆ b) = b` and `b ∆ a ∆ a = b`.

Author: YaelDillies

src/order/symm_diff.lean

@@ -21,6 +21,7 @@ The symmetric difference is the addition operator in the Boolean ring structure
 ## Main declarations
 
 * `symm_diff`: the symmetric difference operator, defined as `(A \ B) ⊔ (B \ A)`
+* `equiv.symm_diff`: Symmetric difference by `a` as an `equiv`.
 
 In generalized Boolean algebras, the symmetric difference operator is:
 
@@ -42,6 +43,8 @@ Proof from the Book" by John McCuan:
 boolean ring, generalized boolean algebra, boolean algebra, symmetric differences
 -/
 
+open function
+
 /-- The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`. -/
 def symm_diff {α : Type*} [has_sup α] [has_sdiff α] (A B : α) : α := (A \ B) ⊔ (B \ A)
 
@@ -151,6 +154,12 @@ calc a ∆ (b ∆ c) = (a \ (b ∆ c)) ⊔ ((b ∆ c) \ a) : symm_diff_def _ _
              ... = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔
                      (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c)   : by ac_refl
 
+@[simp] lemma symm_diff_symm_diff_inf : a ∆ b ∆ (a ⊓ b) = a ⊔ b :=
+by rw [symm_diff_eq_iff_sdiff_eq (symm_diff_le_sup _ _), sup_sdiff_symm_diff]
+
+@[simp] lemma inf_symm_diff_symm_diff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b :=
+by rw [symm_diff_comm, symm_diff_symm_diff_inf]
+
 lemma symm_diff_assoc : a ∆ b ∆ c = a ∆ (b ∆ c) :=
 by rw [symm_diff_symm_diff_left, symm_diff_symm_diff_right]
 
@@ -164,21 +173,26 @@ lemma symm_diff_right_comm : a ∆ b ∆ c = a ∆ c ∆ b := by simp_rw [symm_d
 lemma symm_diff_symm_diff_symm_diff_comm : (a ∆ b) ∆ (c ∆ d) = (a ∆ c) ∆ (b ∆ d) :=
 by simp_rw [symm_diff_assoc, symm_diff_left_comm]
 
-@[simp] lemma symm_diff_symm_diff_self : a ∆ (a ∆ b) = b := by simp [←symm_diff_assoc]
+@[simp] lemma symm_diff_symm_diff_cancel_left : a ∆ (a ∆ b) = b := by simp [←symm_diff_assoc]
+@[simp] lemma symm_diff_symm_diff_cancel_right : b ∆ a ∆ a = b := by simp [symm_diff_assoc]
 
 @[simp] lemma symm_diff_symm_diff_self' : a ∆ b ∆ a = b :=
-by rw [symm_diff_comm, ←symm_diff_assoc, symm_diff_self, bot_symm_diff]
+by rw [symm_diff_comm,symm_diff_symm_diff_cancel_left]
+
+lemma symm_diff_left_involutive (a : α) : involutive (∆ a) := symm_diff_symm_diff_cancel_right _
+lemma symm_diff_right_involutive (a : α) : involutive ((∆) a) := symm_diff_symm_diff_cancel_left _
+lemma symm_diff_left_injective (a : α) : injective (∆ a) := (symm_diff_left_involutive _).injective
+lemma symm_diff_right_injective (a : α) : injective ((∆) a) :=
+(symm_diff_right_involutive _).injective
+lemma symm_diff_left_surjective (a : α) : surjective (∆ a) :=
+(symm_diff_left_involutive _).surjective
+lemma symm_diff_right_surjective (a : α) : surjective ((∆) a) :=
+(symm_diff_right_involutive _).surjective
 
-@[simp] lemma symm_diff_right_inj : a ∆ b = a ∆ c ↔ b = c :=
-begin
-  split; intro h,
-  { have H1 := congr_arg ((∆) a) h,
-    rwa [symm_diff_symm_diff_self, symm_diff_symm_diff_self] at H1, },
-  { rw h, },
-end
+variables {a b c}
 
-@[simp] lemma symm_diff_left_inj : a ∆ b = c ∆ b ↔ a = c :=
-by rw [symm_diff_comm a b, symm_diff_comm c b, symm_diff_right_inj]
+@[simp] lemma symm_diff_left_inj : a ∆ b = c ∆ b ↔ a = c := (symm_diff_left_injective _).eq_iff
+@[simp] lemma symm_diff_right_inj : a ∆ b = a ∆ c ↔ b = c := (symm_diff_right_injective _).eq_iff
 
 @[simp] lemma symm_diff_eq_left : a ∆ b = a ↔ b = ⊥ :=
 calc a ∆ b = a ↔ a ∆ b = a ∆ ⊥ : by rw symm_diff_bot
@@ -190,14 +204,6 @@ calc a ∆ b = a ↔ a ∆ b = a ∆ ⊥ : by rw symm_diff_bot
 calc a ∆ b = ⊥ ↔ a ∆ b = a ∆ a : by rw symm_diff_self
            ... ↔     a = b     : by rw [symm_diff_right_inj, eq_comm]
 
-@[simp] lemma symm_diff_symm_diff_inf : a ∆ b ∆ (a ⊓ b) = a ⊔ b :=
-by rw [symm_diff_eq_iff_sdiff_eq (symm_diff_le_sup _ _), sup_sdiff_symm_diff]
-
-@[simp] lemma inf_symm_diff_symm_diff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b :=
-by rw [symm_diff_comm, symm_diff_symm_diff_inf]
-
-variables {a b c}
-
 protected lemma disjoint.symm_diff_left (ha : disjoint a c) (hb : disjoint b c) :
   disjoint (a ∆ b) c :=
 by { rw symm_diff_eq_sup_sdiff_inf, exact (ha.sup_left hb).disjoint_sdiff_left }