feat(Order/PartialSups): golf, add lemmas (#8138)

- Add `partialSups_iff_forall` and `partialSups_le_iff`.
- Use them to golf some proofs.
- Drop `partialSups_apply_mono`
  because it's just `(partialSups f).mono`.
- Add `disjoint_partialSups_left` and `disjoint_partialSups_right`.

Motivated by `partialSups_le_iff`
from the Mandelbrot Set Connectedness Project.

Co-authored-by: @girving

Mathlib/Order/PartialSups.lean

@@ -59,34 +59,38 @@ theorem partialSups_succ (f : ℕ → α) (n : ℕ) :
   rfl
 #align partial_sups_succ partialSups_succ
 
-theorem le_partialSups_of_le (f : ℕ → α) {m n : ℕ} (h : m ≤ n) : f m ≤ partialSups f n := by
-  induction' n with n ih
-  · rw [nonpos_iff_eq_zero.mp h, partialSups_zero]
-  · cases' h with h h
-    · exact le_sup_right
-    · exact (ih h).trans le_sup_left
+lemma partialSups_iff_forall {f : ℕ → α} (p : α → Prop)
+    (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) : ∀  {n : ℕ}, p (partialSups f n) ↔ ∀ k ≤ n, p (f k)
+  | 0 => by simp
+  | (n + 1) => by simp [hp, partialSups_iff_forall, ← Nat.lt_succ_iff, ← Nat.forall_lt_succ]
+
+@[simp]
+lemma partialSups_le_iff {f : ℕ → α} {n : ℕ} {a : α} : partialSups f n ≤ a ↔ ∀ k ≤ n, f k ≤ a :=
+  partialSups_iff_forall (· ≤ a) sup_le_iff
+
+theorem le_partialSups_of_le (f : ℕ → α) {m n : ℕ} (h : m ≤ n) : f m ≤ partialSups f n :=
+  partialSups_le_iff.1 le_rfl m h
 #align le_partial_sups_of_le le_partialSups_of_le
 
 theorem le_partialSups (f : ℕ → α) : f ≤ partialSups f := fun _n => le_partialSups_of_le f le_rfl
 #align le_partial_sups le_partialSups
 
 theorem partialSups_le (f : ℕ → α) (n : ℕ) (a : α) (w : ∀ m, m ≤ n → f m ≤ a) :
-    partialSups f n ≤ a := by
-  induction' n with n ih
-  · apply w 0 le_rfl
-  · exact sup_le (ih fun m p => w m (Nat.le_succ_of_le p)) (w (n + 1) le_rfl)
+    partialSups f n ≤ a :=
+  partialSups_le_iff.2 w
 #align partial_sups_le partialSups_le
 
+@[simp]
+lemma upperBounds_range_partialSups (f : ℕ → α) :
+    upperBounds (Set.range (partialSups f)) = upperBounds (Set.range f) := by
+  ext a
+  simp only [mem_upperBounds, Set.forall_range_iff, partialSups_le_iff]
+  exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩
+
 @[simp]
 theorem bddAbove_range_partialSups {f : ℕ → α} :
-    BddAbove (Set.range (partialSups f)) ↔ BddAbove (Set.range f) := by
-  apply exists_congr fun a => _
-  intro a
-  constructor
-  · rintro h b ⟨i, rfl⟩
-    exact (le_partialSups _ _).trans (h (Set.mem_range_self i))
-  · rintro h b ⟨i, rfl⟩
-    exact partialSups_le _ _ _ fun _ _ => h (Set.mem_range_self _)
+    BddAbove (Set.range (partialSups f)) ↔ BddAbove (Set.range f) :=
+  .of_eq <| congr_arg Set.Nonempty <| upperBounds_range_partialSups f
 #align bdd_above_range_partial_sups bddAbove_range_partialSups
 
 theorem Monotone.partialSups_eq {f : ℕ → α} (hf : Monotone f) : (partialSups f : ℕ → α) = f := by
@@ -96,16 +100,10 @@ theorem Monotone.partialSups_eq {f : ℕ → α} (hf : Monotone f) : (partialSup
   · rw [partialSups_succ, ih, sup_eq_right.2 (hf (Nat.le_succ _))]
 #align monotone.partial_sups_eq Monotone.partialSups_eq
 
-theorem partialSups_mono : Monotone (partialSups : (ℕ → α) → ℕ →o α) := by
-  rintro f g h n
-  induction' n with n ih
-  · exact h 0
-  · exact sup_le_sup ih (h _)
+theorem partialSups_mono : Monotone (partialSups : (ℕ → α) → ℕ →o α) := fun _f _g h _n ↦
+  partialSups_le_iff.2 fun k hk ↦ (h k).trans (le_partialSups_of_le _ hk)
 #align partial_sups_mono partialSups_mono
 
-theorem partialSups_apply_mono (f : ℕ → α) : Monotone (partialSups f) :=
-  fun n _ hnm => partialSups_le f n _ (fun _ hm'n => le_partialSups_of_le _ (hm'n.trans hnm))
-
 /-- `partialSups` forms a Galois insertion with the coercion from monotone functions to functions.
 -/
 def partialSups.gi : GaloisInsertion (partialSups : (ℕ → α) → ℕ →o α) (↑) where
@@ -120,42 +118,42 @@ def partialSups.gi : GaloisInsertion (partialSups : (ℕ → α) → ℕ →o α
 #align partial_sups.gi partialSups.gi
 
 theorem partialSups_eq_sup'_range (f : ℕ → α) (n : ℕ) :
-    partialSups f n = (Finset.range (n + 1)).sup' ⟨n, Finset.self_mem_range_succ n⟩ f := by
-  induction' n with n ih
-  · simp
-  · dsimp [partialSups] at ih ⊢
-    simp_rw [@Finset.range_succ n.succ]
-    rw [ih, Finset.sup'_insert, sup_comm]
+    partialSups f n = (Finset.range (n + 1)).sup' ⟨n, Finset.self_mem_range_succ n⟩ f :=
+  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]
 #align partial_sups_eq_sup'_range partialSups_eq_sup'_range
 
 end SemilatticeSup
 
 theorem partialSups_eq_sup_range [SemilatticeSup α] [OrderBot α] (f : ℕ → α) (n : ℕ) :
-    partialSups f n = (Finset.range (n + 1)).sup f := by
-  induction' n with n ih
-  · simp
-  · dsimp [partialSups] at ih ⊢
-    rw [Finset.range_succ, Finset.sup_insert, sup_comm, ih]
+    partialSups f n = (Finset.range (n + 1)).sup f :=
+  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]
 #align partial_sups_eq_sup_range partialSups_eq_sup_range
 
+@[simp]
+lemma disjoint_partialSups_left [DistribLattice α] [OrderBot α] {f : ℕ → α} {n : ℕ} {x : α} :
+    Disjoint (partialSups f n) x ↔ ∀ k ≤ n, Disjoint (f k) x :=
+  partialSups_iff_forall (Disjoint · x) disjoint_sup_left
+
+@[simp]
+lemma disjoint_partialSups_right [DistribLattice α] [OrderBot α] {f : ℕ → α} {n : ℕ} {x : α} :
+    Disjoint x (partialSups f n) ↔ ∀ k ≤ n, Disjoint x (f k) :=
+  partialSups_iff_forall (Disjoint x) disjoint_sup_right
+
 /- Note this lemma requires a distributive lattice, so is not useful (or true) in situations such as
 submodules. -/
 theorem partialSups_disjoint_of_disjoint [DistribLattice α] [OrderBot α] (f : ℕ → α)
-    (h : Pairwise (Disjoint on f)) {m n : ℕ} (hmn : m < n) : Disjoint (partialSups f m) (f n) := by
-  induction' m with m ih
-  · exact h hmn.ne
-  · rw [partialSups_succ, disjoint_sup_left]
-    exact ⟨ih (Nat.lt_of_succ_lt hmn), h hmn.ne⟩
+    (h : Pairwise (Disjoint on f)) {m n : ℕ} (hmn : m < n) : Disjoint (partialSups f m) (f n) :=
+  disjoint_partialSups_left.2 fun _k hk ↦ h <| (hk.trans_lt hmn).ne
 #align partial_sups_disjoint_of_disjoint partialSups_disjoint_of_disjoint
 
 section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice α]
 
-theorem partialSups_eq_ciSup_Iic (f : ℕ → α) (n : ℕ) : partialSups f n = ⨆ i : Set.Iic n, f i := by
-  have : Set.Iio (n + 1) = Set.Iic n := Set.ext fun _ => Nat.lt_succ_iff
-  rw [partialSups_eq_sup'_range, Finset.sup'_eq_csSup_image, Finset.coe_range, iSup, this]
-  simp only [Set.range, Subtype.exists, Set.mem_Iic, exists_prop, (· '' ·)]
+theorem partialSups_eq_ciSup_Iic (f : ℕ → α) (n : ℕ) : partialSups f n = ⨆ i : Set.Iic n, f i :=
+  eq_of_forall_ge_iff fun _ ↦ by
+    rw [ciSup_set_le_iff Set.nonempty_Iic ((Set.finite_le_nat _).image _).bddAbove,
+      partialSups_le_iff]; rfl
 #align partial_sups_eq_csupr_Iic partialSups_eq_ciSup_Iic
 
 @[simp]