refactor(data/finset/lattice): finset.{min,max} away from option (#15163

)

Switch to a `with_top`/`with_bot` based API. This avoids exposing `option`
as implementation detail.
Redefines `polynomial.degree` to use `coe` instead of `some`





Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -45,9 +45,9 @@ begin
   -- Given an index `i`, produce the set of increasing (resp., decreasing) subsequences which ends
   -- at `i`.
   let inc_sequences_ending_in : fin n → finset (finset (fin n)) :=
-    λ i, univ.powerset.filter (λ t, finset.max t = some i ∧ strict_mono_on f ↑t),
+    λ i, univ.powerset.filter (λ t, finset.max t = i ∧ strict_mono_on f ↑t),
   let dec_sequences_ending_in : fin n → finset (finset (fin n)) :=
-    λ i, univ.powerset.filter (λ t, finset.max t = some i ∧ strict_anti_on f ↑t),
+    λ i, univ.powerset.filter (λ t, finset.max t = i ∧ strict_anti_on f ↑t),
   -- The singleton sequence is in both of the above collections.
   -- (This is useful to show that the maximum length subsequence is at least 1, and that the set
   -- of subsequences is nonempty.)
@@ -96,7 +96,7 @@ begin
       rcases this with ⟨t, ht₁, ht₂⟩,
       rw mem_filter at ht₁,
       -- Ensure `t` ends at `i`.
-      have : i ∈ t.max,
+      have : t.max = i,
         simp [ht₁.2.1],
       -- Now our new subsequence is given by adding `j` at the end of `t`.
       refine ⟨insert j t, _, _⟩,
@@ -106,8 +106,8 @@ begin
         { rw mem_powerset, apply subset_univ },
         -- It ends at `j` since `i < j`.
         { convert max_insert,
-          rw [ht₁.2.1, option.lift_or_get_some_some, max_eq_left, with_top.some_eq_coe],
-          apply le_of_lt ‹i < j› },
+          rw [ht₁.2.1, max_eq_left],
+          apply with_bot.coe_le_coe.mpr (le_of_lt ‹i < j›) },
         -- To show it's increasing (i.e., `f` is monotone increasing on `t.insert j`), we do cases
         -- on what the possibilities could be - either in `t` or equals `j`.
         simp only [strict_mono_on, strict_anti_on, coe_insert, set.mem_insert_iff,
@@ -116,16 +116,16 @@ begin
         rintros x ⟨rfl | _⟩ y ⟨rfl | _⟩ _,
         { apply (irrefl _ ‹j < j›).elim },
         { exfalso,
-          apply not_le_of_lt (trans ‹i < j› ‹j < y›) (le_max_of_mem ‹y ∈ t› ‹i ∈ t.max›) },
+          apply not_le_of_lt (trans ‹i < j› ‹j < y›) (le_max_of_mem ‹y ∈ t› ‹t.max = i›) },
         { apply lt_of_le_of_lt _ ‹f i < f j› <|> apply lt_of_lt_of_le ‹f j < f i› _,
-          rcases lt_or_eq_of_le (le_max_of_mem ‹x ∈ t› ‹i ∈ t.max›) with _ | rfl,
-          { apply le_of_lt (ht₁.2.2 ‹x ∈ t› (mem_of_max ‹i ∈ t.max›) ‹x < i›) },
+          rcases lt_or_eq_of_le (le_max_of_mem ‹x ∈ t› ‹t.max = i›) with _ | rfl,
+          { apply le_of_lt (ht₁.2.2 ‹x ∈ t› (mem_of_max ‹t.max = i›) ‹x < i›) },
           { refl } },
         { apply ht₁.2.2 ‹x ∈ t› ‹y ∈ t› ‹x < y› } },
       -- Finally show that this new subsequence is one longer than the old one.
       { rw [card_insert_of_not_mem, ht₂],
         intro _,
-        apply not_le_of_lt ‹i < j› (le_max_of_mem ‹j ∈ t› ‹i ∈ t.max›) } } },
+        apply not_le_of_lt ‹i < j› (le_max_of_mem ‹j ∈ t› ‹t.max = i›) } } },
       -- Finished both goals!
   -- Now that we have uniqueness of each label, it remains to do some counting to finish off.
   -- Suppose all the labels are small.

src/combinatorics/simple_graph/basic.lean

