feat(order/symm_diff): More symmetric difference lemmas (#13133)

A few more `symm_diff` lemmas.

Co-authored-by: Bryan Gin-ge Chen

src/order/boolean_algebra.lean

@@ -123,25 +123,6 @@ begin
   exact (eq_of_inf_eq_sup_eq i s).symm,
 end
 
-theorem sdiff_symm (hy : y ≤ x) (hz : z ≤ x) (H : x \ y = z) : x \ z = y :=
-have hyi : x ⊓ y = y := inf_eq_right.2 hy,
-have hzi : x ⊓ z = z := inf_eq_right.2 hz,
-eq_of_inf_eq_sup_eq
-  (begin
-    have ixy := inf_inf_sdiff x y,
-    rw [H, hyi] at ixy,
-    have ixz := inf_inf_sdiff x z,
-    rwa [hzi, inf_comm, ←ixy] at ixz,
-  end)
-  (begin
-    have sxz := sup_inf_sdiff x z,
-    rw [hzi, sup_comm] at sxz,
-    rw sxz,
-    symmetry,
-    have sxy := sup_inf_sdiff x y,
-    rwa [H, hyi] at sxy,
-  end)
-
 lemma sdiff_le : x \ y ≤ x :=
 calc x \ y ≤ (x ⊓ y) ⊔ (x \ y) : le_sup_right
        ... = x                 : sup_inf_sdiff x y
@@ -372,6 +353,8 @@ lemma sdiff_le_iff : y \ x ≤ z ↔ y ≤ x ⊔ z :=
               ... ≤ (x ⊔ z) ⊔ x : sup_le_sup_right h x
               ... ≤ z ⊔ x       : by rw [sup_assoc, sup_comm, sup_assoc, sup_idem])⟩
 
+lemma sdiff_sdiff_le : x \ (x \ y) ≤ y := sdiff_le_iff.2 le_sdiff_sup
+
 @[simp] lemma le_sdiff_iff : x ≤ y \ x ↔ x = ⊥ :=
 ⟨λ h, disjoint_self.1 (disjoint_sdiff_self_right.mono_right h), λ h, h.le.trans bot_le⟩
 
@@ -442,12 +425,22 @@ calc  x \ (y \ z) = (x \ y) ⊔ (x ⊓ y ⊓ z) : sdiff_sdiff_right
               ... = z ⊓ x ⊓ y ⊔ (x \ y)   : by ac_refl
               ... = (x \ y) ⊔ (x ⊓ z)     : by rw [sup_inf_inf_sdiff, sup_comm, inf_comm]
 
+lemma sdiff_sdiff_eq_sdiff_sup (h : z ≤ x) : x \ (y \ z) = x \ y ⊔ z :=
+by rw [sdiff_sdiff_right', inf_eq_right.2 h]
+
 @[simp] lemma sdiff_sdiff_right_self : x \ (x \ y) = x ⊓ y :=
 by rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
 
 lemma sdiff_sdiff_eq_self (h : y ≤ x) : x \ (x \ y) = y :=
 by rw [sdiff_sdiff_right_self, inf_of_le_right h]
 
+lemma sdiff_eq_symm (hy : y ≤ x) (h : x \ y = z) : x \ z = y := by rw [←h, sdiff_sdiff_eq_self hy]
+lemma sdiff_eq_comm (hy : y ≤ x) (hz : z ≤ x) : x \ y = z ↔ x \ z = y :=
+⟨sdiff_eq_symm hy, sdiff_eq_symm hz⟩
+
+lemma eq_of_sdiff_eq_sdiff (hxz : x ≤ z) (hyz : y ≤ z) (h : z \ x = z \ y) : x = y :=
+by rw [←sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]
+
 lemma sdiff_sdiff_left : (x \ y) \ z = x \ (y ⊔ z) :=
 begin
   rw sdiff_sup,
@@ -528,6 +521,19 @@ sdiff_unique
   (calc x ⊓ y ⊓ z ⊓ (x ⊓ (y \ z)) = x ⊓ x ⊓ ((y ⊓ z) ⊓ (y \ z)) : by ac_refl
                               ... = ⊥                           : by rw [inf_inf_sdiff, inf_bot_eq])
 
+lemma inf_sdiff_right_comm : x \ z ⊓ y = (x ⊓ y) \ z :=
+by rw [@inf_comm _ _ x, inf_comm, inf_sdiff_assoc]
+
+lemma inf_sdiff_distrib_left (a b c : α) : a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c) :=
+by rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
+
+lemma inf_sdiff_distrib_right (a b c : α) : a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c) :=
+by simp_rw [@inf_comm _ _ _ c, inf_sdiff_distrib_left]
+
+lemma sdiff_sup_sdiff_cancel (hyx : y ≤ x) (hzy : z ≤ y) : x \ y ⊔ y \ z = x \ z :=
+by rw [←sup_sdiff_inf (x \ z) y, sdiff_sdiff_left, sup_eq_right.2 hzy, inf_sdiff_right_comm,
+  inf_eq_right.2 hyx]
+
 lemma sup_eq_sdiff_sup_sdiff_sup_inf : x ⊔ y = (x \ y) ⊔ (y \ x) ⊔ (x ⊓ y) :=
 eq.symm $
   calc (x \ y) ⊔ (y \ x) ⊔ (x ⊓ y) =

