chore: small progress on equiv and list basics (#124)

* small progress on equiv and list basics

* Apply suggestions from code review

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* removing @[simp] from theorem

* adapting names and filling another gap in Logic.Function.Basic

* fixing lint

* fixing functor and removing simp mark

* recovering commented theorem marked with simp

* removing theorem without simp mark

* adding old todo theorem

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Mathlib/Data/Equiv/Basic.lean

@@ -20,43 +20,50 @@ open Function
 variable {α : Sort u} {β : Sort v} {γ : Sort w}
 
 /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
-structure equiv (α : Sort u) (β : Sort v) :=
-(to_fun    : α → β)
-(inv_fun   : β → α)
-(left_inv  : left_inverse inv_fun to_fun)
-(right_inv : right_inverse inv_fun to_fun)
+structure Equiv (α : Sort u) (β : Sort v) where
+  toFun    : α → β
+  invFun   : β → α
+  leftInv  : left_inverse invFun toFun
+  rightInv : right_inverse invFun toFun
 
-infix:25 " ≃ " => equiv
+infix:25 " ≃ " => Equiv
 
-namespace equiv
+namespace Equiv
 
 /-- `perm α` is the type of bijections from `α` to itself. -/
-@[reducible] def perm (α : Sort u) := equiv α α
+@[reducible] def perm (α : Sort u) := Equiv α α
 
 instance : CoeFun (α ≃ β) (λ _ => α → β):=
-⟨to_fun⟩
+⟨toFun⟩
 
 -- Does not need to be simp, since the coercion is the projection,
 -- which simp has built-in support for.
-theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
+theorem coe_fn_mk (f : α → β) (g l r) : (Equiv.mk f g l r : α → β) = f :=
 rfl
 
 def refl (α) : α ≃ α := ⟨id, id, λ _ => rfl, λ _ => rfl⟩
 
-def symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩
+instance : Inhabited (α ≃ α) := ⟨Equiv.refl α⟩
+
+def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun, e.rightInv, e.leftInv⟩
+
 
 def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 ⟨e₂ ∘ (e₁ : α → β), e₁.symm ∘ (e₂.symm : γ → β),
-  e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
+  e₂.leftInv.comp e₁.leftInv, e₂.rightInv.comp e₁.rightInv⟩
+
+theorem to_fun_as_coe (e : α ≃ β) : e.toFun = e := rfl
+
+@[simp] theorem inv_fun_as_coe (e : α ≃ β) : e.invFun = e.symm := rfl
 
 @[simp] theorem apply_symm_apply  (e : α ≃ β) (x : β) : e (e.symm x) = x :=
-e.right_inv x
+e.rightInv x
 
 @[simp] theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x :=
-e.left_inv x
+e.leftInv x
 
 @[simp] theorem symm_comp_self (e : α ≃ β) : e.symm ∘ (e : α → β) = id := funext e.symm_apply_apply
 
 @[simp] theorem self_comp_symm (e : α ≃ β) : e ∘ (e.symm : β → α) = id := funext e.apply_symm_apply
 
-end equiv
+end Equiv

Mathlib/Data/Equiv/Functor.lean

@@ -16,7 +16,7 @@ def functor.map_equiv (f : Type u → Type v) [functor f] [is_lawful_functor f]
 
 -/
 
-open equiv
+open Equiv
 
 namespace Functor
 
@@ -29,10 +29,10 @@ theorem map_map (m : α → β) (g : β → γ) (x : f α) :
 
 /-- Apply a functor to an `equiv`. -/
 def map_equiv (h : α ≃ β) : f α ≃ f β where
-  to_fun    := map h
-  inv_fun   := map h.symm
-  left_inv x := by simp [map_map]
-  right_inv x := by simp [map_map]
+  toFun    := map h
+  invFun   := map h.symm
+  leftInv x := by simp [map_map]
+  rightInv x := by simp [map_map]
 
 @[simp]
 lemma map_equiv_apply (h : α ≃ β) (x : f α) :

Mathlib/Data/List/Basic.lean

@@ -2,6 +2,9 @@ import Mathlib.Logic.Basic
 import Mathlib.Data.Nat.Basic
 import Mathlib.Init.SetNotation
 import Lean
+
+open Function
+
 namespace List
 
 /-- The same as append, but with simpler defeq. (The one in the standard library is more efficient,
@@ -293,10 +296,10 @@ theorem mem_map {f : α → β} {b} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a
          fun | ⟨_, Or.inl rfl, h⟩ => Or.inl h
              | ⟨l, Or.inr h₁, h₂⟩ => Or.inr ⟨l, h₁, h₂⟩⟩
 
--- theorem mem_map_of_injective {f : α → β} (H : injective f) {a : α} {l : List α} :
---   f a ∈ map f l ↔ a ∈ l :=
--- ⟨fun m => let ⟨a', m', e⟩ := exists_of_mem_map m
---           H e ▸ m', mem_map_of_mem _⟩
+theorem mem_map_of_injective {f : α → β} (H : injective f) {a : α} {l : List α} :
+  f a ∈ map f l ↔ a ∈ l :=
+⟨fun m => let ⟨a', m', e⟩ := exists_of_mem_map m
+          H e ▸ m', mem_map_of_mem _⟩
 
 lemma forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
   (∀ i ∈ l.map f, P i) ↔ ∀ j ∈ l, P (f j) := by
@@ -763,16 +766,17 @@ lemma append_ne_nil_of_left_ne_nil (a b : List α) (h0 : a ≠ []) : a ++ b ≠
 | 0 => []
 | Nat.succ n => a :: repeat a n
 
-theorem repeatSucc (a: α) (n: ℕ) : repeat a (n + 1) = a :: repeat a n := rfl
-theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
-  b ∈ List.bind l f → ∃ a, a ∈ l ∧ b ∈ f a :=
-mem_bind.1
-
 @[simp] lemma length_repeat (a : α) (n : ℕ) : length (repeat a n) = n := by
 induction n with
 | zero => simp
 | succ x ih => simp; assumption
 
+theorem repeat_succ (a: α) (n: ℕ) : repeat a (n + 1) = a :: repeat a n := rfl
+
+theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
+  b ∈ List.bind l f → ∃ a, a ∈ l ∧ b ∈ f a :=
+mem_bind.1
+
 /-! ### insert -/
 section insert
 variable [DecidableEq α]

Mathlib/Logic/Function/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Logic.Basic
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Function
 import Mathlib.Init.Set
 import Mathlib.Init.SetNotation
@@ -585,7 +586,8 @@ end uncurry
 /-- A function is involutive, if `f ∘ f = id`. -/
 def involutive {α} (f : α → α) : Prop := ∀ x, f (f x) = x
 
--- TODO: involutive_iff_iter_2_eq_id
+lemma involutive_iff_iter_2_eq_id {α} {f : α → α} : involutive f ↔ (f^[2] = id) :=
+funext_iff.symm
 
 namespace involutive
 variable {α : Sort u} {f : α → α} (h : involutive f)