chore: tidy various files (#5449)

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -106,7 +106,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       rw [mem_filter] at ht₁
       -- Ensure `t` ends at `i`.
       have : t.max = i
-      simp [ht₁.2.1]
+      simp only [ht₁.2.1]
       -- Now our new subsequence is given by adding `j` at the end of `t`.
       refine' ⟨insert j t, _, _⟩
       -- First make sure it's valid, i.e., that this subsequence ends at `j` and is increasing

Mathlib/Algebra/Category/Mon/FilteredColimits.lean

@@ -19,13 +19,14 @@ import Mathlib.CategoryTheory.Limits.Types
 Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
 to preserve _filtered_ colimits.
 
-In this file, we start with a small filtered category `J` and a functor `F : J ⥤ Mon`.
-We then construct a monoid structure on the colimit of `F ⋙ forget Mon` (in `Type`), thereby
-showing that the forgetful functor `forget Mon` preserves filtered colimits. Similarly for `AddMon`,
-`CommMon` and `AddCommMon`.
+In this file, we start with a small filtered category `J` and a functor `F : J ⥤ MonCat`.
+We then construct a monoid structure on the colimit of `F ⋙ forget MonCat` (in `Type`), thereby
+showing that the forgetful functor `forget MonCat` preserves filtered colimits. Similarly for
+`AddMonCat`, `CommMonCat` and `AddCommMonCat`.
 
 -/
 
+set_option linter.uppercaseLean3 false
 
 universe v u
 
@@ -47,36 +48,30 @@ section
 -- `M.mk` below, without passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] (F : J ⥤ MonCat.{max v u})
 
-/-- The colimit of `F ⋙ forget Mon` in the category of types.
+/-- The colimit of `F ⋙ forget MonCat` in the category of types.
 In the following, we will construct a monoid structure on `M`.
 -/
 @[to_additive
       "The colimit of `F ⋙ forget AddMon` in the category of types.
       In the following, we will construct an additive monoid structure on `M`."]
 abbrev M : TypeMax.{v, u} :=
   Types.Quot (F ⋙ forget MonCat)
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.M MonCat.FilteredColimits.M
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.M AddMonCat.FilteredColimits.M
 
 /-- The canonical projection into the colimit, as a quotient type. -/
 @[to_additive "The canonical projection into the colimit, as a quotient type."]
 abbrev M.mk : (Σ j, F.obj j) → M.{v, u} F :=
   Quot.mk (Types.Quot.Rel (F ⋙ forget MonCat))
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.M.mk MonCat.FilteredColimits.M.mk
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.M.mk AddMonCat.FilteredColimits.M.mk
 
 @[to_additive]
 theorem M.mk_eq (x y : Σ j, F.obj j)
     (h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) :
   M.mk.{v, u} F x = M.mk F y :=
   Quot.EqvGen_sound (Types.FilteredColimit.eqvGen_quot_rel_of_rel (F ⋙ forget MonCat) x y h)
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.M.mk_eq MonCat.FilteredColimits.M.mk_eq
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.M.mk_eq AddMonCat.FilteredColimits.M.mk_eq
 
 variable [IsFiltered J]
@@ -89,9 +84,7 @@ variable [IsFiltered J]
   define the \"zero\" in the colimit as the equivalence class of `⟨j₀, 0 : F.obj j₀⟩`."]
 noncomputable instance colimitOne :
   One (M.{v, u} F) where one := M.mk F ⟨IsFiltered.Nonempty.some,1⟩
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_has_one MonCat.FilteredColimits.colimitOne
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_has_zero AddMonCat.FilteredColimits.colimitZero
 
 /-- The definition of the "one" in the colimit is independent of the chosen object of `J`.
@@ -106,9 +99,7 @@ theorem colimit_one_eq (j : J) : (1 : M.{v, u} F) = M.mk F ⟨j, 1⟩ := by
   apply M.mk_eq
   refine' ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, _⟩
   simp
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_one_eq MonCat.FilteredColimits.colimit_one_eq
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_zero_eq AddMonCat.FilteredColimits.colimit_zero_eq
 
 /-- The "unlifted" version of multiplication in the colimit. To multiply two dependent pairs
@@ -122,9 +113,7 @@ and multiply them there.
 noncomputable def colimitMulAux (x y : Σ j, F.obj j) : M.{v, u} F :=
   M.mk F ⟨IsFiltered.max x.fst y.fst, F.map (IsFiltered.leftToMax x.1 y.1) x.2 *
     F.map (IsFiltered.rightToMax x.1 y.1) y.2⟩
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_mul_aux MonCat.FilteredColimits.colimitMulAux
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_aux AddMonCat.FilteredColimits.colimitAddAux
 
 /-- Multiplication in the colimit is well-defined in the left argument. -/
