feat(data/equiv/basic): improve arrow_congr, define conj (#1119)

* feat(data/equiv/basic): improve arrow_congr, define conj

- redefine `equiv.arrow_congr` without an enclosing `match`
- prove some trivial lemmas about `equiv.arrow_congr`
- define `equiv.conj`, and prove trivial lemmas about it

* chore(data/equiv/basic): add @[simp]

Also split some long lines, and swap lhs with rhs in a few lemmas.

* Reorder, drop TODO

src/data/equiv/basic.lean

@@ -212,12 +212,52 @@ protected def ulift {α : Type u} : ulift α ≃ α :=
 protected def plift : plift α ≃ α :=
 ⟨plift.down, plift.up, plift.up_down, plift.down_up⟩
 
-@[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} : α₁ ≃ α₂ → β₁ ≃ β₂ → (α₁ → β₁) ≃ (α₂ → β₂)
-| ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ :=
-  ⟨λ (h : α₁ → β₁) (a : α₂), f₂ (h (g₁ a)),
-   λ (h : α₂ → β₂) (a : α₁), g₂ (h (f₁ a)),
-   λ h, by funext a; dsimp; rw [l₁, l₂],
-   λ h, by funext a; dsimp; rw [r₁, r₂]⟩
+@[congr] def arrow_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
+  (α₁ → β₁) ≃ (α₂ → β₂) :=
+{ to_fun := λ f, e₂.to_fun ∘ f ∘ e₁.inv_fun,
+  inv_fun := λ f, e₂.inv_fun ∘ f ∘ e₁.to_fun,
+  left_inv := λ f, funext $ λ x, by dsimp; rw [e₂.left_inv, e₁.left_inv],
+  right_inv := λ f, funext $ λ x, by dsimp; rw [e₂.right_inv, e₁.right_inv] }
+
+@[simp] lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂)
+  (f : α₁ → β₁) (x : α₂) :
+  arrow_congr e₁ e₂ f x = (e₂ $ f $ e₁.symm x) :=
+rfl
+
+lemma arrow_congr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*}
+  (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :
+  arrow_congr ea ec (g ∘ f) = (arrow_congr eb ec g) ∘ (arrow_congr ea eb f) :=
+by ext; simp only [comp, arrow_congr_apply, eb.symm_apply_apply]
+
+@[simp] lemma arrow_congr_refl {α β : Sort*} :
+  arrow_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α → β) := rfl
+
+@[simp] lemma arrow_congr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*}
+  (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
+  arrow_congr (e₁.trans e₂) (e₁'.trans e₂') = (arrow_congr e₁ e₁').trans (arrow_congr e₂ e₂') :=
+rfl
+
+@[simp] lemma arrow_congr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
+  (arrow_congr e₁ e₂).symm = arrow_congr e₁.symm e₂.symm :=
+rfl
+
+def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrow_congr e e
+
+@[simp] lemma conj_apply (e : α ≃ β) (f : α → α) (x : β) :
+  e.conj f x = (e $ f $ e.symm x) :=
+rfl
+
+@[simp] lemma conj_refl : conj (equiv.refl α) = equiv.refl (α → α) := rfl
+
+@[simp] lemma conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj := rfl
+
+@[simp] lemma conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
+  (e₁.trans e₂).conj = e₁.conj.trans e₂.conj :=
+rfl
+
+@[simp] lemma conj_comp (e : α ≃ β) (f₁ f₂ : α → α) :
+  e.conj (f₁ ∘ f₂) = (e.conj f₁) ∘ (e.conj f₂) :=
+by apply arrow_congr_comp
 
 def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
 ⟨λ _, punit.star, λ _, punit.star, λ u, by cases u; refl, λ u, by cases u; reflexivity⟩