feat(finset/lattice): sup' is to sup as max' is to max (#7087)

Introducing `finset.sup'`, modelled on `finset.max'` but having no need for a `linear_order`. I wanted this for functions so also provide `sup_apply` and `sup'_apply`. By using `cons` instead of `insert` the axiom of choice is avoided throughout and I have replaced the proofs of three existing lemmas (`sup_lt_iff`, `comp_sup_eq_sup_comp`, `sup_closed_of_sup_closed`) that didn't need it. I have removed `sup_subset` entirely as it was surely introduced in ignorance of `sup_mono`.

src/data/finset/basic.lean

@@ -517,15 +517,25 @@ lemma ssubset_insert {s : finset α} {a : α} (h : a ∉ s) : s ⊂ insert a s :
 ssubset_iff.mpr ⟨a, h, subset.refl _⟩
 
 @[elab_as_eliminator]
-protected theorem induction {α : Type*} {p : finset α → Prop} [decidable_eq α]
-  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) : ∀ s, p s
+lemma cons_induction {α : Type*} {p : finset α → Prop}
+  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α} (h : a ∉ s), p s → p (cons a s h)) : ∀ s, p s
 | ⟨s, nd⟩ := multiset.induction_on s (λ _, h₁) (λ a s IH nd, begin
     cases nodup_cons.1 nd with m nd',
-    rw [← (eq_of_veq _ : insert a (finset.mk s _) = ⟨a ::ₘ s, nd⟩)],
+    rw [← (eq_of_veq _ : cons a (finset.mk s _) m = ⟨a ::ₘ s, nd⟩)],
     { exact h₂ (by exact m) (IH nd') },
-    { rw [insert_val, ndinsert_of_not_mem m] }
+    { rw [cons_val] }
   end) nd
 
+@[elab_as_eliminator]
+lemma cons_induction_on {α : Type*} {p : finset α → Prop} (s : finset α)
+  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α} (h : a ∉ s), p s → p (cons a s h)) : p s :=
+cons_induction h₁ h₂ s
+
+@[elab_as_eliminator]
+protected theorem induction {α : Type*} {p : finset α → Prop} [decidable_eq α]
+  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) : ∀ s, p s :=
+cons_induction h₁ $ λ a s ha, (s.cons_eq_insert a ha).symm ▸ h₂ ha
+
 /--
 To prove a proposition about an arbitrary `finset α`,
 it suffices to prove it for the empty `finset`,

src/data/finset/fold.lean

@@ -29,6 +29,9 @@ variables {op} {f : α → β} {b : β} {s : finset α} {a : α}
 
 @[simp] theorem fold_empty : (∅ : finset α).fold op b f = b := rfl
 
+@[simp] theorem fold_cons (h : a ∉ s) : (cons a s h).fold op b f = f a * s.fold op b f :=
+by { dunfold fold, rw [cons_val, map_cons, fold_cons_left], }
+
 @[simp] theorem fold_insert [decidable_eq α] (h : a ∉ s) :
   (insert a s).fold op b f = f a * s.fold op b f :=
 by unfold fold; rw [insert_val, ndinsert_of_not_mem h, map_cons, fold_cons_left]

src/data/finset/lattice.lean

@@ -31,6 +31,9 @@ lemma sup_def : s.sup f = (s.1.map f).sup := rfl
 @[simp] lemma sup_empty : (∅ : finset β).sup f = ⊥ :=
 fold_empty
 
+@[simp] lemma sup_cons {b : β} (h : b ∉ s) : (cons b s h).sup f = f b ⊔ s.sup f :=
+fold_cons h
+
 @[simp] lemma sup_insert [decidable_eq β] {b : β} : (insert b s : finset β).sup f = f b ⊔ s.sup f :=
 fold_insert_idem
 
