feat(order/complete_lattice): add complete_lattice.independent_pair (#12565)

This makes `complete_lattice.independent` easier to work with in the degenerate case.

Author: eric-wieser

counterexamples/direct_sum_is_internal.lean

@@ -54,17 +54,10 @@ end
 
 def with_sign.independent : complete_lattice.independent with_sign :=
 begin
+  refine (complete_lattice.independent_pair units_int.one_ne_neg_one _).mpr
+    with_sign.is_compl.disjoint,
   intros i,
-  rw [←finset.sup_univ_eq_supr, units_int.univ, finset.sup_insert, finset.sup_singleton],
-  fin_cases i,
-  { convert with_sign.is_compl.disjoint,
-    convert bot_sup_eq,
-    { exact supr_neg (not_not_intro rfl), },
-    { rw supr_pos units_int.one_ne_neg_one.symm } },
-  { convert with_sign.is_compl.disjoint.symm,
-    convert sup_bot_eq,
-    { exact supr_neg (not_not_intro rfl), },
-    { rw supr_pos units_int.one_ne_neg_one } },
+  fin_cases i; simp,
 end
 
 lemma with_sign.supr : supr with_sign = ⊤ :=

src/data/set/basic.lean

@@ -1060,6 +1060,16 @@ lemma insert_diff_self_of_not_mem {a : α} {s : set α} (h : a ∉ s) :
   insert a s \ {a} = s :=
 by { ext, simp [and_iff_left_of_imp (λ hx : x ∈ s, show x ≠ a, from λ hxa, h $ hxa ▸ hx)] }
 
+@[simp] lemma insert_diff_eq_singleton {a : α} {s : set α} (h : a ∉ s) :
+  insert a s \ s = {a} :=
+begin
+  ext,
+  rw [set.mem_diff, set.mem_insert_iff, set.mem_singleton_iff, or_and_distrib_right,
+    and_not_self, or_false, and_iff_left_iff_imp],
+  rintro rfl,
+  exact h,
+end
+
 lemma insert_inter_of_mem {s₁ s₂ : set α} {a : α} (h : a ∈ s₂) :
   insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
 by simp [set.insert_inter, h]

src/order/complete_lattice.lean

@@ -1348,6 +1348,19 @@ theorem set_independent.mono {t : set α} (hst : t ⊆ s) :
 lemma set_independent.disjoint {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : disjoint x y :=
 disjoint_Sup_right (hs hx) ((mem_diff y).mpr ⟨hy, by simp [h.symm]⟩)
 
+lemma set_independent_pair {a b : α} (hab : a ≠ b) :
+  set_independent ({a, b} : set α) ↔ disjoint a b :=
+begin
+  split,
+  { intro h,
+    exact h.disjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab, },
+  { rintros h c ((rfl : c = a) | (rfl : c = b)),
+    { convert h using 1,
+      simp [hab, Sup_singleton] },
+    { convert h.symm using 1,
+      simp [hab, Sup_singleton] }, },
+end
+
 include hs
 
 /-- If the elements of a set are independent, then any element is disjoint from the `Sup` of some
@@ -1422,6 +1435,20 @@ lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
   exact supr_le_supr_const hf.ne,
 end
 
+lemma independent_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j):
+  independent t ↔ disjoint (t i) (t j) :=
+begin
+  split,
+  { intro h,
+    exact h.disjoint hij, },
+  { rintros h k,
+    obtain rfl | rfl := huniv k,
+    { refine h.mono_right (supr_le $ λ i, supr_le $ λ hi, eq.le _),
+      rw (huniv i).resolve_left hi },
+    { refine h.symm.mono_right (supr_le $ λ j, supr_le $ λ hj, eq.le _),
+      rw (huniv j).resolve_right hj } },
+end
+
 /-- Composing an indepedent indexed family with an order isomorphism on the elements results in
 another indepedendent indexed family. -/
 lemma independent.map_order_iso {ι : Sort*} {α β : Type*}