chore: re-port Init.Function (#5859)

Notably this fixes the naming of `comp_left` and `comp_right`.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib/Init/Function.lean

@@ -2,130 +2,207 @@
 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
+
+! This file was ported from Lean 3 source module init.function
+! leanprover-community/lean commit 03a6a6015c0b12dce7b36b4a1f7205a92dfaa592
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
+import Mathlib.Init.Data.Prod
+import Mathlib.Init.Logic
 import Mathlib.Mathport.Rename
 import Mathlib.Tactic.Attr.Register
--- a port of core Lean `init/function.lean`
 
 /-!
 # General operations on functions
 -/
 
+
+universe u₁ u₂ u₃ u₄ u₅
+
 namespace Function
 
+-- porting note: fix the universe of `ζ`, it used to be `u₁`
 variable {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₅}
 
-@[reducible] def comp_right (f : β → β → β) (g : α → β) : β → α → β :=
-λ b a => f b (g a)
+#align function.comp Function.comp
+
+/-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
+and type of `f (g x)` depends on `x` and `g x`. -/
+@[inline, reducible]
+def dcomp {β : α → Sort u₂} {φ : ∀ {x : α}, β x → Sort u₃} (f : ∀ {x : α} (y : β x), φ y)
+    (g : ∀ x, β x) : ∀ x, φ (g x) := fun x => f (g x)
+#align function.dcomp Function.dcomp
 
-@[reducible] def comp_left (f : β → β → β) (g : α → β) : α → β → β :=
-λ a b => f (g a) b
+infixr:80 " ∘' " => Function.dcomp
+
+@[reducible]
+def compRight (f : β → β → β) (g : α → β) : β → α → β := fun b a => f b (g a)
+#align function.comp_right Function.compRight
+
+@[reducible]
+def compLeft (f : β → β → β) (g : α → β) : α → β → β := fun a b => f (g a) b
+#align function.comp_left Function.compLeft
 
 /-- Given functions `f : β → β → φ` and `g : α → β`, produce a function `α → α → φ` that evaluates
 `g` on each argument, then applies `f` to the results. Can be used, e.g., to transfer a relation
 from `β` to `α`. -/
-@[reducible] def onFun (f : β → β → φ) (g : α → β) : α → α → φ :=
-λ x y => f (g x) (g y)
+@[reducible]
+def onFun (f : β → β → φ) (g : α → β) : α → α → φ := fun x y => f (g x) (g y)
+#align function.on_fun Function.onFun
 
 /-- Given functions `f : α → β → φ`, `g : α → β → δ` and a binary operator `op : φ → δ → ζ`,
 produce a function `α → β → ζ` that applies `f` and `g` on each argument and then applies
 `op` to the results.
 -/
 -- Porting note: the ζ variable was originally constrained to `Sort u₁`, but this seems to
 -- have been an oversight.
-@[reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)
-  : α → β → ζ :=
-λ x y => op (f x y) (g x y)
+@[reducible]
+def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ) : α → β → ζ := fun x y =>
+  op (f x y) (g x y)
+#align function.combine Function.combine
 
-@[reducible] def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y :=
-λ y x => f x y
+#align function.const Function.const
 
-@[reducible] def app {β : α → Sort u₂} (f : ∀ x, β x) (x : α) : β x :=
-f x
+@[reducible]
+def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := fun y x => f x y
+#align function.swap Function.swap
+
+@[reducible]
+def app {β : α → Sort u₂} (f : ∀ x, β x) (x : α) : β x :=
+  f x
+#align function.app Function.app
 
 @[inherit_doc onFun]
 infixl:2 " on " => onFun
 
-theorem left_id (f : α → β) : id ∘ f = f := rfl
+-- porting note: removed, it was never used
+-- notation f " -[" op "]- " g => combine f op g
+
+theorem left_id (f : α → β) : id ∘ f = f :=
+  rfl
+#align function.left_id Function.left_id
 
-theorem right_id (f : α → β) : f ∘ id = f := rfl
+theorem right_id (f : α → β) : f ∘ id = f :=
+  rfl
+#align function.right_id Function.right_id
 
 #align function.comp_app Function.comp_apply
 
-theorem comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
+theorem comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ g ∘ h :=
+  rfl
+#align function.comp.assoc Function.comp.assoc
 
-@[simp, mfld_simps] theorem comp.left_id (f : α → β) : id ∘ f = f := rfl
+@[simp, mfld_simps]
+theorem comp.left_id (f : α → β) : id ∘ f = f :=
+  rfl
+#align function.comp.left_id Function.comp.left_id
 