@@ -847,7 +847,7 @@ The key properties of this are given in `exists_minimal_degree_vertex`, `min_deg
 and `le_min_degree_of_forall_le_degree`.
 -/
 def min_degree [decidable_rel G.adj] : ℕ :=
-option.get_or_else (univ.image (λ v, G.degree v)).min 0
+with_top.untop' 0 (univ.image (λ v, G.degree v)).min
 
 /--
 There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as
@@ -866,8 +866,7 @@ lemma min_degree_le_degree [decidable_rel G.adj] (v : V) : G.min_degree ≤ G.de
 begin
   obtain ⟨t, ht⟩ := finset.min_of_mem (mem_image_of_mem (λ v, G.degree v) (mem_univ v)),
   have := finset.min_le_of_mem (mem_image_of_mem _ (mem_univ v)) ht,
-  rw option.mem_def at ht,
-  rwa [min_degree, ht, option.get_or_else_some],
+  rwa [min_degree, ht]
 end
 
 /--
@@ -899,7 +898,6 @@ begin
   have ht₂ := mem_of_max ht,
   simp only [mem_image, mem_univ, exists_prop_of_true] at ht₂,
   rcases ht₂ with ⟨v, rfl⟩,
-  rw option.mem_def at ht,
   refine ⟨v, _⟩,
   rw [max_degree, ht],
   refl
@@ -910,7 +908,7 @@ lemma degree_le_max_degree [decidable_rel G.adj] (v : V) : G.degree v ≤ G.max_
 begin
   obtain ⟨t, ht : _ = _⟩ := finset.max_of_mem (mem_image_of_mem (λ v, G.degree v) (mem_univ v)),
   have := finset.le_max_of_mem (mem_image_of_mem _ (mem_univ v)) ht,
-  rwa [max_degree, ht, option.get_or_else_some],
+  rwa [max_degree, ht],
 end
 
 /--

src/data/finset/lattice.lean

@@ -777,105 +777,104 @@ section max_min
 variables [linear_order α]
 
 /-- Let `s` be a finset in a linear order. Then `s.max` is the maximum of `s` if `s` is not empty,
-and `none` otherwise. It belongs to `option α`. If you want to get an element of `α`, see
+and `⊥` otherwise. It belongs to `with_bot α`. If you want to get an element of `α`, see
 `s.max'`. -/
-protected def max : finset α → option α :=
-fold (option.lift_or_get max) none some
+protected def max : finset α → with_bot α :=
+fold max ⊥ coe
 
 theorem max_eq_sup_with_bot (s : finset α) :
-  s.max = @sup (with_bot α) α _ _ s some := rfl
+  s.max = sup s coe := rfl
 
-@[simp] theorem max_empty : (∅ : finset α).max = none := rfl
+@[simp] theorem max_empty : (∅ : finset α).max = ⊥ := rfl
 
 @[simp] theorem max_insert {a : α} {s : finset α} :
-  (insert a s).max = option.lift_or_get max (some a) s.max := fold_insert_idem
+  (insert a s).max = max a s.max := fold_insert_idem
 
-@[simp] theorem max_singleton {a : α} : finset.max {a} = some a :=
+@[simp] theorem max_singleton {a : α} : finset.max {a} = (a : with_bot α) :=
 by { rw [← insert_emptyc_eq], exact max_insert }
 
