refactor(data/finset/lattice): sup' and inf' without option (#15195)

Hide the option API further, by using `unbot` and `untop`.





Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>

src/data/finset/lattice.lean

@@ -500,12 +500,12 @@ Exists.imp (λ a, Exists.fst) (@le_sup (with_bot α) _ _ _ _ _ _ h (f b) rfl)
 unbounded) join-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a bottom element
 you may instead use `finset.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)
+with_bot.unbot (s.sup (coe ∘ f)) (by simpa using H)
 
 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]
+by rw [sup', with_bot.coe_unbot]
 
 @[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 :=
@@ -544,15 +544,16 @@ lemma comp_sup'_eq_sup'_comp [semilattice_sup γ] {s : finset β} (H : s.nonempt
   g (s.sup' H f) = s.sup' H (g ∘ f) :=
 begin
   rw [←with_bot.coe_eq_coe, coe_sup'],
-  let g' : with_bot α → with_bot γ := with_bot.rec_bot_coe ⊥ (λ x, ↑(g x)),
+  let g' := with_bot.map g,
   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,
-    exact congr_arg coe (g_sup f₁ f₂), },
+  induction f₁ using with_bot.rec_bot_coe,
+  { rw [bot_sup_eq], exact bot_sup_eq.symm, },
+  { induction f₂ using with_bot.rec_bot_coe,
+    { refl },
+    { exact congr_arg coe (g_sup f₁ f₂) } }
 end
 
 lemma sup'_induction {p : α → Prop} (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂))
@@ -580,6 +581,11 @@ begin
   simp only [sup'_le_iff, h₂] { contextual := tt }
 end
 
+@[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) :=
+by rw [←with_bot.coe_eq_coe, coe_sup', sup_map, coe_sup']
+
 end sup'
 
 section inf'
@@ -593,7 +599,7 @@ lemma inf_of_mem {s : finset β} (f : β → α) {b : β} (h : b ∈ s) :
 unbounded) meet-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a top element you
 may instead use `finset.inf` which does not require `s` nonempty. -/
 def inf' (s : finset β) (H : s.nonempty) (f : β → α) : α :=
-@sup' αᵒᵈ _ _ s H f
+with_top.untop (s.inf (coe ∘ f)) (by simpa using H)
 
 variables {s : finset β} (H : s.nonempty) (f : β → α) {a : α} {b : β}
 
@@ -602,19 +608,19 @@ variables {s : finset β} (H : s.nonempty) (f : β → α) {a : α} {b : β}
 
 @[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 αᵒᵈ _ _ _ H f _ _ _
+@sup'_cons αᵒᵈ _ _ _ H f _ _ h
 
 @[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 αᵒᵈ _ _ _ H f _ _ _
+@sup'_insert αᵒᵈ _ _ _ H f _ _ h
 
 @[simp] lemma inf'_singleton {b : β} {h : ({b} : finset β).nonempty} :
   ({b} : finset β).inf' h f = f b := rfl
 
 lemma le_inf' (hs : ∀ b ∈ s, a ≤ f b) : a ≤ s.inf' H f := @sup'_le αᵒᵈ _ _ _ H f _ hs
 lemma inf'_le (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b := @le_sup' αᵒᵈ _ _ _ f _ h
 
-@[simp] lemma inf'_const (a : α) : s.inf' H (λ b, a) = a := @sup'_const αᵒᵈ _ _ _ _ _
+@[simp] lemma inf'_const (a : α) : s.inf' H (λ b, a) = a := @sup'_const αᵒᵈ _ _ _ H _
 
 @[simp] lemma le_inf'_iff : a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b := @sup'_le_iff αᵒᵈ _ _ _ H f _
 
@@ -640,6 +646,11 @@ 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 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) :=
+@sup'_map αᵒᵈ _ _ _ _ _ _ hs hs'
+
 end inf'
 
 section sup
@@ -877,19 +888,17 @@ le_inf st
 element of `α`, where `h` is a proof of nonemptiness. Without this assumption, use instead `s.min`,
 taking values in `with_top α`. -/
 def min' (s : finset α) (H : s.nonempty) : α :=
-with_top.untop s.min $ mt min_eq_top.1 H.ne_empty
+inf' s H id
 
 /-- Given a nonempty finset `s` in a linear order `α `, then `s.max' h` is its maximum, as an
 element of `α`, where `h` is a proof of nonemptiness. Without this assumption, use instead `s.max`,
 taking values in `with_bot α`. -/
 def max' (s : finset α) (H : s.nonempty) : α :=
-with_bot.unbot s.max $
-  let ⟨k, hk⟩ := H in
-  let ⟨b, hb⟩ := max_of_mem hk in by simp [hb]
+sup' s H id
 
 variables (s : finset α) (H : s.nonempty) {x : α}
 
-theorem min'_mem : s.min' H ∈ s := mem_of_min $ by simp [min']
+theorem min'_mem : s.min' H ∈ s := mem_of_min $ by simp [min', finset.min]
 
 theorem min'_le (x) (H2 : x ∈ s) : s.min' ⟨x, H2⟩ ≤ x :=
 min_le_of_mem H2 (with_top.coe_untop _ _).symm
@@ -906,7 +915,7 @@ le_is_glb_iff (is_least_min' s H).is_glb
   ({a} : finset α).min' (singleton_nonempty _) = a :=
 by simp [min']
 
-theorem max'_mem : s.max' H ∈ s := mem_of_max $ by simp [max']
+theorem max'_mem : s.max' H ∈ s := mem_of_max $ by simp [max', finset.max]
 
 theorem le_max' (x) (H2 : x ∈ s) : x ≤ s.max' ⟨x, H2⟩ :=
 le_max_of_mem H2 (with_bot.coe_unbot _ _).symm

src/order/conditionally_complete_lattice.lean

@@ -1036,15 +1036,15 @@ end
 
 lemma inf'_eq_cInf_image [conditionally_complete_lattice β] (s : finset α) (H) (f : α → β) :
   s.inf' H f = Inf (f '' s) :=
-@sup'_eq_cSup_image _ βᵒᵈ _ _ _ _
+@sup'_eq_cSup_image _ βᵒᵈ _ _ H _
 
 lemma sup'_id_eq_cSup [conditionally_complete_lattice α] (s : finset α) (H) :
   s.sup' H id = Sup s :=
 by rw [sup'_eq_cSup_image s H, set.image_id]
 
 lemma inf'_id_eq_cInf [conditionally_complete_lattice α] (s : finset α) (H) :
   s.inf' H id = Inf s :=
-@sup'_id_eq_cSup αᵒᵈ _ _ _
+@sup'_id_eq_cSup αᵒᵈ _ _ H
 
 end finset