feat(data/finset/lattice): sup'/inf' lemmas (#18989)

YaelDillies · YaelDillies · commit 442a83d738cb · 2023-08-31T08:51:42.000Z
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`.
diff --git 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
@@ -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
@@ -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,22 +116,15 @@ 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
 
 /-- 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
@@ -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
@@ -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,
