refactor(library/algebra/function): move function.lean to init folder

Motivation: this file defines basic things such as function composition.
In the HoTT library, it is located in the init folder.

library/algebra/binary.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Jeremy Avigad
 
 General properties of binary operations.
 -/
-import algebra.function
 open eq.ops function
 
 namespace binary

library/algebra/category/functor.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 -/
 import .basic
-import logic.cast algebra.function
+import logic.cast
 open function
 open category eq eq.ops heq
 

library/algebra/field.lean

@@ -8,7 +8,7 @@ The development is modeled after Isabelle's library.
 -/
 ----------------------------------------------------------------------------------------------------
 import logic.eq logic.connectives data.unit data.sigma data.prod
-import algebra.function algebra.binary algebra.group algebra.ring
+import algebra.binary algebra.group algebra.ring
 open eq eq.ops
 
 namespace algebra

library/algebra/group.lean

@@ -7,7 +7,7 @@ Various multiplicative and additive structures. Partially modeled on Isabelle's
 -/
 
 import logic.eq data.unit data.sigma data.prod
-import algebra.function algebra.binary algebra.priority
+import algebra.binary algebra.priority
 
 open eq eq.ops   -- note: ⁻¹ will be overloaded
 open binary

library/algebra/ordered_group.lean

@@ -7,8 +7,7 @@ Partially ordered additive groups, modeled on Isabelle's library. These classes
 if necessary.
 -/
 import logic.eq data.unit data.sigma data.prod
-import algebra.function algebra.binary
+import algebra.binary algebra.group algebra.order
-import algebra.group algebra.order
 open eq eq.ops   -- note: ⁻¹ will be overloaded
 
 namespace algebra

library/algebra/ring.lean

@@ -8,7 +8,7 @@ The development is modeled after Isabelle's library.
 -/
 
 import logic.eq logic.connectives data.unit data.sigma data.prod
-import algebra.function algebra.binary algebra.group
+import algebra.binary algebra.group
 open eq eq.ops
 
 namespace algebra

library/data/countable.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 
 Define countable types
 -/
-import algebra.function
 open function
 
 definition countable (A : Type) : Prop := ∃ f : A → nat, injective f

library/data/list/basic.lean

@@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
 
 Basic properties of lists.
 -/
-import logic tools.helper_tactics data.nat.order algebra.function
+import logic tools.helper_tactics data.nat.order
 open eq.ops helper_tactics nat prod function option
 
 inductive list (T : Type) : Type :=

library/data/set/function.lean

@@ -6,7 +6,6 @@ Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang
 Functions between subsets of finite types.
 -/
 import .basic
-import algebra.function
 open function eq.ops
 
 namespace set

library/data/stream.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import data.nat data.list algebra.function
+import data.nat data.list
 open nat function option
 
 definition stream (A : Type) := nat → A

library/data/uprod.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 
 Unordered pairs
 -/
-import data.prod logic.identities algebra.function
+import data.prod logic.identities
 open prod prod.ops quot function
 
 private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=

library/data/vec.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 
 vectors as list subtype
 -/
-import logic data.list data.subtype algebra.function
+import logic data.list data.subtype
 open nat list subtype function
 
 definition vec [reducible] (A : Type) (n : nat) := {l : list A | length l = n}

library/init/default.lean

@@ -7,4 +7,4 @@ prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod init.priority
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
-import init.funext
+import init.funext init.function

library/init/function.lean

@@ -5,7 +5,8 @@ Author: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
 
 General operations on functions.
 -/
-import logic.cast
+prelude
+import init.prod init.funext init.logic
 
 namespace function
 

library/init/logic.lean

@@ -70,6 +70,12 @@ end eq
 theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
 eq.subst H₁ (eq.subst H₂ rfl)
 
+theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
+eq.subst H (eq.refl (f a))
+
+theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) (H : a₁ = a₂) : f a₁ = f a₂ :=
+congr rfl H
+
 section
   variables {A : Type} {a b c: A}
   open eq.ops

library/logic/axioms/examples/leftinv_of_inj.lean

@@ -9,7 +9,7 @@ The proof uses the classical axioms: choice and excluded middle.
 The excluded middle is being used "behind the scenes" to allow us to write the if-then-else expression
 with (∃ a : A, f a = b).
 -/
-import algebra.function logic.axioms.classical
+import logic.axioms.classical
 open function
 
 definition mk_left_inv {A B : Type} [h : nonempty A] (f : A → B) : B → A :=

library/logic/eq.lean

@@ -47,12 +47,6 @@ section
   variables {A B C D E F : Type}
   variables {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E}
 
-  theorem congr_fun {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
-  by substvars
-
-  theorem congr_arg (f : A → B) (H : a = a') : f a = f a' :=
-  by substvars
-
   theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
   by substvars