@@ -149,9 +138,7 @@ theorem colimitMulAux_eq_of_rel_left {x x' y : Σ j, F.obj j}
   congr 1
   change F.map _ (F.map _ _) = F.map _ (F.map _ _)
   rw [hfg]
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_mul_aux_eq_of_rel_left MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_aux_eq_of_rel_left AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_left
 
 /-- Multiplication in the colimit is well-defined in the right argument. -/
@@ -176,9 +163,7 @@ theorem colimitMulAux_eq_of_rel_right {x y y' : Σ j, F.obj j}
   congr 1
   change F.map _ (F.map _ _) = F.map _ (F.map _ _)
   rw [hfg]
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_mul_aux_eq_of_rel_right MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_aux_eq_of_rel_right AddMonCat.FilteredColimits.colimitAddAux_eq_of_rel_right
 
 /-- Multiplication in the colimit. See also `colimitMulAux`. -/
@@ -194,9 +179,7 @@ noncomputable instance colimitMul : Mul (M.{v, u} F) :=
       apply colimitMulAux_eq_of_rel_left
       apply Types.FilteredColimit.rel_of_quot_rel
       exact h }
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_has_mul MonCat.FilteredColimits.colimitMul
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_has_add AddMonCat.FilteredColimits.colimitAdd
 
 /-- Multiplication in the colimit is independent of the chosen "maximum" in the filtered category.
@@ -220,9 +203,7 @@ theorem colimit_mul_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1
   change (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _ =
     (F.map _ ≫ F.map _) _ * (F.map _ ≫ F.map _) _
   simp_rw [← F.map_comp, h₁, h₂]
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_mul_mk_eq MonCat.FilteredColimits.colimit_mul_mk_eq
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_mk_eq AddMonCat.FilteredColimits.colimit_add_mk_eq
 
 @[to_additive]
@@ -271,19 +252,15 @@ noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
       rw [F.map_id, show ∀ x, (𝟙 (F.obj (IsFiltered.max j₁ (IsFiltered.max j₂ j₃)))) x = x
         from fun _ => rfl, mul_assoc, MonoidHom.map_mul, F.map_comp, F.map_comp]
       rfl }
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_monoid MonCat.FilteredColimits.colimitMonoid
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_monoid AddMonCat.FilteredColimits.colimitAddMonoid
 
 /-- The bundled monoid giving the filtered colimit of a diagram. -/
 @[to_additive
   "The bundled additive monoid giving the filtered colimit of a diagram."]
 noncomputable def colimit : MonCat.{max v u} :=
   MonCat.of (M.{v, u} F)
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit MonCat.FilteredColimits.colimit
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit AddMonCat.FilteredColimits.colimit
 
 /-- The monoid homomorphism from a given monoid in the diagram to the colimit monoid. -/
@@ -297,28 +274,22 @@ def coconeMorphism (j : J) : F.obj j ⟶ colimit.{v, u} F where
     convert (colimit_mul_mk_eq.{v, u} F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 j) (𝟙 j)).symm
     rw [F.map_id]
     rfl
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.cocone_morphism MonCat.FilteredColimits.coconeMorphism
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.cocone_morphism AddMonCat.FilteredColimits.coconeMorphism
 
 @[to_additive (attr := simp)]
 theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
     F.map f ≫ coconeMorphism.{v, u} F j' = coconeMorphism F j :=
   MonoidHom.ext fun x => congr_fun ((Types.colimitCocone (F ⋙ forget MonCat)).ι.naturality f) x
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.cocone_naturality MonCat.FilteredColimits.cocone_naturality
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.cocone_naturality AddMonCat.FilteredColimits.cocone_naturality
 
 /-- The cocone over the proposed colimit monoid. -/
 @[to_additive "The cocone over the proposed colimit additive monoid."]
 noncomputable def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι := { app := coconeMorphism F }
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_cocone MonCat.FilteredColimits.colimitCocone
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_cocone AddMonCat.FilteredColimits.colimitCocone
 
 /-- Given a cocone `t` of `F`, the induced monoid homomorphism from the colimit to the cocone point.
@@ -349,12 +320,10 @@ def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt where
     -- so can't rewrite `t.w_apply`
     congr 1 <;>
     exact t.w_apply _ _
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_desc MonCat.FilteredColimits.colimitDesc
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_desc AddMonCat.FilteredColimits.colimitDesc
 