-@[simp, mfld_simps] theorem comp.right_id (f : α → β) : f ∘ id = f := rfl
+@[simp, mfld_simps]
+theorem comp.right_id (f : α → β) : f ∘ id = f :=
+  rfl
+#align function.comp.right_id Function.comp.right_id
 
-theorem comp_const_right (f : β → φ) (b : β) : f ∘ (const α b) = const α (f b) := rfl
+theorem comp_const_right (f : β → φ) (b : β) : f ∘ const α b = const α (f b) :=
+  rfl
+#align function.comp_const_right Function.comp_const_right
 
 /-- A function `f : α → β` is called injective if `f x = f y` implies `x = y`. -/
-def Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+def Injective (f : α → β) : Prop :=
+  ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+#align function.injective Function.Injective
 
 theorem Injective.comp {g : β → φ} {f : α → β} (hg : Injective g) (hf : Injective f) :
-  Injective (g ∘ f) :=
-fun _ _ h ↦ hf (hg h)
+    Injective (g ∘ f) := fun _a₁ _a₂ => fun h => hf (hg h)
+#align function.injective.comp Function.Injective.comp
 
 /-- A function `f : α → β` is called surjective if every `b : β` is equal to `f a`
 for some `a : α`. -/
-def Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
+@[reducible]
+def Surjective (f : α → β) : Prop :=
+  ∀ b, ∃ a, f a = b
+#align function.surjective Function.Surjective
 
 theorem Surjective.comp {g : β → φ} {f : α → β} (hg : Surjective g) (hf : Surjective f) :
-  Surjective (g ∘ f) :=
-λ (c : φ) => Exists.elim (hg c) (λ b hb => Exists.elim (hf b) (λ a ha =>
-  Exists.intro a (show g (f a) = c from (Eq.trans (congrArg g ha) hb))))
+    Surjective (g ∘ f) := fun c : φ =>
+  Exists.elim (hg c) fun b hb =>
+    Exists.elim (hf b) fun a ha =>
+      Exists.intro a (show g (f a) = c from Eq.trans (congr_arg g ha) hb)
+#align function.surjective.comp Function.Surjective.comp
 
 /-- A function is called bijective if it is both injective and surjective. -/
-def Bijective (f : α → β) := Injective f ∧ Surjective f
+def Bijective (f : α → β) :=
+  Injective f ∧ Surjective f
+#align function.bijective Function.Bijective
 
 theorem Bijective.comp {g : β → φ} {f : α → β} : Bijective g → Bijective f → Bijective (g ∘ f)
   | ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩
+#align function.bijective.comp Function.Bijective.comp
 
 /-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
-def LeftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
+def LeftInverse (g : β → α) (f : α → β) : Prop :=
+  ∀ x, g (f x) = x
+#align function.left_inverse Function.LeftInverse
 
 /-- `HasLeftInverse f` means that `f` has an unspecified left inverse. -/
-def HasLeftInverse (f : α → β) : Prop := ∃ finv : β → α, LeftInverse finv f
+def HasLeftInverse (f : α → β) : Prop :=
+  ∃ finv : β → α, LeftInverse finv f
 #align function.has_left_inverse Function.HasLeftInverse
 
 /-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
-def RightInverse (g : β → α) (f : α → β) : Prop := LeftInverse f g
+def RightInverse (g : β → α) (f : α → β) : Prop :=
+  LeftInverse f g
+#align function.right_inverse Function.RightInverse
 
-/-- `hasRightInverse f` means that `f` has an unspecified right inverse. -/
-def HasRightInverse (f : α → β) : Prop := ∃ finv : β → α, RightInverse finv f
+/-- `HasRightInverse f` means that `f` has an unspecified right inverse. -/
+def HasRightInverse (f : α → β) : Prop :=
+  ∃ finv : β → α, RightInverse finv f
 #align function.has_right_inverse Function.HasRightInverse
 
 theorem LeftInverse.injective {g : β → α} {f : α → β} : LeftInverse g f → Injective f :=
