Feat: port Order.Filter.Basic (#1750)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: ADedecker <anatolededecker@gmail.com>

Author: 5 people

Mathlib.lean

@@ -642,6 +642,7 @@ import Mathlib.Order.Cover
 import Mathlib.Order.Directed
 import Mathlib.Order.Disjoint
 import Mathlib.Order.Extension.Linear
+import Mathlib.Order.Filter.Basic
 import Mathlib.Order.FixedPoints
 import Mathlib.Order.GaloisConnection
 import Mathlib.Order.GameAdd

Mathlib/Data/Finset/Basic.lean

@@ -1205,8 +1205,8 @@ then it holds for the `Finset` obtained by inserting a new element.
 -/
 @[elab_as_elim]
 protected theorem induction_on {α : Type _} {p : Finset α → Prop} [DecidableEq α] (s : Finset α)
-    (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) : p s :=
-  Finset.induction h₁ h₂ s
+    (empty : p ∅) (insert : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)) : p s :=
+  Finset.induction empty insert s
 #align finset.induction_on Finset.induction_on
 
 /-- To prove a proposition about `S : Finset α`,

Mathlib/Logic/Function/Conjugate.lean

@@ -78,12 +78,18 @@ Given `h : function.commute f g` and `a : α`, we have `h a : f (g a) = g (f a)`
 def Commute (f g : α → α) : Prop :=
   Semiconj f g g
 
+/-- Reinterpret `Function.Semiconj f g g` as `Function.Commute f g`. These two predicates are
+definitionally equal but have different dot-notation lemmas. -/
 theorem Semiconj.commute {f g : α → α} (h : Semiconj f g g) : Commute f g := h
 
 namespace Commute
 
 variable {f f' g g' : α → α}
 
+/-- Reinterpret `Function.Commute f g` as `Function.Semiconj f g g`. These two predicates are
+definitionally equal but have different dot-notation lemmas. -/
+theorem semiconj (h : Commute f g) : Semiconj f g g := h
+
 @[refl]
 theorem refl (f : α → α) : Commute f f :=
   fun _ ↦ Eq.refl _

Mathlib/Mathport/Syntax.lean

@@ -8,6 +8,7 @@ import Lean.Elab.Quotation
 import Std.Tactic.Ext
 import Std.Tactic.RCases
 import Mathlib.Logic.Equiv.LocalEquiv
+import Mathlib.Order.Filter.Basic
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Alias
 import Mathlib.Tactic.ApplyFun
@@ -280,9 +281,6 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
 
 /- S -/ syntax (name := mkDecorations) "mk_decorations" : tactic
 
-/- M -/ syntax (name := filterUpwards) "filter_upwards" (termList)?
-  (" with" term:max*)? (" using" term)? : tactic
-
 /- E -/ syntax (name := isBounded_default) "isBounded_default" : tactic
 
 /- N -/ syntax (name := opInduction) "op_induction" (ppSpace (colGt term))? : tactic