-theorem max_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.max :=
+theorem max_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ (b : α), s.max = b :=
 (@le_sup (with_bot α) _ _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
 
-theorem max_of_nonempty {s : finset α} (h : s.nonempty) : ∃ a, a ∈ s.max :=
+theorem max_of_nonempty {s : finset α} (h : s.nonempty) : ∃ (a : α), s.max = a :=
 let ⟨a, ha⟩ := h in max_of_mem ha
 
-theorem max_eq_none {s : finset α} : s.max = none ↔ s = ∅ :=
+theorem max_eq_bot {s : finset α} : s.max = ⊥ ↔ s = ∅ :=
 ⟨λ h, s.eq_empty_or_nonempty.elim id
   (λ H, let ⟨a, ha⟩ := max_of_nonempty H in by rw h at ha; cases ha),
   λ h, h.symm ▸ max_empty⟩
 
-theorem mem_of_max {s : finset α} : ∀ {a : α}, a ∈ s.max → a ∈ s :=
+theorem mem_of_max {s : finset α} : ∀ {a : α}, s.max = a → a ∈ s :=
 finset.induction_on s (λ _ H, by cases H)
-  (λ b s _ (ih : ∀ {a}, a ∈ s.max → a ∈ s) a (h : a ∈ (insert b s).max),
+  (λ b s _ (ih : ∀ {a : α}, s.max = a → a ∈ s) a (h : (insert b s).max = a),
   begin
     by_cases p : b = a,
     { induction p, exact mem_insert_self b s },
-    { cases option.lift_or_get_choice max_choice (some b) s.max with q q;
+    { cases max_choice ↑b s.max with q q;
       rw [max_insert, q] at h,
       { cases h, cases p rfl },
       { exact mem_insert_of_mem (ih h) } }
   end)
 
-theorem le_max_of_mem {s : finset α} {a b : α} (h₁ : a ∈ s) (h₂ : b ∈ s.max) : a ≤ b :=
+theorem le_max_of_mem {s : finset α} {a b : α} (h₁ : a ∈ s) (h₂ : s.max = b) : a ≤ b :=
 by rcases @le_sup (with_bot α) _ _ _ _ _ _ h₁ _ rfl with ⟨b', hb, ab⟩;
    cases h₂.symm.trans hb; assumption
 
 /-- Let `s` be a finset in a linear order. Then `s.min` is the minimum of `s` if `s` is not empty,
-and `none` otherwise. It belongs to `option α`. If you want to get an element of `α`, see
+and `⊤` otherwise. It belongs to `with_top α`. If you want to get an element of `α`, see
 `s.min'`. -/
-protected def min : finset α → option α :=
-fold (option.lift_or_get min) none some
+protected def min : finset α → with_top α :=
+fold min ⊤ coe
 
 theorem min_eq_inf_with_top (s : finset α) :
-  s.min = @inf (with_top α) α _ _ s some := rfl
+  s.min = inf s coe := rfl
 
-@[simp] theorem min_empty : (∅ : finset α).min = none := rfl
+@[simp] theorem min_empty : (∅ : finset α).min = ⊤ := rfl
 
 @[simp] theorem min_insert {a : α} {s : finset α} :
-  (insert a s).min = option.lift_or_get min (some a) s.min :=
+  (insert a s).min = min ↑a s.min :=
 fold_insert_idem
 
-@[simp] theorem min_singleton {a : α} : finset.min {a} = some a :=
+@[simp] theorem min_singleton {a : α} : finset.min {a} = (a : with_top α) :=
 by { rw ← insert_emptyc_eq, exact min_insert }
 
-theorem min_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b, b ∈ s.min :=
+theorem min_of_mem {s : finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.min = b :=
 (@inf_le (with_top α) _ _ _ _ _ _ h _ rfl).imp $ λ b, Exists.fst
 
-theorem min_of_nonempty {s : finset α} (h : s.nonempty) : ∃ a, a ∈ s.min :=
+theorem min_of_nonempty {s : finset α} (h : s.nonempty) : ∃ a : α, s.min = a :=
 let ⟨a, ha⟩ := h in min_of_mem ha
 
-theorem min_eq_none {s : finset α} : s.min = none ↔ s = ∅ :=
+theorem min_eq_top {s : finset α} : s.min = ⊤ ↔ s = ∅ :=
 ⟨λ h, s.eq_empty_or_nonempty.elim id
   (λ H, let ⟨a, ha⟩ := min_of_nonempty H in by rw h at ha; cases ha),
   λ h, h.symm ▸ min_empty⟩
 
-theorem mem_of_min {s : finset α} : ∀ {a : α}, a ∈ s.min → a ∈ s := @mem_of_max αᵒᵈ _ s
+theorem mem_of_min {s : finset α} : ∀ {a : α}, s.min = a → a ∈ s := @mem_of_max αᵒᵈ _ s
 
-theorem min_le_of_mem {s : finset α} {a b : α} (h₁ : b ∈ s) (h₂ : a ∈ s.min) : a ≤ b :=
+theorem min_le_of_mem {s : finset α} {a b : α} (h₁ : b ∈ s) (h₂ : s.min = a) : a ≤ b :=
 by rcases @inf_le (with_top α) _ _ _ _ _ _ h₁ _ rfl with ⟨b', hb, ab⟩;
    cases h₂.symm.trans hb; assumption
 
 /-- Given a nonempty finset `s` in a linear order `α `, then `s.min' h` is its minimum, as an
 element of `α`, where `h` is a proof of nonemptiness. Without this assumption, use instead `s.min`,
-taking values in `option α`. -/
+taking values in `with_top α`. -/
 def min' (s : finset α) (H : s.nonempty) : α :=
-@option.get _ s.min $
-  let ⟨k, hk⟩ := H in
-  let ⟨b, hb⟩ := min_of_mem hk in by simp at hb; simp [hb]
+with_top.untop s.min $ mt min_eq_top.1 H.ne_empty
 
 /-- 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 `option α`. -/
+taking values in `with_bot α`. -/
 def max' (s : finset α) (H : s.nonempty) : α :=
-@option.get _ s.max $
+with_bot.unbot s.max $
   let ⟨k, hk⟩ := H in
-  let ⟨b, hb⟩ := max_of_mem hk in by simp at hb; simp [hb]
+  let ⟨b, hb⟩ := max_of_mem hk in by simp [hb]
 
 variables (s : finset α) (H : s.nonempty) {x : α}
 
 theorem min'_mem : s.min' H ∈ s := mem_of_min $ by simp [min']
 
-theorem min'_le (x) (H2 : x ∈ s) : s.min' ⟨x, H2⟩ ≤ x := min_le_of_mem H2 $ option.get_mem _
+theorem min'_le (x) (H2 : x ∈ s) : s.min' ⟨x, H2⟩ ≤ x :=
+min_le_of_mem H2 (with_top.coe_untop _ _).symm
 
 theorem le_min' (x) (H2 : ∀ y ∈ s, x ≤ y) : x ≤ s.min' H := H2 _ $ min'_mem _ _
 
@@ -891,7 +890,8 @@ by simp [min']
 
 theorem max'_mem : s.max' H ∈ s := mem_of_max $ by simp [max']
 
-theorem le_max' (x) (H2 : x ∈ s) : x ≤ s.max' ⟨x, H2⟩ := le_max_of_mem H2 $ option.get_mem _
+theorem le_max' (x) (H2 : x ∈ s) : x ≤ s.max' ⟨x, H2⟩ :=
+le_max_of_mem H2 (with_bot.coe_unbot _ _).symm
 
 theorem max'_le (x) (H2 : ∀ y ∈ s, y ≤ x) : s.max' H ≤ x := H2 _ $ max'_mem _ _
 

src/data/mv_polynomial/equiv.lean

@@ -460,7 +460,6 @@ begin
   have h' : (fin_succ_equiv R n f).support.sup (λ x , x)  = degree_of 0 f,
   { rw [degree_of_eq_sup, fin_succ_equiv_support f, finset.sup_image] },
   rw [polynomial.degree, ← h', finset.coe_sup_of_nonempty (support_fin_succ_equiv_nonempty h)],
-  congr,
 end
 
 lemma nat_degree_fin_succ_equiv (f : mv_polynomial (fin (n + 1)) R) :

src/data/polynomial/degree/definitions.lean

@@ -34,7 +34,7 @@ variables [semiring R] {p q r : R[X]}
 /-- `degree p` is the degree of the polynomial `p`, i.e. the largest `X`-exponent in `p`.
 `degree p = some n` when `p ≠ 0` and `n` is the highest power of `X` that appears in `p`, otherwise
 `degree 0 = ⊥`. -/
-def degree (p : R[X]) : with_bot ℕ := p.support.sup some
+def degree (p : R[X]) : with_bot ℕ := p.support.sup coe
 
 lemma degree_lt_wf : well_founded (λp q : R[X], degree p < degree q) :=
 inv_image.wf degree (with_bot.well_founded_lt nat.lt_wf)
@@ -70,8 +70,7 @@ lemma monic.coeff_nat_degree {p : R[X]} (hp : p.monic) : p.coeff p.nat_degree =
 @[simp] lemma coeff_nat_degree : coeff p (nat_degree p) = leading_coeff p := rfl
 
 lemma degree_eq_bot : degree p = ⊥ ↔ p = 0 :=
-⟨λ h, by rw [degree, ← max_eq_sup_with_bot] at h;
-  exact support_eq_empty.1 (max_eq_none.1 h),
+⟨λ h, support_eq_empty.1 (finset.max_eq_bot.1 h),
 λ h, h.symm ▸ rfl⟩
 
 @[nontriviality] lemma degree_of_subsingleton [subsingleton R] : degree p = ⊥ :=

src/data/polynomial/degree/trailing_degree.lean

@@ -66,8 +66,7 @@ by unfold trailing_monic; apply_instance
 @[simp] lemma nat_trailing_degree_zero : nat_trailing_degree (0 : R[X]) = 0 := rfl
 
 lemma trailing_degree_eq_top : trailing_degree p = ⊤ ↔ p = 0 :=
-⟨λ h, by rw [trailing_degree, ← min_eq_inf_with_top] at h;
-  exact support_eq_empty.1 (min_eq_none.1 h),
+⟨λ h, support_eq_empty.1 (finset.min_eq_top.1 h),
 λ h, by simp [h]⟩
 
 lemma trailing_degree_eq_nat_trailing_degree (hp : p ≠ 0) :

src/order/bounded_order.lean

@@ -547,6 +547,18 @@ def rec_bot_coe {C : with_bot α → Sort*} (h₁ : C ⊥) (h₂ : Π (a : α),
   Π (n : with_bot α), C n :=
 option.rec h₁ h₂
 
+@[simp] lemma rec_bot_coe_bot {C : with_bot α → Sort*} (d : C ⊥) (f : Π (a : α), C a) :
+  @rec_bot_coe _ C d f ⊥ = d := rfl
+@[simp] lemma rec_bot_coe_coe {C : with_bot α → Sort*} (d : C ⊥) (f : Π (a : α), C a)
+  (x : α) : @rec_bot_coe _ C d f ↑x = f x := rfl
+
+/-- Specialization of `option.get_or_else` to values in `with_bot α` that respects API boundaries.
+-/
+def unbot' (d : α) (x : with_bot α) : α := rec_bot_coe d id x
+
+@[simp] lemma unbot'_bot {α} (d : α) : unbot' d ⊥ = d := rfl
+@[simp] lemma unbot'_coe {α} (d x : α) : unbot' d x = x := rfl
+
 @[norm_cast] lemma coe_eq_coe : (a : with_bot α) = b ↔ a = b := option.some_inj
 
 /-- Lift a map `f : α → β` to `with_bot α → with_bot β`. Implemented using `option.map`. -/
@@ -838,6 +850,18 @@ def rec_top_coe {C : with_top α → Sort*} (h₁ : C ⊤) (h₂ : Π (a : α),
   Π (n : with_top α), C n :=
 option.rec h₁ h₂
 
+@[simp] lemma rec_top_coe_top {C : with_top α → Sort*} (d : C ⊤) (f : Π (a : α), C a) :
+  @rec_top_coe _ C d f ⊤ = d := rfl
+@[simp] lemma rec_top_coe_coe {C : with_top α → Sort*} (d : C ⊤) (f : Π (a : α), C a)
+  (x : α) : @rec_top_coe _ C d f ↑x = f x := rfl
+
+/-- Specialization of `option.get_or_else` to values in `with_top α` that respects API boundaries.
+-/
+def untop' (d : α) (x : with_top α) : α := rec_top_coe d id x
+
+@[simp] lemma untop'_top {α} (d : α) : untop' d ⊤ = d := rfl
+@[simp] lemma untop'_coe {α} (d x : α) : untop' d x = x := rfl
+
 @[norm_cast] lemma coe_eq_coe : (a : with_top α) = b ↔ a = b := option.some_inj
 
 /-- Lift a map `f : α → β` to `with_top α → with_top β`. Implemented using `option.map`. -/

src/ring_theory/polynomial/basic.lean

@@ -81,7 +81,7 @@ end
 theorem mem_degree_lt {n : ℕ} {f : R[X]} :
   f ∈ degree_lt R n ↔ degree f < n :=
 by { simp_rw [degree_lt, submodule.mem_infi, linear_map.mem_ker, degree,
-    finset.sup_lt_iff (with_bot.bot_lt_coe n), mem_support_iff, with_bot.some_eq_coe,
+    finset.sup_lt_iff (with_bot.bot_lt_coe n), mem_support_iff,
     with_bot.coe_lt_coe, lt_iff_not_le, ne, not_imp_not], refl }
 
 @[mono] theorem degree_lt_mono {m n : ℕ} (H : m ≤ n) :