-  λ h a b hf => h a ▸ h b ▸ hf ▸ rfl
-
-theorem HasLeftInverse.injective {f : α → β} : HasLeftInverse f → Injective f :=
-  λ h => Exists.elim h (λ _ inv => inv.injective)
-
-theorem rightInverse_of_injective_of_leftInverse {f : α → β} {g : β → α}
-    (injf : Injective f) (lfg : LeftInverse f g) :
-  RightInverse f g :=
-λ x => injf $ lfg $ f x
+  fun h a b faeqfb =>
+  calc
+    a = g (f a) := (h a).symm
+    _ = g (f b) := (congr_arg g faeqfb)
+    _ = b := h b
+#align function.left_inverse.injective Function.LeftInverse.injective
+
+theorem HasLeftInverse.injective {f : α → β} : HasLeftInverse f → Injective f := fun h =>
+  Exists.elim h fun _finv inv => inv.injective
+#align function.has_left_inverse.injective Function.HasLeftInverse.injective
+
+theorem rightInverse_of_injective_of_leftInverse {f : α → β} {g : β → α} (injf : Injective f)
+    (lfg : LeftInverse f g) : RightInverse f g := fun x =>
+  have h : f (g (f x)) = f x := lfg (f x)
+  injf h
 #align function.right_inverse_of_injective_of_left_inverse Function.rightInverse_of_injective_of_leftInverse
 
 theorem RightInverse.surjective {f : α → β} {g : β → α} (h : RightInverse g f) : Surjective f :=
-  λ y => ⟨g y, h y⟩
+  fun y => ⟨g y, h y⟩
+#align function.right_inverse.surjective Function.RightInverse.surjective
 
 theorem HasRightInverse.surjective {f : α → β} : HasRightInverse f → Surjective f
-  | ⟨_, inv⟩ => inv.surjective
+  | ⟨_finv, inv⟩ => inv.surjective
+#align function.has_right_inverse.surjective Function.HasRightInverse.surjective
 
 theorem leftInverse_of_surjective_of_rightInverse {f : α → β} {g : β → α} (surjf : Surjective f)
-  (rfg : RightInverse f g) : LeftInverse f g :=
-λ y =>
-  let ⟨x, hx⟩ := surjf y
-  by rw [← hx, rfg]
+    (rfg : RightInverse f g) : LeftInverse f g := fun y =>
+  Exists.elim (surjf y) fun x hx =>
+    calc
+      f (g y) = f (g (f x)) := hx ▸ rfl
+      _ = f x := (Eq.symm (rfg x) ▸ rfl)
+      _ = y := hx
 #align function.left_inverse_of_surjective_of_right_inverse Function.leftInverse_of_surjective_of_rightInverse
 
-theorem injective_id : Injective (@id α) := fun _ _ ↦ id
+theorem injective_id : Injective (@id α) := fun _a₁ _a₂ h => h
+#align function.injective_id Function.injective_id
 
-theorem surjective_id : Surjective (@id α) := λ a => ⟨a, rfl⟩
+theorem surjective_id : Surjective (@id α) := fun a => ⟨a, rfl⟩
+#align function.surjective_id Function.surjective_id
 
-theorem bijective_id : Bijective (@id α) := ⟨injective_id, surjective_id⟩
+theorem bijective_id : Bijective (@id α) :=
+  ⟨injective_id, surjective_id⟩
+#align function.bijective_id Function.bijective_id
 
 end Function
 
@@ -134,23 +211,31 @@ namespace Function
 variable {α : Type u₁} {β : Type u₂} {φ : Type u₃}
 
 /-- Interpret a function on `α × β` as a function with two arguments. -/
-@[inline] def curry : (α × β → φ) → α → β → φ :=
-λ f a b => f (a, b)
+@[inline]
+def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
+#align function.curry Function.curry
 
 /-- Interpret a function with two arguments as a function on `α × β` -/
-@[inline] def uncurry : (α → β → φ) → α × β → φ :=
-λ f a => f a.1 a.2
+@[inline]
+def uncurry : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2
+#align function.uncurry Function.uncurry
 
-@[simp] theorem curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
+@[simp]
+theorem curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
   rfl
+#align function.curry_uncurry Function.curry_uncurry
 
-@[simp] theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
-  funext (λ ⟨_, _⟩ => rfl)
+@[simp]
+theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
+  funext fun ⟨_a, _b⟩ => rfl
+#align function.uncurry_curry Function.uncurry_curry
 
 protected theorem LeftInverse.id {g : β → α} {f : α → β} (h : LeftInverse g f) : g ∘ f = id :=
   funext h
+#align function.left_inverse.id Function.LeftInverse.id
 
 protected theorem RightInverse.id {g : β → α} {f : α → β} (h : RightInverse g f) : f ∘ g = id :=
   funext h
+#align function.right_inverse.id Function.RightInverse.id
 
 end Function

Mathlib/ModelTheory/LanguageMap.lean

@@ -149,24 +149,24 @@ def comp (g : L' →ᴸ L'') (f : L →ᴸ L') : L →ᴸ L'' :=
   ⟨fun _n F => g.1 (f.1 F), fun _ R => g.2 (f.2 R)⟩
 #align first_order.language.Lhom.comp FirstOrder.Language.LHom.comp
 
---Porting note: added ' to avoid clash with function composition
+-- Porting note: added ᴸ to avoid clash with function composition
 @[inherit_doc]
