feat(data/finset/*): Diverse lemmas (#10388)

A bunch of simple lemmas

src/analysis/box_integral/basic.lean

@@ -114,7 +114,7 @@ begin
   rw [← integral_sum_inf_partition f vol π₁ h₂,
     ← integral_sum_inf_partition f vol π₂ h₁, integral_sum, integral_sum,
     finset.sum_sub_distrib],
-  simp only [inf_prepartition_to_prepartition, inf_comm]
+  simp only [inf_prepartition_to_prepartition, _root_.inf_comm]
 end
 
 @[simp] lemma integral_sum_disj_union (f : ℝⁿ → E) (vol : ι →ᵇᵃ (E →L[ℝ] F))
@@ -663,8 +663,9 @@ begin
     refine (dist_triangle_left _ _ J.upper).trans (add_le_add (h₁.1 _ _ _) (h₂.1 _ _ _)),
     { exact prepartition.bUnion_index_mem _ hJ },
     { exact box.le_iff_Icc.1 (prepartition.le_bUnion_index _ hJ) J.upper_mem_Icc },
-    { rw inf_comm at hJ, exact prepartition.bUnion_index_mem _ hJ, },
-    { rw inf_comm at hJ,
+    { rw _root_.inf_comm at hJ,
+      exact prepartition.bUnion_index_mem _ hJ },
+    { rw _root_.inf_comm at hJ,
       exact box.le_iff_Icc.1 (prepartition.le_bUnion_index _ hJ) J.upper_mem_Icc } },
   refine (norm_sum_le_of_le _ this).trans _,
   rw [← finset.sum_mul, μ.to_box_additive.sum_partition_boxes le_top (h₁p.inf h₂p)],

src/data/finset/basic.lean

@@ -1061,6 +1061,10 @@ val_le_iff.1 $ erase_le_erase _ $ val_le_iff.2 h
 
 theorem erase_subset (a : α) (s : finset α) : erase s a ⊆ s := erase_subset _ _
 
+lemma subset_erase {a : α} {s t : finset α} : s ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s :=
+⟨λ h, ⟨h.trans (erase_subset _ _), λ ha, not_mem_erase _ _ (h ha)⟩,
+  λ h b hb, mem_erase.2 ⟨ne_of_mem_of_not_mem hb h.2, h.1 hb⟩⟩
+
 @[simp, norm_cast] lemma coe_erase (a : α) (s : finset α) : ↑(erase s a) = (s \ {a} : set α) :=
 set.ext $ λ _, mem_erase.trans $ by rw [and_comm, set.mem_diff, set.mem_singleton_iff]; refl
 
@@ -1231,6 +1235,12 @@ by { ext, rw [mem_erase, mem_sdiff, mem_singleton], tauto }
 @[simp] lemma sdiff_singleton_not_mem_eq_self (s : finset α) {a : α} (ha : a ∉ s) : s \ {a} = s :=
 by simp only [sdiff_singleton_eq_erase, ha, erase_eq_of_not_mem, not_false_iff]
 
+lemma sdiff_erase {A : finset α} {x : α} (hx : x ∈ A) : A \ A.erase x = {x} :=
+begin
+  rw [← sdiff_singleton_eq_erase, sdiff_sdiff_right_self],
+  exact inf_eq_right.2 (singleton_subset_iff.2 hx),
+end
+
 lemma sdiff_sdiff_self_left (s t : finset α) : s \ (s \ t) = s ∩ t :=
 sdiff_sdiff_right_self
 
@@ -2792,6 +2802,18 @@ ext $ λ x, by simp only [mem_bUnion, mem_image, mem_singleton, eq_comm]
   s.bUnion (singleton : α → finset α) = s :=
 by { rw bUnion_singleton, exact image_id }
 
+lemma filter_bUnion (s : finset α) (f : α → finset β) (p : β → Prop) [decidable_pred p] :
+  (s.bUnion f).filter p = s.bUnion (λ a, (f a).filter p) :=
+begin
+  ext b,
+  simp only [mem_bUnion, exists_prop, mem_filter],
+  split,
+  { rintro ⟨⟨a, ha, hba⟩, hb⟩,
+    exact ⟨a, ha, hba, hb⟩ },
+  { rintro ⟨a, ha, hba, hb⟩,
+    exact ⟨⟨a, ha, hba⟩, hb⟩ }
+end
+
 lemma bUnion_filter_eq_of_maps_to [decidable_eq α] {s : finset α} {t : finset β} {f : α → β}
   (h : ∀ x ∈ s, f x ∈ t) :
   t.bUnion (λa, s.filter $ (λc, f c = a)) = s :=

src/data/finset/lattice.lean

@@ -5,8 +5,8 @@ Authors: Mario Carneiro
 -/
 import data.finset.fold
 import data.finset.option
+import data.finset.prod
 import data.multiset.lattice
-import order.order_dual
 import order.complete_lattice
 
 /-!
@@ -83,7 +83,7 @@ lemma sup_le {a : α} : (∀b ∈ s, f b ≤ a) → s.sup f ≤ a :=
 sup_le_iff.2
 
 lemma le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f :=
-sup_le_iff.1 (le_refl _) _ hb
+sup_le_iff.1 le_rfl _ hb
 
 lemma sup_mono_fun {g : β → α} (h : ∀b∈s, f b ≤ g b) : s.sup f ≤ s.sup g :=
 sup_le (λ b hb, le_trans (h b hb) (le_sup hb))
@@ -107,9 +107,44 @@ sup_le $ assume b hb, le_sup (h hb)
     (λ h, ⟨c, or.inl rfl, h⟩) (λ h, let ⟨b, hb, hlt⟩ := ih h in ⟨b, or.inr hb, hlt⟩)),
 (λ ⟨b, hb, hlt⟩, lt_of_lt_of_le hlt (le_sup hb))⟩
 
+lemma sup_comm (s : finset β) (t : finset γ) (f : β → γ → α) :
+  s.sup (λ b, t.sup (f b)) = t.sup (λ c, s.sup (λ b, f b c)) :=
+begin
+  refine eq_of_forall_ge_iff (λ a, _),
+  simp_rw sup_le_iff,
+  exact ⟨λ h c hc b hb, h b hb c hc, λ h b hb c hc, h c hc b hb⟩,
+end
+
 @[simp] lemma sup_attach (s : finset β) (f : β → α) : s.attach.sup (λ x, f x) = s.sup f :=
 (s.attach.sup_map (function.embedding.subtype _) f).symm.trans $ congr_arg _ attach_map_val
 
+lemma sup_sigma {γ : β → Type*} (s : finset β) (t : Π i, finset (γ i)) (f : sigma γ → α) :
+  (s.sigma t).sup f = s.sup (λ i, (t i).sup $ λ b, f ⟨i, b⟩) :=
+begin
+  refine le_antisymm _ (sup_le (λ i hi, sup_le $ λ b hb, le_sup $ mem_sigma.2 ⟨hi, hb⟩)),
+  refine sup_le _,
+  rintro ⟨i, b⟩ hb,
+  rw mem_sigma at hb,
+  refine le_trans _ (le_sup hb.1),
+  convert le_sup hb.2,
+end
+
+/-- See also `finset.product_bUnion`. -/
+lemma sup_product_left (s : finset β) (t : finset γ) (f : β × γ → α) :
+  (s.product t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) :=
+begin
+  refine le_antisymm _ (sup_le (λ i hi, sup_le $ λ i' hi', le_sup $ mem_product.2 ⟨hi, hi'⟩)),
+  refine sup_le _,
+  rintro ⟨i, i'⟩ hi,
+  rw mem_product at hi,
+  refine le_trans _ (le_sup hi.1),
+  convert le_sup hi.2,
+end
+
+lemma sup_product_right (s : finset β) (t : finset γ) (f : β × γ → α) :
+  (s.product t).sup f = t.sup (λ i', s.sup $ λ i, f ⟨i, i'⟩) :=
+by rw [sup_product_left, sup_comm]
+
 @[simp] lemma sup_erase_bot [decidable_eq α] (s : finset α) : (s.erase ⊥).sup id = s.sup id :=
 begin
   refine (sup_mono (s.erase_subset _)).antisymm (finset.sup_le_iff.2 $ λ a ha, _),
@@ -270,7 +305,7 @@ lemma le_inf_iff {a : α} : a ≤ s.inf f ↔ ∀ b ∈ s, a ≤ f b :=
 @sup_le_iff (order_dual α) _ _ _ _ _ _
 
 lemma inf_le {b : β} (hb : b ∈ s) : s.inf f ≤ f b :=
-le_inf_iff.1 (le_refl _) _ hb
+le_inf_iff.1 le_rfl _ hb
 
 lemma le_inf {a : α} : (∀b ∈ s, a ≤ f b) → a ≤ s.inf f :=
 le_inf_iff.2
@@ -293,6 +328,22 @@ le_inf $ assume b hb, inf_le (h hb)
 lemma inf_attach (s : finset β) (f : β → α) : s.attach.inf (λ x, f x) = s.inf f :=
 @sup_attach (order_dual α) _ _ _ _ _
 
+lemma inf_comm (s : finset β) (t : finset γ) (f : β → γ → α) :
+  s.inf (λ b, t.inf (f b)) = t.inf (λ c, s.inf (λ b, f b c)) :=
+@sup_comm (order_dual α) _ _ _ _ _ _ _
+
+lemma inf_sigma {γ : β → Type*} (s : finset β) (t : Π i, finset (γ i)) (f : sigma γ → α) :
+  (s.sigma t).inf f = s.inf (λ i, (t i).inf $ λ b, f ⟨i, b⟩) :=
+@sup_sigma (order_dual α) _ _ _ _ _ _ _
+
+lemma inf_product_left (s : finset β) (t : finset γ) (f : β × γ → α) :
+  (s.product t).inf f = s.inf (λ i, t.inf $ λ i', f ⟨i, i'⟩) :=
+@sup_product_left (order_dual α) _ _ _ _ _ _ _
+
+lemma inf_product_right (s : finset β) (t : finset γ) (f : β × γ → α) :
+  (s.product t).inf f = t.inf (λ i', s.inf $ λ i, f ⟨i, i'⟩) :=
+@sup_product_right (order_dual α) _ _ _ _ _ _ _
+
 @[simp] lemma inf_erase_top [decidable_eq α] (s : finset α) : (s.erase ⊤).inf id = s.inf id :=
 @sup_erase_bot (order_dual α) _ _ _ _
 

src/data/finset/prod.lean

@@ -37,6 +37,10 @@ protected def product (s : finset α) (t : finset β) : finset (α × β) := ⟨
 
 @[simp] lemma mem_product {p : α × β} : p ∈ s.product t ↔ p.1 ∈ s ∧ p.2 ∈ t := mem_product
 
+@[simp, norm_cast] lemma coe_product (s : finset α) (t : finset β) :
+  (s.product t : set (α × β)) = (s : set α).prod t :=
+set.ext $ λ x, finset.mem_product
+
 lemma subset_product [decidable_eq α] [decidable_eq β] {s : finset (α × β)} :
   s ⊆ (s.image prod.fst).product (s.image prod.snd) :=
 λ p hp, mem_product.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩
@@ -55,6 +59,12 @@ lemma product_eq_bUnion [decidable_eq α] [decidable_eq β] (s : finset α) (t :
 ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bUnion, mem_image, exists_prop, prod.mk.inj_iff,
   and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left]
 
+lemma product_eq_bUnion_right [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
+  s.product t = t.bUnion (λ b, s.image $ λ a, (a, b)) :=
+ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bUnion, mem_image, exists_prop, prod.mk.inj_iff,
+  and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left]
+
+/-- See also `finset.sup_product_left`. -/
 @[simp] lemma product_bUnion [decidable_eq γ] (s : finset α) (t : finset β) (f : α × β → finset γ) :
   (s.product t).bUnion f = s.bUnion (λ a, t.bUnion (λ b, f (a, b))) :=
 by { classical, simp_rw [product_eq_bUnion, bUnion_bUnion, image_bUnion] }

src/data/fintype/basic.lean

@@ -104,8 +104,10 @@ univ_nonempty_iff.2 ‹_›
 lemma univ_eq_empty_iff : (univ : finset α) = ∅ ↔ is_empty α :=
 by rw [← not_nonempty_iff, ← univ_nonempty_iff, not_nonempty_iff_eq_empty]
 
-lemma univ_eq_empty [is_empty α] : (univ : finset α) = ∅ :=
-univ_eq_empty_iff.2 ‹_›
+@[simp] lemma univ_eq_empty [is_empty α] : (univ : finset α) = ∅ := univ_eq_empty_iff.2 ‹_›
+
+@[simp] lemma univ_unique [unique α] : (univ : finset α) = {default α} :=
+finset.ext $ λ x, iff_of_true (mem_univ _) $ mem_singleton.2 $ subsingleton.elim x $ default α
 
 @[simp] theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 
@@ -563,8 +565,8 @@ subsingleton.elim (of_subsingleton $ default α) h ▸ card_of_subsingleton _
 instance of_is_empty [is_empty α] : fintype α := ⟨∅, is_empty_elim⟩
 
 /-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
-arbitrary `fintype` instances, use `fintype.univ_is_empty`. -/
--- no-lint since while `fintype.of_is_empty` can prove this, it isn't applicable for `dsimp`.
+arbitrary `fintype` instances, use `finset.univ_eq_empty`. -/
+-- no-lint since while `finset.univ_eq_empty` can prove this, it isn't applicable for `dsimp`.
 @[simp, nolint simp_nf] theorem univ_of_is_empty [is_empty α] : @univ α _ = ∅ := rfl
 
 /-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
@@ -736,12 +738,6 @@ since that relies on a subsingleton elimination for `unique`. -/
 instance fintype.subtype_eq' (y : α) : fintype {x // y = x} :=
 fintype.subtype {y} (by simp [eq_comm])
 
-@[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
-by rw [subsingleton.elim f (@unique.fintype α _)]; refl
-
-@[simp] lemma univ_is_empty {α : Type*} [is_empty α] [fintype α] : @finset.univ α _ = ∅ :=
-finset.ext is_empty_elim
-
 @[simp] lemma fintype.card_subtype_eq (y : α) [fintype {x // x = y}] :
   fintype.card {x // x = y} = 1 :=
 fintype.card_unique
@@ -790,6 +786,8 @@ instance multiplicative.fintype : Π [fintype α], fintype (multiplicative α) :
 instance {α : Type*} [fintype α] : fintype (option α) :=
 ⟨univ.insert_none, λ a, by simp⟩
 
+lemma univ_option (α : Type*) [fintype α] : (univ : finset (option α)) = insert_none univ := rfl
+
 @[simp] theorem fintype.card_option {α : Type*} [fintype α] :
   fintype.card (option α) = fintype.card α + 1 :=
 (finset.card_cons _).trans $ congr_arg2 _ (card_map _) rfl
@@ -1187,7 +1185,7 @@ def pi_finset (t : Π a, finset (δ a)) : finset (Π a, δ a) :=
 (finset.univ.pi t).map ⟨λ f a, f a (mem_univ a), λ _ _, by simp [function.funext_iff]⟩
 
 @[simp] lemma mem_pi_finset {t : Π a, finset (δ a)} {f : Π a, δ a} :
-  f ∈ pi_finset t ↔ (∀ a, f a ∈ t a) :=
+  f ∈ pi_finset t ↔ ∀ a, f a ∈ t a :=
 begin
   split,
   { simp only [pi_finset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ,
@@ -1201,7 +1199,7 @@ end
 
 @[simp] lemma coe_pi_finset (t : Π a, finset (δ a)) :
   (pi_finset t : set (Π a, δ a)) = set.pi set.univ (λ a, t a) :=
-by { ext, simp }
+set.ext $ λ x, by { rw set.mem_univ_pi, exact fintype.mem_pi_finset }
 
 lemma pi_finset_subset (t₁ t₂ : Π a, finset (δ a)) (h : ∀ a, t₁ a ⊆ t₂ a) :
   pi_finset t₁ ⊆ pi_finset t₂ :=

src/data/nat/interval.lean

@@ -54,9 +54,10 @@ instance : locally_finite_order ℕ :=
       exact iff_of_false (λ hx, hx.2.not_le hx.1) (λ hx, h.not_le (hx.1.trans hx.2)) }
   end }
 
-namespace nat
 variables (a b c : ℕ)
 
+namespace nat
+
 lemma Icc_eq_range' : Icc a b = (list.range' a (b + 1 - a)).to_finset := rfl
 lemma Ico_eq_range' : Ico a b = (list.range' a (b - a)).to_finset := rfl
 lemma Ioc_eq_range' : Ioc a b = (list.range' (a + 1) (b - a)).to_finset := rfl
@@ -173,12 +174,23 @@ begin
     lt_iff_le_and_ne],
 end
 
+end nat
+
+namespace finset
+
 lemma range_image_pred_top_sub (n : ℕ) : (finset.range n).image (λ j, n - 1 - j) = finset.range n :=
 begin
   cases n,
   { rw [range_zero, image_empty] },
-  { rw [finset.range_eq_Ico, Ico_image_const_sub_eq_Ico (zero_le _)],
+  { rw [finset.range_eq_Ico, nat.Ico_image_const_sub_eq_Ico (zero_le _)],
     simp_rw [succ_sub_succ, tsub_zero, tsub_self] }
 end
 
-end nat
+lemma range_add_eq_union : range (a + b) = range a ∪ (range b).map (add_left_embedding a) :=
+begin
+  rw [finset.range_eq_Ico, map_eq_image],
+  convert (Ico_union_Ico_eq_Ico a.zero_le le_self_add).symm,
+  exact image_add_left_Ico _ _ _,
+end
+
+end finset

src/data/set/basic.lean

@@ -446,6 +446,11 @@ lemma not_subset_iff_exists_mem_not_mem {α : Type*} {s t : set α} :
   ¬ s ⊆ t ↔ ∃ x, x ∈ s ∧ x ∉ t :=
 by simp [subset_def]
 
+lemma univ_unique [unique α] : @set.univ α = {default α} :=
+set.ext $ λ x, iff_of_true trivial $ subsingleton.elim x $ default α
+
+/-! ### Diagonal -/
+
 /-- `diagonal α` is the subset of `α × α` consisting of all pairs of the form `(a, a)`. -/
 def diagonal (α : Type*) : set (α × α) := {p | p.1 = p.2}
 

src/geometry/euclidean/monge_point.lean

@@ -422,11 +422,11 @@ begin
       have hd : finrank ℝ (s.altitude i).direction = 0,
       { rw [←h, finrank_bot] },
       simpa using hd },
-    { rw [←submodule.mem_inf, inf_comm, ←direction_altitude, ←h],
+    { rw [←submodule.mem_inf, _root_.inf_comm, ←direction_altitude, ←h],
       exact vsub_mem_vector_span ℝ (set.mem_insert _ _)
                                    (set.mem_insert_of_mem _ (set.mem_singleton _)) } },
   { rintro ⟨hne, h⟩,
-    rw [←submodule.mem_inf, inf_comm, ←direction_altitude] at h,
+    rw [←submodule.mem_inf, _root_.inf_comm, ←direction_altitude] at h,
     rw [vector_span_eq_span_vsub_set_left_ne ℝ (set.mem_insert _ _),
         set.insert_diff_of_mem _ (set.mem_singleton _),
         set.diff_singleton_eq_self (λ h, hne (set.mem_singleton_iff.1 h)), set.image_singleton],

src/linear_algebra/basis.lean

@@ -630,7 +630,7 @@ begin
   rw fintype.linear_independent_iff,
   rintros g sum_eq i,
   cases i,
-  simp only [function.const_apply, fin.default_eq_zero, submodule.coe_mk, univ_unique,
+  simp only [function.const_apply, fin.default_eq_zero, submodule.coe_mk, finset.univ_unique,
              function.comp_const, finset.sum_singleton] at sum_eq,
   convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
 end