src/order/lattice.lean

@@ -243,6 +243,12 @@ by rw [sup_assoc, sup_assoc, @sup_comm _ _ b]
 lemma sup_sup_sup_comm (a b c d : α) : a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d) :=
 by rw [sup_assoc, sup_left_comm b, ←sup_assoc]
 
+lemma sup_sup_distrib_left (a b c : α) : a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ (a ⊔ c) :=
+by rw [sup_sup_sup_comm, sup_idem]
+
+lemma sup_sup_distrib_right (a b c : α) : (a ⊔ b) ⊔ c = (a ⊔ c) ⊔ (b ⊔ c) :=
+by rw [sup_sup_sup_comm, sup_idem]
+
 lemma forall_le_or_exists_lt_sup (a : α) : (∀b, b ≤ a) ∨ (∃b, a < b) :=
 suffices (∃b, ¬b ≤ a) → (∃b, a < b),
   by rwa [or_iff_not_imp_left, not_forall],
@@ -417,6 +423,12 @@ lemma inf_right_comm (a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b :=
 lemma inf_inf_inf_comm (a b c d : α) : a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d) :=
 @sup_sup_sup_comm (order_dual α) _ _ _ _ _
 
+lemma inf_inf_distrib_left (a b c : α) : a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ (a ⊓ c) :=
+@sup_sup_distrib_left (order_dual α) _ _ _ _
+
+lemma inf_inf_distrib_right (a b c : α) : (a ⊓ b) ⊓ c = (a ⊓ c) ⊓ (b ⊓ c) :=
+@sup_sup_distrib_right (order_dual α) _ _ _ _
+
 lemma forall_le_or_exists_lt_inf (a : α) : (∀b, a ≤ b) ∨ (∃b, b < a) :=
 @forall_le_or_exists_lt_sup (order_dual α) _ a
 

src/order/symm_diff.lean

@@ -67,6 +67,9 @@ instance symm_diff_is_comm : is_commutative α (Δ) := ⟨symm_diff_comm⟩
 lemma symm_diff_eq_sup_sdiff_inf : a Δ b = (a ⊔ b) \ (a ⊓ b) :=
 by simp [sup_sdiff, sdiff_inf, sup_comm, (Δ)]
 
+@[simp] lemma sup_sdiff_symm_diff : (a ⊔ b) \ (a Δ b) = a ⊓ b :=
+sdiff_eq_symm inf_le_sup (by rw symm_diff_eq_sup_sdiff_inf)
+
 lemma disjoint_symm_diff_inf : disjoint (a Δ b) (a ⊓ b) :=
 begin
   rw [symm_diff_eq_sup_sdiff_inf],
@@ -75,6 +78,13 @@ end
 
 lemma symm_diff_le_sup : a Δ b ≤ a ⊔ b := by { rw symm_diff_eq_sup_sdiff_inf, exact sdiff_le }
 
+lemma inf_symm_diff_distrib_left : a ⊓ (b Δ c) = (a ⊓ b) Δ (a ⊓ c) :=
+by rw [symm_diff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
+  symm_diff_eq_sup_sdiff_inf]
+
+lemma inf_symm_diff_distrib_right : (a Δ b) ⊓ c = (a ⊓ c) Δ (b ⊓ c) :=
+by simp_rw [@inf_comm _ _ _ c, inf_symm_diff_distrib_left]
+
 lemma sdiff_symm_diff : c \ (a Δ b) = (c ⊓ a ⊓ b) ⊔ ((c \ a) ⊓ (c \ b)) :=
 by simp only [(Δ), sdiff_sdiff_sup_sdiff']
 
@@ -168,12 +178,21 @@ 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]
 
-lemma disjoint.disjoint_symm_diff_of_disjoint {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :
+@[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 :=
-begin
-  rw symm_diff_eq_sup_sdiff_inf,
-  exact (ha.sup_left hb).disjoint_sdiff_left,
-end
+by { rw symm_diff_eq_sup_sdiff_inf, exact (ha.sup_left hb).disjoint_sdiff_left }
+
+protected lemma disjoint.symm_diff_right (ha : disjoint a b) (hb : disjoint a c) :
+  disjoint a (b Δ c) :=
+(ha.symm.symm_diff_left hb.symm).symm
 
 end generalized_boolean_algebra