-local infixl:60 " ∘' " => LHom.comp
+local infixl:60 " ∘ᴸ " => LHom.comp
 
 @[simp]
-theorem id_comp (F : L →ᴸ L') : LHom.id L' ∘' F = F := by
+theorem id_comp (F : L →ᴸ L') : LHom.id L' ∘ᴸ F = F := by
   cases F
   rfl
 #align first_order.language.Lhom.id_comp FirstOrder.Language.LHom.id_comp
 
 @[simp]
-theorem comp_id (F : L →ᴸ L') : F ∘' LHom.id L = F := by
+theorem comp_id (F : L →ᴸ L') : F ∘ᴸ LHom.id L = F := by
   cases F
   rfl
 #align first_order.language.Lhom.comp_id FirstOrder.Language.LHom.comp_id
 
 theorem comp_assoc {L3 : Language} (F : L'' →ᴸ L3) (G : L' →ᴸ L'') (H : L →ᴸ L') :
-    F ∘' G ∘' H = F ∘' (G ∘' H) :=
+    F ∘ᴸ G ∘ᴸ H = F ∘ᴸ (G ∘ᴸ H) :=
   rfl
 #align first_order.language.Lhom.comp_assoc FirstOrder.Language.LHom.comp_assoc
 
@@ -181,11 +181,11 @@ protected def sumElim : L.sum L'' →ᴸ L' where
   onRelation _n := Sum.elim (fun f => ϕ.onRelation f) fun f => ψ.onRelation f
 #align first_order.language.Lhom.sum_elim FirstOrder.Language.LHom.sumElim
 
-theorem sumElim_comp_inl (ψ : L'' →ᴸ L') : ϕ.sumElim ψ ∘' LHom.sumInl = ϕ :=
+theorem sumElim_comp_inl (ψ : L'' →ᴸ L') : ϕ.sumElim ψ ∘ᴸ LHom.sumInl = ϕ :=
   LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)
 #align first_order.language.Lhom.sum_elim_comp_inl FirstOrder.Language.LHom.sumElim_comp_inl
 
-theorem sumElim_comp_inr (ψ : L'' →ᴸ L') : ϕ.sumElim ψ ∘' LHom.sumInr = ψ :=
+theorem sumElim_comp_inr (ψ : L'' →ᴸ L') : ϕ.sumElim ψ ∘ᴸ LHom.sumInr = ψ :=
   LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)
 #align first_order.language.Lhom.sum_elim_comp_inr FirstOrder.Language.LHom.sumElim_comp_inr
 
@@ -194,7 +194,7 @@ theorem sumElim_inl_inr : LHom.sumInl.sumElim LHom.sumInr = LHom.id (L.sum L') :
 #align first_order.language.Lhom.sum_elim_inl_inr FirstOrder.Language.LHom.sumElim_inl_inr
 
 theorem comp_sumElim {L3 : Language} (θ : L' →ᴸ L3) :
-    θ ∘' ϕ.sumElim ψ = (θ ∘' ϕ).sumElim (θ ∘' ψ) :=
+    θ ∘ᴸ ϕ.sumElim ψ = (θ ∘ᴸ ϕ).sumElim (θ ∘ᴸ ψ) :=
   LHom.funext (funext fun _n => Sum.comp_elim _ _ _) (funext fun _n => Sum.comp_elim _ _ _)
 #align first_order.language.Lhom.comp_sum_elim FirstOrder.Language.LHom.comp_sumElim
 
@@ -212,12 +212,12 @@ def sumMap : L.sum L₁ →ᴸ L'.sum L₂ where
 #align first_order.language.Lhom.sum_map FirstOrder.Language.LHom.sumMap
 
 @[simp]
-theorem sumMap_comp_inl : ϕ.sumMap ψ ∘' LHom.sumInl = LHom.sumInl ∘' ϕ :=
+theorem sumMap_comp_inl : ϕ.sumMap ψ ∘ᴸ LHom.sumInl = LHom.sumInl ∘ᴸ ϕ :=
   LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)
 #align first_order.language.Lhom.sum_map_comp_inl FirstOrder.Language.LHom.sumMap_comp_inl
 
 @[simp]
-theorem sumMap_comp_inr : ϕ.sumMap ψ ∘' LHom.sumInr = LHom.sumInr ∘' ψ :=
+theorem sumMap_comp_inr : ϕ.sumMap ψ ∘ᴸ LHom.sumInr = LHom.sumInr ∘ᴸ ψ :=
   LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)
 #align first_order.language.Lhom.sum_map_comp_inr FirstOrder.Language.LHom.sumMap_comp_inr