-/-- The proposed colimit cocone is a colimit in `Mon`. -/
+/-- The proposed colimit cocone is a colimit in `MonCat`. -/
 @[to_additive "The proposed colimit cocone is a colimit in `AddMon`."]
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   desc := colimitDesc.{v, u} F
@@ -364,9 +333,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
       ((Types.colimitCoconeIsColimit (F ⋙ forget MonCat)).uniq ((forget MonCat).mapCocone t)
         ((forget MonCat).map m)
         fun j => funext fun x => FunLike.congr_fun (i := MonCat.Hom_FunLike _ _) (h j) x) y
-set_option linter.uppercaseLean3 false in
 #align Mon.filtered_colimits.colimit_cocone_is_colimit MonCat.FilteredColimits.colimitCoconeIsColimit
-set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_cocone_is_colimit AddMonCat.FilteredColimits.colimitCoconeIsColimit
 
 @[to_additive]
@@ -389,17 +356,15 @@ section
 -- passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ CommMonCat.{max v u})
 
-/-- The colimit of `F ⋙ forget₂ CommMon Mon` in the category `Mon`.
+/-- The colimit of `F ⋙ forget₂ CommMonCat MonCat` in the category `MonCat`.
 In the following, we will show that this has the structure of a _commutative_ monoid.
 -/
 @[to_additive
-      "The colimit of `F ⋙ forget₂ AddCommMon AddMon` in the category `AddMon`. In the
+      "The colimit of `F ⋙ forget₂ AddCommMonCat AddMonCat` in the category `AddMonCat`. In the
       following, we will show that this has the structure of a _commutative_ additive monoid."]
 noncomputable abbrev M : MonCat.{max v u} :=
   MonCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ CommMonCat MonCat.{max v u})
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.M CommMonCat.FilteredColimits.M
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.M AddCommMonCat.FilteredColimits.M
 
 @[to_additive]
@@ -416,18 +381,14 @@ noncomputable instance colimitCommMonoid : CommMonoid.{max v u} (M.{v, u} F):=
         colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) y x k g f]
       dsimp
       rw [mul_comm] }
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.colimit_comm_monoid CommMonCat.FilteredColimits.colimitCommMonoid
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.colimit_add_comm_monoid AddCommMonCat.FilteredColimits.colimitAddCommMonoid
 
 /-- The bundled commutative monoid giving the filtered colimit of a diagram. -/
 @[to_additive "The bundled additive commutative monoid giving the filtered colimit of a diagram."]
 noncomputable def colimit : CommMonCat.{max v u} :=
   CommMonCat.of (M.{v, u} F)
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.colimit CommMonCat.FilteredColimits.colimit
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.colimit AddCommMonCat.FilteredColimits.colimit
 
 /-- The cocone over the proposed colimit commutative monoid. -/
@@ -436,12 +397,10 @@ noncomputable def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι := { (MonCat.FilteredColimits.colimitCocone.{v, u}
     (F ⋙ forget₂ CommMonCat MonCat.{max v u})).ι with }
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.colimit_cocone CommMonCat.FilteredColimits.colimitCocone
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.colimit_cocone AddCommMonCat.FilteredColimits.colimitCocone
 
-/-- The proposed colimit cocone is a colimit in `CommMon`. -/
+/-- The proposed colimit cocone is a colimit in `CommMonCat`. -/
 @[to_additive "The proposed colimit cocone is a colimit in `AddCommMon`."]
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   desc t :=
@@ -457,9 +416,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
         ((forget CommMonCat.{max v u}).mapCocone t)
         ((forget CommMonCat.{max v u}).map m) fun j => funext fun x =>
           FunLike.congr_fun (i := CommMonCat.Hom_FunLike _ _) (h j) x
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.colimit_cocone_is_colimit CommMonCat.FilteredColimits.colimitCoconeIsColimit
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.colimit_cocone_is_colimit AddCommMonCat.FilteredColimits.colimitCoconeIsColimit
 
 @[to_additive forget₂AddMonPreservesFilteredColimits]
@@ -468,18 +425,14 @@ noncomputable instance forget₂MonPreservesFilteredColimits :
 ⟨fun J hJ1 _ => letI hJ3 : Category J := hJ1
   ⟨fun {F} => preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
     (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ CommMonCat MonCat.{u}))⟩⟩
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.forget₂_Mon_preserves_filtered_colimits CommMonCat.FilteredColimits.forget₂MonPreservesFilteredColimits
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits
 
 @[to_additive]
 noncomputable instance forgetPreservesFilteredColimits :
     PreservesFilteredColimits (forget CommMonCat.{u}) :=
   Limits.compPreservesFilteredColimits (forget₂ CommMonCat MonCat) (forget MonCat)
