chore(Logic/Function/Defs): move file out of Init (#14754)

jcommelin · jcommelin · commit f0587c5d3961 · 2024-07-16T07:40:50.000Z
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2742,7 +2742,6 @@ import Mathlib.Init.Data.Quot
 import Mathlib.Init.Data.Rat.Basic
 import Mathlib.Init.Data.Sigma.Basic
 import Mathlib.Init.Data.Sigma.Lex
-import Mathlib.Init.Function
 import Mathlib.Init.Logic
 import Mathlib.Init.Meta.WellFoundedTactics
 import Mathlib.Init.Order.Defs
@@ -2995,9 +2994,11 @@ import Mathlib.Logic.Equiv.TransferInstance
 import Mathlib.Logic.Function.Basic
 import Mathlib.Logic.Function.CompTypeclasses
 import Mathlib.Logic.Function.Conjugate
+import Mathlib.Logic.Function.Defs
 import Mathlib.Logic.Function.FromTypes
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Logic.Function.OfArity
+import Mathlib.Logic.Function.ULift
 import Mathlib.Logic.Godel.GodelBetaFunction
 import Mathlib.Logic.Hydra
 import Mathlib.Logic.IsEmpty
diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.Data.ULift
+import Mathlib.Logic.Function.ULift
 
 #align_import category_theory.yoneda from "leanprover-community/mathlib"@"369525b73f229ccd76a6ec0e0e0bf2be57599768"
 
diff --git a/Mathlib/Control/Basic.lean b/Mathlib/Control/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Control.Combinators
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.CasesM
 import Mathlib.Tactic.Attr.Core
 
diff --git a/Mathlib/Control/Traversable/Basic.lean b/Mathlib/Control/Traversable/Basic.lean
@@ -5,6 +5,7 @@ Authors: Simon Hudon
 -/
 import Mathlib.Data.Option.Defs
 import Mathlib.Control.Functor
+import Batteries.Data.List.Basic
 
 #align_import control.traversable.basic from "leanprover-community/mathlib"@"1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a"
 
diff --git a/Mathlib/Data/Bool/Basic.lean b/Mathlib/Data/Bool/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 import Mathlib.Init.Order.Defs
 
 #align_import data.bool.basic from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
@@ -8,6 +8,7 @@ import Mathlib.Control.Functor
 import Mathlib.Data.SProd
 import Mathlib.Util.CompileInductive
 import Batteries.Tactic.Lint.Basic
+import Batteries.Data.List.Lemmas
 
 #align_import data.list.defs from "leanprover-community/mathlib"@"d2d8742b0c21426362a9dacebc6005db895ca963"
 
diff --git a/Mathlib/Data/Option/NAry.lean b/Mathlib/Data/Option/NAry.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 
 #align_import data.option.n_ary from "leanprover-community/mathlib"@"995b47e555f1b6297c7cf16855f1023e355219fb"
 
diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Inhabit
 
diff --git a/Mathlib/Data/Prod/PProd.lean b/Mathlib/Data/Prod/PProd.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 
 #align_import data.prod.pprod from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
diff --git a/Mathlib/Data/Sigma/Basic.lean b/Mathlib/Data/Sigma/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 import Mathlib.Logic.Function.Basic
 
 #align_import data.sigma.basic from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 import Mathlib.Init.Logic
-import Mathlib.Init.Function
 import Mathlib.Init.Algebra.Classes
+import Mathlib.Tactic.Attr.Register
+import Mathlib.Tactic.Basic
 import Batteries.Util.LibraryNote
 import Batteries.Tactic.Lint.Basic
 
@@ -66,22 +67,6 @@ theorem congr_arg_heq {β : α → Sort*} (f : ∀ a, β a) :
   | _, _, rfl => HEq.rfl
 #align congr_arg_heq congr_arg_heq
 
-theorem ULift.down_injective {α : Sort _} : Function.Injective (@ULift.down α)
-  | ⟨a⟩, ⟨b⟩, _ => by congr
-#align ulift.down_injective ULift.down_injective
-
-@[simp] theorem ULift.down_inj {α : Sort _} {a b : ULift α} : a.down = b.down ↔ a = b :=
-  ⟨fun h ↦ ULift.down_injective h, fun h ↦ by rw [h]⟩
-#align ulift.down_inj ULift.down_inj
-
-theorem PLift.down_injective : Function.Injective (@PLift.down α)
-  | ⟨a⟩, ⟨b⟩, _ => by congr
-#align plift.down_injective PLift.down_injective
-
-@[simp] theorem PLift.down_inj {a b : PLift α} : a.down = b.down ↔ a = b :=
-  ⟨fun h ↦ PLift.down_injective h, fun h ↦ by rw [h]⟩
-#align plift.down_inj PLift.down_inj
-
 @[simp] theorem eq_iff_eq_cancel_left {b c : α} : (∀ {a}, a = b ↔ a = c) ↔ b = c :=
   ⟨fun h ↦ by rw [← h], fun h a ↦ by rw [h]⟩
 #align eq_iff_eq_cancel_left eq_iff_eq_cancel_left
@@ -273,7 +258,8 @@ theorem not_imp_comm : ¬a → b ↔ ¬b → a := Decidable.not_imp_comm
 @[simp] theorem not_imp_self : ¬a → a ↔ a := Decidable.not_imp_self
 #align not_imp_self not_imp_self
 
-theorem Imp.swap {a b : Sort*} {c : Prop} : a → b → c ↔ b → a → c := ⟨Function.swap, Function.swap⟩
+theorem Imp.swap {a b : Sort*} {c : Prop} : a → b → c ↔ b → a → c :=
+  ⟨fun h x y ↦ h y x, fun h x y ↦ h y x⟩
 #align imp.swap Imp.swap
 
 alias Iff.not := not_congr
@@ -653,7 +639,8 @@ variable {α β : Sort*} {p q : α → Prop}
 
 #align exists_imp_exists' Exists.imp'
 
-theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y := ⟨swap, swap⟩
+theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
+  ⟨fun f x y ↦ f y x, fun f x y ↦ f y x⟩
 #align forall_swap forall_swap
 
 theorem forall₂_swap
diff --git a/Mathlib/Logic/Function/CompTypeclasses.lean b/Mathlib/Logic/Function/CompTypeclasses.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
 
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 
 /-!
 # Propositional typeclasses on several maps
diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean
@@ -3,27 +3,16 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
 -/
-import Mathlib.Tactic.Basic
 import Mathlib.Mathport.Rename
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Attr.Register
+import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.TypeStar
 
 #align_import init.function from "leanprover-community/lean"@"03a6a6015c0b12dce7b36b4a1f7205a92dfaa592"
 
 /-!
-# Note about `Mathlib/Init/`
-The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
-(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)
-
-We intend to move all the content of these files out into the main `Mathlib` directory structure.
-Contributions assisting with this are appreciated.
-
-`#align` statements without corresponding declarations
-(i.e. because the declaration is in Batteries or Lean) can be left here.
-These will be deleted soon so will not significantly delay deleting otherwise empty `Init` files.
-
 # General operations on functions
 -/
 
diff --git a/Mathlib/Logic/Function/ULift.lean b/Mathlib/Logic/Function/ULift.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2016 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import Mathlib.Logic.Function.Defs
+
+/-!
+# `ULift` and `PLift`
+-/
+
+theorem ULift.down_injective {α : Sort _} : Function.Injective (@ULift.down α)
+  | ⟨a⟩, ⟨b⟩, _ => by congr
+#align ulift.down_injective ULift.down_injective
+
+@[simp] theorem ULift.down_inj {α : Sort _} {a b : ULift α} : a.down = b.down ↔ a = b :=
+  ⟨fun h ↦ ULift.down_injective h, fun h ↦ by rw [h]⟩
+#align ulift.down_inj ULift.down_inj
+
+variable {α : Sort*}
+
+theorem PLift.down_injective : Function.Injective (@PLift.down α)
+  | ⟨a⟩, ⟨b⟩, _ => by congr
+#align plift.down_injective PLift.down_injective
+
+@[simp] theorem PLift.down_inj {a b : PLift α} : a.down = b.down ↔ a = b :=
+  ⟨fun h ↦ PLift.down_injective h, fun h ↦ by rw [h]⟩
+#align plift.down_inj PLift.down_inj
+
diff --git a/Mathlib/Logic/Nonempty.lean b/Mathlib/Logic/Nonempty.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Init.ZeroOne
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 
 #align_import logic.nonempty from "leanprover-community/mathlib"@"d2d8742b0c21426362a9dacebc6005db895ca963"
 
diff --git a/Mathlib/Logic/Nontrivial/Defs.lean b/Mathlib/Logic/Nontrivial/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Init.Logic
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.TypeStar
 
 #align_import logic.nontrivial from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
diff --git a/Mathlib/Logic/Relator.lean b/Mathlib/Logic/Relator.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 
 #align_import logic.relator from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
diff --git a/Mathlib/Order/ULift.lean b/Mathlib/Order/ULift.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
+import Mathlib.Logic.Function.ULift
 import Mathlib.Order.Basic
 
 /-! # Ordered structures on `ULift.{v} α`
diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean
@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
 import Mathlib.Control.Traversable.Lemmas
+import Lean.Elab.Match
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.PreDefinition.Main
 
 #align_import control.traversable.derive from "leanprover-community/mathlib"@"b01d6eb9d0a308807af54319b264d0994b91774b"
 
diff --git a/scripts/noshake.json b/scripts/noshake.json
@@ -298,7 +298,7 @@
   "Mathlib.Lean.Expr.ExtraRecognizers": ["Mathlib.Data.Set.Defs"],
   "Mathlib.Lean.Expr.Basic": ["Batteries.Logic"],
   "Mathlib.Init.Logic": ["Batteries.Logic"],
-  "Mathlib.Init.Function": ["Mathlib.Tactic.AdaptationNote"],
+  "Mathlib.Logic.Function.Defs": ["Mathlib.Tactic.AdaptationNote"],
   "Mathlib.Init.Data.Nat.Lemmas": ["Batteries.Data.Nat.Lemmas", "Batteries.WF"],
   "Mathlib.Init.Data.Nat.GCD": ["Batteries.Data.Nat.Gcd"],
   "Mathlib.Init.Data.List.Basic": ["Batteries.Data.List.Basic"],
@@ -323,7 +323,7 @@
   "Mathlib.Data.Finset.Basic": ["Mathlib.Data.Finset.Attr"],
   "Mathlib.Data.DFinsupp.Notation": ["Mathlib.Data.Finsupp.Notation"],
   "Mathlib.Control.Traversable.Instances": ["Mathlib.Control.Applicative"],
-  "Mathlib.Control.Basic": ["Mathlib.Init.Function"],
+  "Mathlib.Control.Basic": ["Mathlib.Logic.Function.Defs"],
   "Mathlib.Combinatorics.SetFamily.AhlswedeZhang":
   ["Mathlib.Algebra.Order.Field.Basic"],
   "Mathlib.CategoryTheory.Sites.IsSheafFor":
diff --git a/test/apply_fun.lean b/test/apply_fun.lean
@@ -1,7 +1,7 @@
 import Mathlib.Data.Nat.Notation
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.ApplyFun
-import Mathlib.Init.Function
+import Mathlib.Logic.Function.Defs
 import Mathlib.Data.Fintype.Card
 import Mathlib.Data.Matrix.Basic
 
