From 442a83d738cb208d3600056c489be16900ba701d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 31 Aug 2023 08:51:42 +0000 Subject: [PATCH] feat(data/finset/lattice): `sup'`/`inf'` lemmas (#18989) Match (most of) the lemmas between `finset.sup`/`finset.inf` and `finset.sup'`/`finset.inf'`. Also golf two proofs using `eq_of_forall_ge_iff` to make sure both APIs prove their lemmas in as closely as possible a way. Also define `finset.nontrivial` to match `set.nontrivial`. --- src/data/dfinsupp/multiset.lean | 5 +- src/data/finset/basic.lean | 80 +++++++------ src/data/finset/lattice.lean | 107 +++++++++++++++--- src/data/finset/locally_finite.lean | 6 +- .../gauss_eisenstein_lemmas.lean | 2 +- 5 files changed, 140 insertions(+), 60 deletions(-) diff --git a/src/data/dfinsupp/multiset.lean b/src/data/dfinsupp/multiset.lean index de2ed3c8f1031..9b20c21615ef9 100644 --- a/src/data/dfinsupp/multiset.lean +++ b/src/data/dfinsupp/multiset.lean @@ -53,9 +53,8 @@ def to_dfinsupp : multiset α →+ Π₀ a : α, ℕ := @[simp] lemma to_dfinsupp_apply (s : multiset α) (a : α) : s.to_dfinsupp a = s.count a := rfl -@[simp] lemma to_dfinsupp_support (s : multiset α) : - s.to_dfinsupp.support = s.to_finset := -(finset.filter_eq_self _).mpr (λ x hx, count_ne_zero.mpr $ multiset.mem_to_finset.1 hx) +@[simp] lemma to_dfinsupp_support (s : multiset α) : s.to_dfinsupp.support = s.to_finset := +finset.filter_true_of_mem $ λ x hx, count_ne_zero.mpr $ multiset.mem_to_finset.1 hx @[simp] lemma to_dfinsupp_replicate (a : α) (n : ℕ) : to_dfinsupp (multiset.replicate n a) = dfinsupp.single a n := diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index ae0db3da0b9b8..9bb6c39eb6a06 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -536,14 +536,27 @@ by rw [←coe_ssubset, coe_singleton, set.ssubset_singleton_iff, coe_eq_empty] lemma eq_empty_of_ssubset_singleton {s : finset α} {x : α} (hs : s ⊂ {x}) : s = ∅ := ssubset_singleton_iff.1 hs -lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ (s : set α).nontrivial := +/-- A finset is nontrivial if it has at least two elements. -/ +@[reducible] protected def nontrivial (s : finset α) : Prop := (s : set α).nontrivial + +@[simp] lemma not_nontrivial_empty : ¬ (∅ : finset α).nontrivial := by simp [finset.nontrivial] + +@[simp] lemma not_nontrivial_singleton : ¬ ({a} : finset α).nontrivial := +by simp [finset.nontrivial] + +lemma nontrivial.ne_singleton (hs : s.nontrivial) : s ≠ {a} := +by { rintro rfl, exact not_nontrivial_singleton hs } + +lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ s.nontrivial := by { rw ←coe_eq_singleton, exact set.eq_singleton_or_nontrivial ha } -lemma nonempty.exists_eq_singleton_or_nontrivial : - s.nonempty → (∃ a, s = {a}) ∨ (s : set α).nontrivial := +lemma nontrivial_iff_ne_singleton (ha : a ∈ s) : s.nontrivial ↔ s ≠ {a} := +⟨nontrivial.ne_singleton, (eq_singleton_or_nontrivial ha).resolve_left⟩ + +lemma nonempty.exists_eq_singleton_or_nontrivial : s.nonempty → (∃ a, s = {a}) ∨ s.nontrivial := λ ⟨a, ha⟩, (eq_singleton_or_nontrivial ha).imp_left $ exists.intro a -instance [nonempty α] : nontrivial (finset α) := +instance nontrivial' [nonempty α] : nontrivial (finset α) := ‹nonempty α›.elim $ λ a, ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩ instance [is_empty α] : unique (finset α) := @@ -577,6 +590,8 @@ lemma forall_of_forall_cons {p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ co @[simp] lemma mk_cons {s : multiset α} (h : (a ::ₘ s).nodup) : (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 := rfl +@[simp] lemma cons_empty (a : α) : cons a ∅ (not_mem_empty _) = {a} := rfl + @[simp] lemma nonempty_cons (h : a ∉ s) : (cons a s h).nonempty := ⟨a, mem_cons.2 $ or.inl rfl⟩ @[simp] lemma nonempty_mk {m : multiset α} {hm} : (⟨m, hm⟩ : finset α).nonempty ↔ m ≠ 0 := @@ -1379,7 +1394,7 @@ lemma inter_sdiff (s t u : finset α) : s ∩ (t \ u) = s ∩ t \ u := by { ext @[simp] lemma sdiff_inter_self (s₁ s₂ : finset α) : (s₂ \ s₁) ∩ s₁ = ∅ := inf_sdiff_self_left -@[simp] lemma sdiff_self (s₁ : finset α) : s₁ \ s₁ = ∅ := sdiff_self +@[simp] protected lemma sdiff_self (s₁ : finset α) : s₁ \ s₁ = ∅ := sdiff_self lemma sdiff_inter_distrib_right (s t u : finset α) : s \ (t ∩ u) = (s \ t) ∪ (s \ u) := sdiff_inf @@ -1531,7 +1546,7 @@ by rw [←sdiff_singleton_eq_erase, sdiff_sdiff_eq_sdiff_union (singleton_subset union_comm] lemma sdiff_erase_self (ha : a ∈ s) : s \ s.erase a = {a} := -by rw [sdiff_erase ha, sdiff_self, insert_emptyc_eq] +by rw [sdiff_erase ha, finset.sdiff_self, insert_emptyc_eq] lemma sdiff_sdiff_self_left (s t : finset α) : s \ (s \ t) = s ∩ t := sdiff_sdiff_right_self @@ -1588,10 +1603,10 @@ theorem sizeof_lt_sizeof_of_mem [has_sizeof α] {x : α} {s : finset α} (hx : x @[simp] theorem attach_empty : attach (∅ : finset α) = ∅ := rfl -@[simp] lemma attach_nonempty_iff (s : finset α) : s.attach.nonempty ↔ s.nonempty := +@[simp] lemma attach_nonempty_iff {s : finset α} : s.attach.nonempty ↔ s.nonempty := by simp [finset.nonempty] -@[simp] lemma attach_eq_empty_iff (s : finset α) : s.attach = ∅ ↔ s = ∅ := +@[simp] lemma attach_eq_empty_iff {s : finset α} : s.attach = ∅ ↔ s = ∅ := by simpa [eq_empty_iff_forall_not_mem] /-! ### piecewise -/ @@ -1747,7 +1762,7 @@ end decidable_pi_exists /-! ### filter -/ section filter -variables (p q : α → Prop) [decidable_pred p] [decidable_pred q] +variables (p q : α → Prop) [decidable_pred p] [decidable_pred q] {s : finset α} /-- `filter p s` is the set of elements of `s` that satisfy `p`. -/ def filter (s : finset α) : finset α := ⟨_, s.2.filter p⟩ @@ -1772,38 +1787,34 @@ variable (p) theorem filter_filter (s : finset α) : (s.filter p).filter q = s.filter (λa, p a ∧ q a) := ext $ assume a, by simp only [mem_filter, and_comm, and.left_comm] -lemma filter_true {s : finset α} [h : decidable_pred (λ _, true)] : - @finset.filter α (λ _, true) h s = s := -by ext; simp +lemma filter_comm (s : finset α) : (s.filter p).filter q = (s.filter q).filter p := +by simp_rw [filter_filter, and_comm] + +/- We can simplify an application of filter where the decidability is inferred in "the wrong way" -/ +@[simp] lemma filter_congr_decidable (s : finset α) (p : α → Prop) (h : decidable_pred p) + [decidable_pred p] : @filter α p h s = s.filter p := +by congr -@[simp] theorem filter_false {h} (s : finset α) : @filter α (λa, false) h s = ∅ := -ext $ assume a, by simp only [mem_filter, and_false]; refl +lemma filter_true {h} (s : finset α) : @filter α (λ a, true) h s = s := by ext; simp +lemma filter_false {h} (s : finset α) : @filter α (λ a, false) h s = ∅ := by ext; simp variables {p q} -lemma filter_eq_self (s : finset α) : - s.filter p = s ↔ ∀ x ∈ s, p x := -by simp [finset.ext_iff] +lemma filter_eq_self : s.filter p = s ↔ ∀ ⦃x⦄, x ∈ s → p x := by simp [finset.ext_iff] +lemma filter_eq_empty_iff : s.filter p = ∅ ↔ ∀ ⦃x⦄, x ∈ s → ¬ p x := by simp [finset.ext_iff] + +lemma filter_nonempty_iff {s : finset α} : (s.filter p).nonempty ↔ ∃ a ∈ s, p a := +by simp only [nonempty_iff_ne_empty, ne.def, filter_eq_empty_iff, not_not, not_forall] /-- If all elements of a `finset` satisfy the predicate `p`, `s.filter p` is `s`. -/ -@[simp] lemma filter_true_of_mem {s : finset α} (h : ∀ x ∈ s, p x) : s.filter p = s := -(filter_eq_self s).mpr h +@[simp] lemma filter_true_of_mem (h : ∀ x ∈ s, p x) : s.filter p = s := filter_eq_self.2 h /-- If all elements of a `finset` fail to satisfy the predicate `p`, `s.filter p` is `∅`. -/ -lemma filter_false_of_mem {s : finset α} (h : ∀ x ∈ s, ¬ p x) : s.filter p = ∅ := -eq_empty_of_forall_not_mem (by simpa) +@[simp] lemma filter_false_of_mem (h : ∀ x ∈ s, ¬ p x) : s.filter p = ∅ := filter_eq_empty_iff.2 h -lemma filter_eq_empty_iff (s : finset α) : - (s.filter p = ∅) ↔ ∀ x ∈ s, ¬ p x := -begin - refine ⟨_, filter_false_of_mem⟩, - intros hs, - injection hs with hs', - rwa filter_eq_nil at hs' -end - -lemma filter_nonempty_iff {s : finset α} : (s.filter p).nonempty ↔ ∃ a ∈ s, p a := -by simp only [nonempty_iff_ne_empty, ne.def, filter_eq_empty_iff, not_not, not_forall] +@[simp] lemma filter_const (p : Prop) [decidable p] (s : finset α) : + s.filter (λ a, p) = if p then s else ∅ := +by split_ifs; simp [*] lemma filter_congr {s : finset α} (H : ∀ x ∈ s, p x ↔ q x) : filter p s = filter q s := eq_of_veq $ filter_congr H @@ -1944,11 +1955,6 @@ begin { intro x, simp, intros hx hx₂, refine ⟨or.resolve_left (h hx) hx₂, hx₂⟩ } end -/- We can simplify an application of filter where the decidability is inferred in "the wrong way" -/ -@[simp] lemma filter_congr_decidable {α} (s : finset α) (p : α → Prop) (h : decidable_pred p) - [decidable_pred p] : @filter α p h s = s.filter p := -by congr - section classical open_locale classical /-- The following instance allows us to write `{x ∈ s | p x}` for `finset.filter p s`. diff --git a/src/data/finset/lattice.lean b/src/data/finset/lattice.lean index 208cbac617b55..60a235f53593d 100644 --- a/src/data/finset/lattice.lean +++ b/src/data/finset/lattice.lean @@ -55,10 +55,6 @@ fold_map @[simp] lemma sup_singleton {b : β} : ({b} : finset β).sup f = f b := sup_singleton -lemma sup_union [decidable_eq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f := -finset.induction_on s₁ (by rw [empty_union, sup_empty, bot_sup_eq]) $ λ a s has ih, -by rw [insert_union, sup_insert, sup_insert, ih, sup_assoc] - lemma sup_sup : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g := begin refine finset.cons_induction_on s _ (λ b t _ h, _), @@ -91,6 +87,9 @@ lemma le_sup {b : β} (hb : b ∈ s) : f b ≤ s.sup f := finset.sup_le_iff.1 le lemma le_sup_of_le {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup f := h.trans $ le_sup hb +lemma sup_union [decidable_eq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f := +eq_of_forall_ge_iff $ λ c, by simp [or_imp_distrib, forall_and_distrib] + @[simp] lemma sup_bUnion [decidable_eq β] (s : finset γ) (t : γ → finset β) : (s.bUnion t).sup f = s.sup (λ x, (t x).sup f) := eq_of_forall_ge_iff $ λ c, by simp [@forall_swap _ β] @@ -117,11 +116,7 @@ lemma sup_mono (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f := finset.sup_le protected 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 finset.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 +eq_of_forall_ge_iff $ λ a, by simpa using forall₂_swap @[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 @@ -129,10 +124,7 @@ end /-- See also `finset.product_bUnion`. -/ lemma sup_product_left (s : finset β) (t : finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) := -begin - simp only [le_antisymm_iff, finset.sup_le_iff, mem_product, and_imp, prod.forall], - exact ⟨λ b c hb hc, (le_sup hb).trans' $ le_sup hc, λ b hb c hc, le_sup $ mem_product.2 ⟨hb, hc⟩⟩, -end +eq_of_forall_ge_iff $ λ a, by simp [@forall_swap _ γ] lemma sup_product_right (s : finset β) (t : finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = t.sup (λ i', s.sup $ λ i, f ⟨i, i'⟩) := @@ -288,9 +280,6 @@ fold_map @[simp] lemma inf_singleton {b : β} : ({b} : finset β).inf f = f b := inf_singleton -lemma inf_union [decidable_eq β] : (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f := -@sup_union αᵒᵈ _ _ _ _ _ _ _ - lemma inf_inf : s.inf (f ⊓ g) = s.inf f ⊓ s.inf g := @sup_sup αᵒᵈ _ _ _ _ _ _ @@ -301,6 +290,9 @@ by subst hs; exact finset.fold_congr hfg (f : F) (s : finset ι) (g : ι → α) : f (s.inf g) = s.inf (f ∘ g) := finset.cons_induction_on s (map_top f) $ λ i s _ h, by rw [inf_cons, inf_cons, map_inf, h] +lemma inf_union [decidable_eq β] : (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f := +@sup_union αᵒᵈ _ _ _ _ _ _ _ + @[simp] lemma inf_bUnion [decidable_eq β] (s : finset γ) (t : γ → finset β) : (s.bUnion t).inf f = s.inf (λ x, (t x).inf f) := @sup_bUnion αᵒᵈ _ _ _ _ _ _ _ _ @@ -628,11 +620,28 @@ end @[simp] lemma sup'_le_iff {a : α} : s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a := iff.intro (λ h b hb, trans (le_sup' f hb) h) (sup'_le H f) +lemma sup'_union [decidable_eq β] {s₁ s₂ : finset β} (h₁ : s₁.nonempty) (h₂ : s₂.nonempty) + (f : β → α) : + (s₁ ∪ s₂).sup' (h₁.mono $ subset_union_left _ _) f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f := +eq_of_forall_ge_iff $ λ a, by simp [or_imp_distrib, forall_and_distrib] + lemma sup'_bUnion [decidable_eq β] {s : finset γ} (Hs : s.nonempty) {t : γ → finset β} (Ht : ∀ b, (t b).nonempty) : (s.bUnion t).sup' (Hs.bUnion (λ b _, Ht b)) f = s.sup' Hs (λ b, (t b).sup' (Ht b) f) := eq_of_forall_ge_iff $ λ c, by simp [@forall_swap _ β] +protected lemma sup'_comm {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β → γ → α) : + s.sup' hs (λ b, t.sup' ht (f b)) = t.sup' ht (λ c, s.sup' hs $ λ b, f b c) := +eq_of_forall_ge_iff $ λ a, by simpa using forall₂_swap + +lemma sup'_product_left {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β × γ → α) : + (s ×ˢ t).sup' (hs.product ht) f = s.sup' hs (λ i, t.sup' ht $ λ i', f ⟨i, i'⟩) := +eq_of_forall_ge_iff $ λ a, by simp [@forall_swap _ γ] + +lemma sup'_product_right {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β × γ → α) : + (s ×ˢ t).sup' (hs.product ht) f = t.sup' ht (λ i', s.sup' hs $ λ i, f ⟨i, i'⟩) := +by rw [sup'_product_left, finset.sup'_comm] + lemma comp_sup'_eq_sup'_comp [semilattice_sup γ] {s : finset β} (H : s.nonempty) {f : β → α} (g : α → γ) (g_sup : ∀ x y, g (x ⊔ y) = g x ⊔ g y) : g (s.sup' H f) = s.sup' H (g ∘ f) := @@ -675,6 +684,15 @@ begin simp only [sup'_le_iff, h₂] { contextual := tt } end +@[simp] lemma _root_.map_finset_sup' [semilattice_sup β] [sup_hom_class F α β] (f : F) + {s : finset ι} (hs) (g : ι → α) : f (s.sup' hs g) = s.sup' hs (f ∘ g) := +by refine hs.cons_induction _ _; intros; simp [*] + +@[simp] lemma sup'_image [decidable_eq β] {s : finset γ} {f : γ → β} (hs : (s.image f).nonempty) + (g : β → α) (hs': s.nonempty := (nonempty.image_iff _).1 hs) : + (s.image f).sup' hs g = s.sup' hs' (g ∘ f) := +by { rw ←with_bot.coe_eq_coe, simp only [coe_sup', sup_image, with_bot.coe_sup] } + @[simp] lemma sup'_map {s : finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f).nonempty) (hs': s.nonempty := finset.map_nonempty.mp hs) : (s.map f).sup' hs g = s.sup' hs' (g ∘ f) := @@ -719,11 +737,28 @@ lemma inf'_le_of_le (hb : b ∈ s) (h : f b ≤ a) : s.inf' ⟨b, hb⟩ f ≤ a @[simp] lemma le_inf'_iff : a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b := @sup'_le_iff αᵒᵈ _ _ _ H f _ +lemma inf'_union [decidable_eq β] {s₁ s₂ : finset β} (h₁ : s₁.nonempty) (h₂ : s₂.nonempty) + (f : β → α) : + (s₁ ∪ s₂).inf' (h₁.mono $ subset_union_left _ _) f = s₁.inf' h₁ f ⊓ s₂.inf' h₂ f := +@sup'_union αᵒᵈ _ _ _ _ _ h₁ h₂ _ + lemma inf'_bUnion [decidable_eq β] {s : finset γ} (Hs : s.nonempty) {t : γ → finset β} (Ht : ∀ b, (t b).nonempty) : (s.bUnion t).inf' (Hs.bUnion (λ b _, Ht b)) f = s.inf' Hs (λ b, (t b).inf' (Ht b) f) := @sup'_bUnion αᵒᵈ _ _ _ _ _ _ Hs _ Ht +protected lemma inf'_comm {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β → γ → α) : + s.inf' hs (λ b, t.inf' ht (f b)) = t.inf' ht (λ c, s.inf' hs $ λ b, f b c) := +@finset.sup'_comm αᵒᵈ _ _ _ _ _ hs ht _ + +lemma inf'_product_left {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β × γ → α) : + (s ×ˢ t).inf' (hs.product ht) f = s.inf' hs (λ i, t.inf' ht $ λ i', f ⟨i, i'⟩) := +@sup'_product_left αᵒᵈ _ _ _ _ _ hs ht _ + +lemma inf'_product_right {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β × γ → α) : + (s ×ˢ t).inf' (hs.product ht) f = t.inf' ht (λ i', s.inf' hs $ λ i, f ⟨i, i'⟩) := +@sup'_product_right αᵒᵈ _ _ _ _ _ hs ht _ + lemma comp_inf'_eq_inf'_comp [semilattice_inf γ] {s : finset β} (H : s.nonempty) {f : β → α} (g : α → γ) (g_inf : ∀ x y, g (x ⊓ y) = g x ⊓ g y) : g (s.inf' H f) = s.inf' H (g ∘ f) := @@ -741,6 +776,15 @@ lemma inf'_mem (s : set α) (w : ∀ x y ∈ s, x ⊓ y ∈ s) s.inf' H f = t.inf' (h₁ ▸ H) g := @sup'_congr αᵒᵈ _ _ _ H _ _ _ h₁ h₂ +@[simp] lemma _root_.map_finset_inf' [semilattice_inf β] [inf_hom_class F α β] (f : F) + {s : finset ι} (hs) (g : ι → α) : f (s.inf' hs g) = s.inf' hs (f ∘ g) := +by refine hs.cons_induction _ _; intros; simp [*] + +@[simp] lemma inf'_image [decidable_eq β] {s : finset γ} {f : γ → β} (hs : (s.image f).nonempty) + (g : β → α) (hs': s.nonempty := (nonempty.image_iff _).1 hs) : + (s.image f).inf' hs g = s.inf' hs' (g ∘ f) := +@sup'_image αᵒᵈ _ _ _ _ _ _ hs _ hs' + @[simp] lemma inf'_map {s : finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f).nonempty) (hs': s.nonempty := finset.map_nonempty.mp hs) : (s.map f).inf' hs g = s.inf' hs' (g ∘ f) := @@ -829,6 +873,37 @@ end inf' @[simp] lemma of_dual_inf' [semilattice_sup α] {s : finset ι} (hs : s.nonempty) (f : ι → αᵒᵈ) : of_dual (s.inf' hs f) = s.sup' hs (of_dual ∘ f) := rfl +section distrib_lattice +variables [distrib_lattice α] {s : finset ι} {t : finset κ} (hs : s.nonempty) (ht : t.nonempty) + {f : ι → α} {g : κ → α} {a : α} + +lemma sup'_inf_distrib_left (f : ι → α) (a : α) : a ⊓ s.sup' hs f = s.sup' hs (λ i, a ⊓ f i) := +begin + refine hs.cons_induction (λ i, _) (λ i s hi hs ih, _) , + { simp }, + { simp_rw [sup'_cons hs, inf_sup_left], + rw ih } +end + +lemma sup'_inf_distrib_right (f : ι → α) (a : α) : s.sup' hs f ⊓ a = s.sup' hs (λ i, f i ⊓ a) := +by { rw [inf_comm, sup'_inf_distrib_left], simp_rw inf_comm } + +lemma sup'_inf_sup' (f : ι → α) (g : κ → α) : + s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) (λ i, f i.1 ⊓ g i.2) := +by simp_rw [finset.sup'_inf_distrib_right, finset.sup'_inf_distrib_left, sup'_product_left] + +lemma inf'_sup_distrib_left (f : ι → α) (a : α) : a ⊔ s.inf' hs f = s.inf' hs (λ i, a ⊔ f i) := +@sup'_inf_distrib_left αᵒᵈ _ _ _ hs _ _ + +lemma inf'_sup_distrib_right (f : ι → α) (a : α) : s.inf' hs f ⊔ a = s.inf' hs (λ i, f i ⊔ a) := +@sup'_inf_distrib_right αᵒᵈ _ _ _ hs _ _ + +lemma inf'_sup_inf' (f : ι → α) (g : κ → α) : + s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' (hs.product ht) (λ i, f i.1 ⊔ g i.2) := +@sup'_inf_sup' αᵒᵈ _ _ _ _ _ hs ht _ _ + +end distrib_lattice + section linear_order variables [linear_order α] {s : finset ι} (H : s.nonempty) {f : ι → α} {a : α} diff --git a/src/data/finset/locally_finite.lean b/src/data/finset/locally_finite.lean index f8b6e5b429cc9..7864e60893459 100644 --- a/src/data/finset/locally_finite.lean +++ b/src/data/finset/locally_finite.lean @@ -199,16 +199,16 @@ end lemma Icc_filter_lt_of_lt_right {a b c : α} [decidable_pred (< c)] (h : b < c) : (Icc a b).filter (< c) = Icc a b := -(finset.filter_eq_self _).2 (λ x hx, lt_of_le_of_lt (mem_Icc.1 hx).2 h) +filter_true_of_mem $ λ x hx, (mem_Icc.1 hx).2.trans_lt h lemma Ioc_filter_lt_of_lt_right {a b c : α} [decidable_pred (< c)] (h : b < c) : (Ioc a b).filter (< c) = Ioc a b := -(finset.filter_eq_self _).2 (λ x hx, lt_of_le_of_lt (mem_Ioc.1 hx).2 h) +filter_true_of_mem $ λ x hx, (mem_Ioc.1 hx).2.trans_lt h lemma Iic_filter_lt_of_lt_right {α} [preorder α] [locally_finite_order_bot α] {a c : α} [decidable_pred (< c)] (h : a < c) : (Iic a).filter (< c) = Iic a := -(finset.filter_eq_self _).2 (λ x hx, lt_of_le_of_lt (mem_Iic.1 hx) h) +filter_true_of_mem $ λ x hx, (mem_Iic.1 hx).trans_lt h variables (a b) [fintype α] diff --git a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean index 344697e529726..171dcc9523d6f 100644 --- a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean +++ b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean @@ -90,7 +90,7 @@ calc (a ^ (p / 2) * (p / 2)! : zmod p) = (λ _ _ _ _ _ _, id) (λ b h _, ⟨b, by simp [-not_le, *] at *⟩) (by intros; split_ifs at *; simp * at *), - by rw [prod_mul_distrib, this]; simp + by rw [prod_mul_distrib, this, prod_const] ... = (-1)^((Ico 1 (p / 2).succ).filter (λ x : ℕ, ¬(a * x : zmod p).val ≤ p / 2)).card * (p / 2)! : by rw [← prod_nat_cast, finset.prod_eq_multiset_prod,