-set_option linter.uppercaseLean3 false in
 #align CommMon.filtered_colimits.forget_preserves_filtered_colimits CommMonCat.FilteredColimits.forgetPreservesFilteredColimits
-set_option linter.uppercaseLean3 false in
 #align AddCommMon.filtered_colimits.forget_preserves_filtered_colimits AddCommMonCat.FilteredColimits.forgetPreservesFilteredColimits
 
 end

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1106,7 +1106,6 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq
         have h1 : gcd a b ≠ 0 := by
           have hab : a * b ≠ 0 := mul_ne_zero a0 hb
           contrapose! hab
-          push_neg at hab
           rw [← normalize_eq_zero, ← this, hab, zero_mul]
         have h2 : normalize (gcd a b * l) = gcd a b * l := by rw [this, normalize_idem]
         rw [← normalize_gcd] at this

Mathlib/Analysis/Calculus/BumpFunctionFindim.lean

@@ -570,8 +570,7 @@ instance (priority := 100) {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ
           _root_.smul_ball A.ne', Real.norm_of_nonneg A.le, smul_zero]
         refine' congr (congr_arg ball (Eq.refl 0)) _
         field_simp [A'.ne']
-        ring
-         }
+        ring }
 
 end ExistsContDiffBumpBase
 

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -353,9 +353,6 @@ theorem WithSeminorms.separating_of_T1 [T1Space E] (hp : WithSeminorms p) (x : E
     ∃ i, p i x ≠ 0 := by
   have := ((t1Space_TFAE E).out 0 9).mp (inferInstanceAs <| T1Space E)
   by_contra' h
-  -- In theory, `by_contra'` does `push_neg`, but it doesn't, and `push_neg` on his own
-  -- does nothing... So we have to do `simp` by hand.
-  simp only [not_exists, not_not] at h
   refine' hx (this _)
   rw [hp.hasBasis_zero_ball.specializes_iff]
   rintro ⟨s, r⟩ (hr : 0 < r)

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -426,7 +426,6 @@ theorem differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < n) (h2 :
     have b : ∀ m : ℕ, s + 1 ≠ -m := by
       intro m; have := h2 (1 + m)
       contrapose! this
-      push_neg at this
       rw [← eq_sub_iff_add_eq] at this
       simpa using this
     refine' DifferentiableAt.div (DifferentiableAt.comp _ (hn a b) _) _ _

Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

@@ -157,8 +157,6 @@ theorem exists_adj_boundary_pair (Gc : G.Preconnected) (hK : K.Nonempty) :
   let C : G.ComponentCompl K := G.componentComplMk vnK
   let dis := Set.disjoint_iff.mp C.disjoint_right
   by_contra' h
-  -- Porting note: `push_neg` doesn't do its job
-  simp only [not_exists, not_and] at h
   suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
   symm
   rw [Set.eq_univ_iff_forall]

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -504,8 +504,6 @@ theorem exists_factorization_lt_of_lt {a b : ℕ} (ha : a ≠ 0) (hab : a < b) :
     ∃ p : ℕ, a.factorization p < b.factorization p := by
   have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
   contrapose! hab
-  -- Porting note: `push_neg` fails to push the negation
-  simp_rw [not_exists, not_lt] at hab
   rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
   exact le_of_dvd ha.bot_lt hab
 #align nat.exists_factorization_lt_of_lt Nat.exists_factorization_lt_of_lt

Mathlib/Data/Nat/PartENat.lean

@@ -382,9 +382,8 @@ theorem eq_top_iff_forall_lt (x : PartENat) : x = ⊤ ↔ ∀ n : ℕ, (n : Part
   constructor
   · rintro rfl n
     exact natCast_lt_top _
-  · -- Porting note: was `contrapose!`
-    contrapose
-    rw [←Ne, ne_top_iff, not_forall]
+  · contrapose!
+    rw [ne_top_iff]
     rintro ⟨n, rfl⟩
     exact ⟨n, irrefl _⟩
 #align part_enat.eq_top_iff_forall_lt PartENat.eq_top_iff_forall_lt
@@ -792,10 +791,8 @@ theorem lt_find (n : ℕ) (h : ∀ m ≤ n, ¬P m) : (n : PartENat) < find P :=
   rw [find_get]
   have h₂ := @Nat.find_spec P _ h₁
   revert h₂
-  contrapose
-  intro h₂
-  rw [not_lt] at h₂
-  exact h _ h₂
+  contrapose!
+  exact h _
 #align part_enat.lt_find PartENat.lt_find
 
 theorem lt_find_iff (n : ℕ) : (n : PartENat) < find P ↔ ∀ m ≤ n, ¬P m := by