@@ -70,17 +73,14 @@ sup_le (λ b hb, le_trans (h b hb) (le_sup hb))
 lemma sup_mono (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f :=
 sup_le $ assume b hb, le_sup (h hb)
 
-@[simp] lemma sup_lt_iff [is_total α (≤)] {a : α} (ha : ⊥ < a) :
-  s.sup f < a ↔ (∀b ∈ s, f b < a) :=
-by letI := classical.dec_eq β; from
-⟨ λh b hb, lt_of_le_of_lt (le_sup hb) h,
-  finset.induction_on s (by simp [ha]) (by simp {contextual := tt}) ⟩
+@[simp] lemma sup_lt_iff [is_total α (≤)] {a : α} (ha : ⊥ < a) : s.sup f < a ↔ (∀ b ∈ s, f b < a) :=
+⟨(λ hs b hb, lt_of_le_of_lt (le_sup hb) hs), finset.cons_induction_on s (λ _, ha)
+  (λ c t hc, by simpa only [sup_cons, sup_lt_iff, mem_cons, forall_eq_or_imp] using and.imp_right)⟩
 
 lemma comp_sup_eq_sup_comp [semilattice_sup_bot γ] {s : finset β}
   {f : β → α} (g : α → γ) (g_sup : ∀ x y, g (x ⊔ y) = g x ⊔ g y) (bot : g ⊥ = ⊥) :
   g (s.sup f) = s.sup (g ∘ f) :=
-by letI := classical.dec_eq β; from
-finset.induction_on s (by simp [bot]) (by simp [g_sup] {contextual := tt})
+finset.cons_induction_on s bot (λ c t hc ih, by rw [sup_cons, sup_cons, g_sup, ih])
 
 lemma comp_sup_eq_sup_comp_of_is_total [is_total α (≤)] {γ : Type} [semilattice_sup_bot γ]
   (g : α → γ) (mono_g : monotone g) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
@@ -91,7 +91,7 @@ lemma sup_coe {P : α → Prop}
   {Pbot : P ⊥} {Psup : ∀{{x y}}, P x → P y → P (x ⊔ y)}
   (t : finset β) (f : β → {x : α // P x}) :
   (@sup _ _ (subtype.semilattice_sup_bot Pbot Psup) t f : α) = t.sup (λ x, f x) :=
-by { classical, rw [comp_sup_eq_sup_comp coe]; intros; refl }
+by { rw [comp_sup_eq_sup_comp coe]; intros; refl }
 
 @[simp] lemma sup_to_finset {α β} [decidable_eq β]
   (s : finset α) (f : α → multiset β) :
@@ -104,23 +104,15 @@ theorem subset_range_sup_succ (s : finset ℕ) : s ⊆ range (s.sup id).succ :=
 theorem exists_nat_subset_range (s : finset ℕ) : ∃n : ℕ, s ⊆ range n :=
 ⟨_, s.subset_range_sup_succ⟩
 
-lemma sup_subset {α β} [semilattice_sup_bot β] {s t : finset α} (hst : s ⊆ t) (f : α → β) :
-  s.sup f ≤ t.sup f :=
-by classical;
-calc t.sup f = (s ∪ t).sup f : by rw [finset.union_eq_right_iff_subset.mpr hst]
-         ... = s.sup f ⊔ t.sup f : by rw finset.sup_union
-         ... ≥ s.sup f : le_sup_left
-
-lemma sup_closed_of_sup_closed {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : ↑t ⊆ s)
-  (h : ∀⦃a b⦄, a ∈ s → b ∈ s → a ⊔ b ∈ s) : t.sup id ∈ s :=
+lemma of_sup_of_forall {p : α → Prop} (hb : p ⊥) (hp : ∀ (a₁ a₂ : α), p a₁ → p a₂ → p (a₁ ⊔ a₂))
+  (hs : ∀ b ∈ s, p (f b)) : p (s.sup f) :=
 begin
-  classical,
-  induction t using finset.induction_on with x t h₀ h₁,
-  { exfalso, apply finset.not_nonempty_empty htne, },
-  { rw [finset.coe_insert, set.insert_subset] at h_subset,
-    cases t.eq_empty_or_nonempty with hte htne,
-    { subst hte, simp only [insert_emptyc_eq, id.def, finset.sup_singleton, h_subset], },
-    { rw [finset.sup_insert, id.def], exact h h_subset.1 (h₁ htne h_subset.2), }, },
+  induction s using finset.cons_induction with c s hc ih,
+  { exact hb, },
+  { rw sup_cons,
+    apply hp,
+    { exact hs c (mem_cons.2 (or.inl rfl)), },
+    { exact ih (λ b h, hs b (mem_cons.2 (or.inr h))), }, },
 end
 
 lemma sup_le_of_le_directed {α : Type*} [semilattice_sup_bot α] (s : set α)
@@ -186,8 +178,8 @@ lemma inf_def : s.inf f = (s.1.map f).inf := rfl
 @[simp] lemma inf_empty : (∅ : finset β).inf f = ⊤ :=
 fold_empty
 
-lemma le_inf_iff {a : α} : a ≤ s.inf f ↔ ∀b ∈ s, a ≤ f b :=
-@sup_le_iff (order_dual α) _ _ _ _ _
+@[simp] lemma inf_cons {b : β} (h : b ∉ s) : (cons b s h).inf f = f b ⊓ s.inf f :=
+@sup_cons (order_dual α) _ _ _ _ _ h
 
 @[simp] lemma inf_insert [decidable_eq β] {b : β} : (insert b s : finset β).inf f = f b ⊓ s.inf f :=
 fold_insert_idem
@@ -201,6 +193,9 @@ lemma inf_union [decidable_eq β] : (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.
 theorem inf_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀a∈s₂, f a = g a) : s₁.inf f = s₂.inf g :=
 by subst hs; exact finset.fold_congr hfg
 
+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
 
@@ -234,7 +229,11 @@ lemma inf_coe {P : α → Prop}
   {Ptop : P ⊤} {Pinf : ∀{{x y}}, P x → P y → P (x ⊓ y)}
   (t : finset β) (f : β → {x : α // P x}) :
   (@inf _ _ (subtype.semilattice_inf_top Ptop Pinf) t f : α) = t.inf (λ x, f x) :=
-by { classical, rw [comp_inf_eq_inf_comp coe]; intros; refl }
+@sup_coe (order_dual α) _ _ _ Ptop Pinf t f
+
+lemma of_inf_of_forall {p : α → Prop} (ht : p ⊤) (hp : ∀ (a₁ a₂ : α), p a₁ → p a₂ → p (a₁ ⊓ a₂))
+  (hs : ∀ b ∈ s, p (f b)) : p (s.inf f) :=
+@of_sup_of_forall (order_dual α) _ _ _ _ _ ht hp hs
 
 end inf
 
@@ -248,6 +247,185 @@ lemma exists_mem_eq_inf [complete_linear_order β] (s : finset α) (h : s.nonemp
   ∃ a, a ∈ s ∧ s.inf f = f a :=
 @exists_mem_eq_sup _ (order_dual β) _ _ h _
 
+section sup'
+variables [semilattice_sup α]
+
+lemma sup_of_mem {s : finset β} (f : β → α) {b : β} (h : b ∈ s) :
+  ∃ (a : α), s.sup (coe ∘ f : β → with_bot α) = ↑a :=
+Exists.imp (λ a, Exists.fst) (@le_sup (with_bot α) _ _ _ _ _ h (f b) rfl)
+
+/-- Given nonempty finset `s` in (possibly unbounded) join-semilattice `α` then `s.sup' H` is its
+supremum in `α` where `H` is a proof of nonemptiness. If `α` has a bottom element you may instead
+use `s.sup` which does not require `s` nonempty. -/
+def sup' (s : finset β) (H : s.nonempty) (f : β → α) : α :=
+option.get $ let ⟨b, hb⟩ := H in option.is_some_iff_exists.2 (sup_of_mem f hb)
+
+variables {s : finset β} (H : s.nonempty) (f : β → α)
+
+@[simp] lemma coe_sup' : ((s.sup' H f : α) : with_bot α) = s.sup (coe ∘ f) :=
+by rw [sup', ←with_bot.some_eq_coe, option.some_get]
+
+@[simp] lemma sup'_cons {b : β} {hb : b ∉ s} {h : (cons b s hb).nonempty} :
+  (cons b s hb).sup' h f = f b ⊔ s.sup' H f :=
+by { rw ←with_bot.coe_eq_coe, simp only [coe_sup', sup_cons, with_bot.coe_sup], }
+
+@[simp] lemma sup'_insert [decidable_eq β] {b : β} {h : (insert b s).nonempty} :
+  (insert b s).sup' h f = f b ⊔ s.sup' H f :=
+by { rw ←with_bot.coe_eq_coe, simp only [coe_sup', sup_insert, with_bot.coe_sup], }
+
+@[simp] lemma sup'_singleton {b : β} {h : ({b} : finset β).nonempty} :
+  ({b} : finset β).sup' h f = f b := rfl
+
+lemma sup'_le {a : α} (hs : ∀ b ∈ s, f b ≤ a) : s.sup' H f ≤ a :=
+by { rw [←with_bot.coe_le_coe, coe_sup'], exact sup_le (λ b h, with_bot.coe_le_coe.2 $ hs b h), }
+
+lemma le_sup' {b : β} (h : b ∈ s) : f b ≤ s.sup' ⟨b, h⟩ f :=
+by { rw [←with_bot.coe_le_coe, coe_sup'], exact le_sup h, }
+
+@[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)
+
+@[simp] lemma sup'_lt_iff [is_total α (≤)] {a : α} : s.sup' H f < a ↔ (∀ b ∈ s, f b < a) :=
+begin
+  rw [←with_bot.coe_lt_coe, coe_sup', sup_lt_iff (with_bot.bot_lt_coe a)],
+  exact ball_congr (λ b hb, with_bot.coe_lt_coe),
+end
+
+lemma of_sup'_of_forall {p : α → Prop} (hp : ∀ (a₁ a₂ : α), p a₁ → p a₂ → p (a₁ ⊔ a₂))
+  (hs : ∀ b ∈ s, p (f b)) : p (s.sup' H f) :=
+begin
+  show @with_bot.rec_bot_coe α (λ _, Prop) true p ↑(s.sup' H f),
+  rw coe_sup',
+  refine of_sup_of_forall trivial _ hs,
+  intros a₁ a₂ h₁ h₂,
+  cases a₁,
+  { rw [with_bot.none_eq_bot, bot_sup_eq], exact h₂, },
+  { cases a₂, exact h₁, exact hp a₁ a₂ h₁ h₂, },
+end
+
+end sup'
+
+section inf'
+variables [semilattice_inf α]
+
+lemma inf_of_mem {s : finset β} (f : β → α) {b : β} (h : b ∈ s) :
+  ∃ (a : α), s.inf (coe ∘ f : β → with_top α) = ↑a :=
+@sup_of_mem (order_dual α) _ _ _ f _ h
+
+/-- Given nonempty finset `s` in (possibly unbounded) meet-semilattice `α` then `s.inf' H` is its
+infimum in `α` where `H` is a proof of nonemptiness. If `α` has a top element you may instead use
+`s.inf` which does not require `s` nonempty. -/
+def inf' (s : finset β) (H : s.nonempty) (f : β → α) : α :=
+@sup' (order_dual α) _ _ s H f
+
+variables {s : finset β} (H : s.nonempty) (f : β → α)
+
+@[simp] lemma coe_inf' : ((s.inf' H f : α) : with_top α) = s.inf (coe ∘ f) :=
+@coe_sup' (order_dual α) _ _ _ H f
+
+@[simp] lemma inf'_cons {b : β} {hb : b ∉ s} {h : (cons b s hb).nonempty} :
+  (cons b s hb).inf' h f = f b ⊓ s.inf' H f :=
+@sup'_cons (order_dual α) _ _ _ H f _ _ _
+
+@[simp] lemma inf'_insert [decidable_eq β] {b : β} {h : (insert b s).nonempty} :
+  (insert b s).inf' h f = f b ⊓ s.inf' H f :=
+@sup'_insert (order_dual α) _ _ _ H f _ _ _
+
+@[simp] lemma inf'_singleton {b : β} {h : ({b} : finset β).nonempty} :
+  ({b} : finset β).inf' h f = f b := rfl
+
+lemma le_inf' {a : α} (hs : ∀ b ∈ s, a ≤ f b) : a ≤ s.inf' H f :=
+@sup'_le (order_dual α) _ _ _ H f _ hs
+
+lemma inf'_le {b : β} (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b :=
+@le_sup' (order_dual α) _ _ _ f _ h
+
+@[simp] lemma le_inf'_iff {a : α} : a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b :=
+@sup'_le_iff (order_dual α) _ _ _ H f _
+
+@[simp] lemma lt_inf'_iff [is_total α (≤)] {a : α} : a < s.inf' H f ↔ (∀ b ∈ s, a < f b) :=
+@sup'_lt_iff (order_dual α) _ _ _ H f _ _
+
+lemma of_inf'_of_forall {p : α → Prop} (hp : ∀ (a₁ a₂ : α), p a₁ → p a₂ → p (a₁ ⊓ a₂))
+  (hs : ∀ b ∈ s, p (f b)) : p (s.inf' H f) :=
+@of_sup'_of_forall (order_dual α) _ _ _ H f _ hp hs
+
+end inf'
+
+section sup
+variable [semilattice_sup_bot α]
+
+lemma sup'_eq_sup {s : finset β} (H : s.nonempty) (f : β → α) : s.sup' H f = s.sup f :=
+le_antisymm (sup'_le H f (λ b, le_sup)) (sup_le (λ b, le_sup' f))
+
+lemma sup_closed_of_sup_closed {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : ↑t ⊆ s)
+  (h : ∀⦃a b⦄, a ∈ s → b ∈ s → a ⊔ b ∈ s) : t.sup id ∈ s :=
+sup'_eq_sup htne id ▸ of_sup'_of_forall _ _ h h_subset
+
+end sup
+
+section inf
+variable [semilattice_inf_top α]
+
+lemma inf'_eq_inf {s : finset β} (H : s.nonempty) (f : β → α) : s.inf' H f = s.inf f :=
+@sup'_eq_sup (order_dual α) _ _ _ H f
+
+lemma inf_closed_of_inf_closed {s : set α} (t : finset α) (htne : t.nonempty) (h_subset : ↑t ⊆ s)
+  (h : ∀⦃a b⦄, a ∈ s → b ∈ s → a ⊓ b ∈ s) : t.inf id ∈ s :=
+@sup_closed_of_sup_closed (order_dual α) _ _ t htne h_subset h
+
+end inf
+
+section sup
+variables {C : β → Type*} [Π (b : β), semilattice_sup_bot (C b)]
+
+protected lemma sup_apply (s : finset α) (f : α → Π (b : β), C b) (b : β) :
+  s.sup f b = s.sup (λ a, f a b) :=
+begin
+  induction s using finset.cons_induction with c s hc ih,
+  { refl, },
+  { rw [sup_cons, sup_cons, _root_.sup_apply, ih], },
+end
+
+end sup
+
+section inf
+variables {C : β → Type*} [Π (b : β), semilattice_inf_top (C b)]
+
+protected lemma inf_apply (s : finset α) (f : α → Π (b : β), C b) (b : β) :
+  s.inf f b = s.inf (λ a, f a b) :=
+@finset.sup_apply _ _ (λ b, order_dual (C b)) _ s f b
+
+end inf
+
+section sup'
+variables {C : β → Type*} [Π (b : β), semilattice_sup (C b)]
+
+lemma sup'_apply {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
+  s.sup' H f b = s.sup' H (λ a, f a b) :=
+begin
+  rw [←with_bot.coe_eq_coe, coe_sup'],
+  let g := @with_bot.rec_bot_coe (Π b, C b) (λ _, with_bot (C b)) ⊥ (λ f, ↑(f b)),
+  show g ↑(s.sup' H f) = s.sup (λ a, g ↑(f a)),
+  rw coe_sup',
+  refine comp_sup_eq_sup_comp g _ rfl,
+  intros f₁ f₂,
+  cases f₁,
+  { rw [with_bot.none_eq_bot, bot_sup_eq], exact bot_sup_eq.symm, },
+  { cases f₂, refl, refl, },
+end
+
+end sup'
+
+section inf'
+variables {C : β → Type*} [Π (b : β), semilattice_inf (C b)]
+
+lemma inf'_apply {s : finset α} (H : s.nonempty) (f : α → Π (b : β), C b) (b : β) :
+  s.inf' H f b = s.inf' H (λ a, f a b) :=
+@sup'_apply _ _ (λ b, order_dual (C b)) _ _ H f b
+
+end inf'
+
 /-! ### max and min of finite sets -/
 section max_min
 variables [linear_order α]

src/data/mv_polynomial/variables.lean

@@ -199,7 +199,7 @@ lemma degrees_map [comm_semiring S] (p : mv_polynomial σ R) (f : R →+* S) :
 begin
   dsimp only [degrees],
   apply multiset.subset_of_le,
-  convert finset.sup_subset _ _,
+  apply finset.sup_mono,
   apply mv_polynomial.support_map_subset
 end