chore(*): bump to lean-3.12.0 (#2681)

## Changes to bracket notation

* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.

## Tactic `norm_num`

The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.

## Tactic combinators

leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.

## Tactic `case`

leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.

Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.11.0"
+lean_version = "leanprover-community/lean:3.12.0"
 path = "src"
 
 [dependencies]

src/algebra/big_operators.lean

@@ -147,7 +147,7 @@ eq.trans fold_singleton $ mul_one _
 @[to_additive]
 lemma prod_pair [decidable_eq α] {a b : α} (h : a ≠ b) :
   (∏ x in ({a, b} : finset α), f x) = f a * f b :=
-by simp [prod_insert (not_mem_singleton.2 h.symm), mul_comm]
+by rw [prod_insert (not_mem_singleton.2 h), prod_singleton]
 
 @[simp, priority 1100] lemma prod_const_one : (∏ x in s, (1 : β)) = 1 :=
 by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow]
@@ -358,7 +358,7 @@ by simp [prod_apply_ite _ _ (λ x, x)]
 begin
   rw ←finset.prod_filter,
   split_ifs;
-  simp only [filter_eq, if_true, if_false, h, prod_empty, prod_singleton, insert_empty_eq_singleton],
+  simp only [filter_eq, if_true, if_false, h, prod_empty, prod_singleton],
 end
 
 /--
@@ -879,8 +879,8 @@ open_locale classical
 lemma prod_add (f g : α → β) (s : finset α) :
   ∏ a in s, (f a + g a) = ∑ t in s.powerset, ((∏ a in t, f a) * (∏ a in (s \ t), g a)) :=
 calc ∏ a in s, (f a + g a)
-    = ∏ a in s, ∑ p in ({false, true} : finset Prop), if p then f a else g a : by simp
-... = ∑ p in (s.pi (λ _, {false, true}) : finset (Π a ∈ s, Prop)),
+    = ∏ a in s, ∑ p in ({true, false} : finset Prop), if p then f a else g a : by simp
+... = ∑ p in (s.pi (λ _, {true, false}) : finset (Π a ∈ s, Prop)),
         ∏ a in s.attach, if p a.1 a.2 then f a.1 else g a.1 : prod_sum
 ... = ∑ t in s.powerset, (∏ a in t, f a) * (∏ a in (s \ t), g a) : begin
   refine eq.symm (sum_bij (λ t _ a _, a ∈ t) _ _ _ _),
@@ -983,7 +983,7 @@ lemma sum_eq_zero_iff_of_nonpos : (∀x∈s, f x ≤ 0) → ((∑ x in s, f x) =
 @sum_eq_zero_iff_of_nonneg _ (order_dual β) _ _ _
 
 lemma single_le_sum (hf : ∀x∈s, 0 ≤ f x) {a} (h : a ∈ s) : f a ≤ (∑ x in s, f x) :=
-have (singleton a).sum f ≤ (∑ x in s, f x),
+have ({a} : finset α).sum f ≤ (∑ x in s, f x),
   from sum_le_sum_of_subset_of_nonneg
   (λ x e, (mem_singleton.1 e).symm ▸ h) (λ x h _, hf x h),
 by rwa sum_singleton at this
@@ -1209,7 +1209,7 @@ multiset.induction_on s rfl
       ... = card (a :: s) :
       begin
         by_cases a ∈ s.to_finset,
-        { have : (to_finset s).sum (λx, ite (x = a) 1 0) = (finset.singleton a).sum (λx, ite (x = a) 1 0),
+        { have : (to_finset s).sum (λx, ite (x = a) 1 0) = ({a} : finset α).sum (λx, ite (x = a) 1 0),
           { apply (finset.sum_subset _ _).symm,
             { intros _ H, rwa mem_singleton.1 H },
             { exact λ _ _ H, if_neg (mt finset.mem_singleton.2 H) } },

src/algebra/classical_lie_algebras.lean

@@ -43,10 +43,8 @@ namespace special_linear
 
 /-- The special linear Lie algebra: square matrices of trace zero. -/
 def sl : lie_subalgebra R (matrix n n R) :=
-{ lie_mem := λ X Y _ _, by
-  { suffices : matrix.trace n R R ⁅X, Y⁆ = 0, apply (list.mem_pure _ 0).2 this,
-    apply matrix_trace_commutator_zero, },
-  ..linear_map.ker (matrix.trace n R R) }
+{ lie_mem := λ X Y _ _, linear_map.mem_ker.2 $ matrix_trace_commutator_zero _ _ _ _,
+  to_submodule := linear_map.ker (matrix.trace n R R) }
 
 lemma sl_bracket (A B : sl n R) : ⁅A, B⁆.val = A.val ⬝ B.val - B.val ⬝ A.val := rfl
 

src/algebra/direct_limit.lean

@@ -355,31 +355,34 @@ begin
   refine span_induction (ideal.quotient.eq_zero_iff_mem.1 H) _ _ _ _,
   { rintros x (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩),
     { refine ⟨j, {⟨i, x⟩, ⟨j, f i j hij x⟩}, _,
-        is_supported_sub (is_supported_of.2 $ or.inl rfl) (is_supported_of.2 $ or.inr $ or.inl rfl), _⟩,
-      { rintros k (rfl | ⟨rfl | h⟩), refl, exact hij, cases h },
+        is_supported_sub (is_supported_of.2 $ or.inr rfl) (is_supported_of.2 $ or.inl rfl), _⟩,
+      { rintros k (rfl | ⟨rfl | _⟩), exact hij, refl },
       { rw [restriction_sub, lift_sub, restriction_of, dif_pos, restriction_of, dif_pos, lift_of, lift_of],
         dsimp only, rw directed_system.map_map f, exact sub_self _,
-        { left, refl }, { right, left, refl }, } },
-    { refine ⟨i, {⟨i, 1⟩}, _, is_supported_sub (is_supported_of.2 $ or.inl rfl) is_supported_one, _⟩,
-      { rintros k (rfl | h), refl, cases h },
+        exacts [or.inr rfl, or.inl rfl] } },
+    { refine ⟨i, {⟨i, 1⟩}, _, is_supported_sub (is_supported_of.2 rfl) is_supported_one, _⟩,
+      { rintros k (rfl|h), refl },
       { rw [restriction_sub, lift_sub, restriction_of, dif_pos, restriction_one, lift_of, lift_one],
-        dsimp only, rw [is_ring_hom.map_one (f i i _), sub_self], exact _inst_7 i i _, { left, refl } } },
+        dsimp only, rw [is_ring_hom.map_one (f i i _), sub_self], exacts [_inst_7 i i _, rfl] } },
     { refine ⟨i, {⟨i, x+y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
-        is_supported_sub (is_supported_of.2 $ or.inr $ or.inr $ or.inl rfl)
-          (is_supported_add (is_supported_of.2 $ or.inr $ or.inl rfl) (is_supported_of.2 $ or.inl rfl)), _⟩,
-      { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩), refl, refl, refl, cases hk },
+        is_supported_sub (is_supported_of.2 $ or.inl rfl)
+          (is_supported_add (is_supported_of.2 $ or.inr $ or.inl rfl)
+            (is_supported_of.2 $ or.inr $ or.inr rfl)), _⟩,
+      { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩); refl },
       { rw [restriction_sub, restriction_add, restriction_of, restriction_of, restriction_of,
           dif_pos, dif_pos, dif_pos, lift_sub, lift_add, lift_of, lift_of, lift_of],
         dsimp only, rw is_ring_hom.map_add (f i i _), exact sub_self _,
-        { right, right, left, refl }, { apply_instance }, { left, refl }, { right, left, refl } } },
+        exacts [or.inl rfl, by apply_instance, or.inr (or.inr rfl), or.inr (or.inl rfl)] } },
     { refine ⟨i, {⟨i, x*y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
-        is_supported_sub (is_supported_of.2 $ or.inr $ or.inr $ or.inl rfl)
-          (is_supported_mul (is_supported_of.2 $ or.inr $ or.inl rfl) (is_supported_of.2 $ or.inl rfl)), _⟩,
-      { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩), refl, refl, refl, cases hk },
+        is_supported_sub (is_supported_of.2 $ or.inl rfl)
+          (is_supported_mul (is_supported_of.2 $ or.inr $ or.inl rfl)
+            (is_supported_of.2 $ or.inr $ or.inr rfl)), _⟩,
+      { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩); refl },
       { rw [restriction_sub, restriction_mul, restriction_of, restriction_of, restriction_of,
           dif_pos, dif_pos, dif_pos, lift_sub, lift_mul, lift_of, lift_of, lift_of],
-        dsimp only, rw is_ring_hom.map_mul (f i i _), exact sub_self _,
-        { right, right, left, refl }, { apply_instance }, { left, refl }, { right, left, refl } } } },
+        dsimp only, rw is_ring_hom.map_mul (f i i _),
+        exacts [sub_self _, or.inl rfl, by apply_instance, or.inr (or.inr rfl),
+          or.inr (or.inl rfl)] } } },
   { refine nonempty.elim (by apply_instance) (assume ind : ι, _),
     refine ⟨ind, ∅, λ _, false.elim, is_supported_zero, _⟩,
     rw [restriction_zero, lift_zero] },

src/algebra/direct_sum.lean

@@ -130,7 +130,7 @@ is_add_group_hom.map_neg _ x
 is_add_group_hom.map_sub _ x y
 
 @[simp] lemma to_group_of (i) (x : β i) : to_group φ (of β i x) = φ i x :=
-(add_zero _).trans $ congr_arg (φ i) $ show (if H : i ∈ finset.singleton i then x else 0) = x,
+(add_zero _).trans $ congr_arg (φ i) $ show (if H : i ∈ ({i} : finset _) then x else 0) = x,
 from dif_pos $ finset.mem_singleton_self i
 
 variables (ψ : direct_sum ι β → γ) [is_add_group_hom ψ]

src/analysis/analytic/composition.lean

@@ -220,7 +220,7 @@ lemma comp_coeff_zero (q : formal_multilinear_series 𝕜 F G) (p : formal_multi
 begin
   let c : composition 0 := composition.ones 0,
   dsimp [formal_multilinear_series.comp],
-  have : finset.singleton c = (finset.univ : finset (composition 0)),
+  have : {c} = (finset.univ : finset (composition 0)),
   { apply finset.eq_of_subset_of_card_le; simp [finset.card_univ, composition_card 0] },
   rw ← this,
   simp only [finset.sum_singleton, continuous_multilinear_map.sum_apply],

src/analysis/convex/basic.lean

@@ -527,7 +527,7 @@ noncomputable def finset.center_mass (t : finset ι) (w : ι → ℝ) (z : ι 
 
 variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι → ℝ) (z : ι → E)
 
-open finset (hiding singleton)
+open finset
 
 lemma finset.center_mass_empty : (∅ : finset ι).center_mass w z = 0 :=
 by simp only [center_mass, sum_empty, smul_zero]
@@ -548,7 +548,7 @@ begin
   { rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div_eq_inv] }
 end
 
-lemma finset.center_mass_singleton (hw : w i ≠ 0) : (finset.singleton i).center_mass w z = z i :=
+lemma finset.center_mass_singleton (hw : w i ≠ 0) : ({i} : finset ι).center_mass w z = z i :=
 by rw [center_mass, sum_singleton, sum_singleton, ← mul_smul, inv_mul_cancel hw, one_smul]
 
 lemma finset.center_mass_eq_of_sum_1 (hw : t.sum w = 1) :
@@ -759,7 +759,7 @@ lemma convex_hull_eq (s : set E) :
 begin
   refine subset.antisymm (convex_hull_min _ _) _,
   { intros x hx,
-    use [punit, finset.singleton punit.star, λ _, 1, λ _, x, λ _ _, zero_le_one,
+    use [punit, {punit.star}, λ _, 1, λ _, x, λ _ _, zero_le_one,
       finset.sum_singleton, λ _ _, hx],
     simp only [finset.center_mass, finset.sum_singleton, inv_one, one_smul] },
   { rintros x y ⟨ι, sx, wx, zx, hwx₀, hwx₁, hzx, rfl⟩ ⟨ι', sy, wy, zy, hwy₀, hwy₁, hzy, rfl⟩

src/analysis/special_functions/trigonometric.lean

@@ -1160,7 +1160,7 @@ lt_of_le_of_ne (neg_pi_div_two_le_arcsin _)
         (le_of_lt (div_sqrt_one_add_lt_one _)), ← arctan, ← h, sin_neg, sin_pi_div_two])
 
 lemma tan_surjective : function.surjective tan :=
-function.surjective_of_has_right_inverse ⟨_, tan_arctan⟩
+function.right_inverse.surjective tan_arctan
 
 lemma arctan_tan {x : ℝ} (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) : arctan (tan x) = x :=
 tan_inj_of_lt_of_lt_pi_div_two (neg_pi_div_two_lt_arctan _)

src/computability/reduce.lean

@@ -74,7 +74,7 @@ theorem one_one_reducible_refl {α} [primcodable α] (p : α → Prop) :
 @[trans]
 theorem one_one_reducible.trans {α β γ} [primcodable α] [primcodable β] [primcodable γ]
   {p : α → Prop} {q : β → Prop} {r : γ → Prop} : p ≤₁ q → q ≤₁ r → p ≤₁ r
-| ⟨f, c₁, i₁, h₁⟩ ⟨g, c₂, i₂, h₂⟩ := ⟨g ∘ f, c₂.comp c₁, injective_comp i₂ i₁,
+| ⟨f, c₁, i₁, h₁⟩ ⟨g, c₂, i₂, h₂⟩ := ⟨g ∘ f, c₂.comp c₁, i₂.comp i₁,
   λ a, ⟨λ h, by rwa [←h₂, ←h₁], λ h, by rwa [h₁, h₂]⟩⟩
 
 theorem one_one_reducible.to_many_one {α β} [primcodable α] [primcodable β]

src/computability/turing_machine.lean

@@ -1079,16 +1079,15 @@ noncomputable def stmts₁ : stmt → finset stmt
 | Q                  := {Q}
 
 theorem stmts₁_self {q} : q ∈ stmts₁ q :=
-by cases q; apply finset.mem_insert_self
+by cases q; apply_rules [finset.mem_insert_self, finset.mem_singleton_self]
 
 theorem stmts₁_trans {q₁ q₂} :
   q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ :=
 begin
   intros h₁₂ q₀ h₀₁,
   induction q₂ with _ q IH _ q IH _ q IH;
     simp only [stmts₁] at h₁₂ ⊢;
-    simp only [finset.mem_insert, finset.mem_union,
-      finset.insert_empty_eq_singleton, finset.mem_singleton] at h₁₂,
+    simp only [finset.mem_insert, finset.mem_union, finset.mem_singleton] at h₁₂,
   iterate 3 {
     rcases h₁₂ with rfl | h₁₂,
     { unfold stmts₁ at h₀₁, exact h₀₁ },
@@ -1109,7 +1108,7 @@ theorem stmts₁_supports_stmt_mono {S q₁ q₂}
 begin
   induction q₂ with _ q IH _ q IH _ q IH;
     simp only [stmts₁, supports_stmt, finset.mem_insert, finset.mem_union,
-      finset.insert_empty_eq_singleton, finset.mem_singleton] at h hs,
+      finset.mem_singleton] at h hs,
   iterate 3 { rcases h with rfl | h; [exact hs, exact IH h hs] },
   case TM1.stmt.branch : p q₁ q₂ IH₁ IH₂ {
     rcases h with rfl | h | h, exacts [hs, IH₁ h hs.1, IH₂ h hs.2] },
@@ -1846,16 +1845,15 @@ noncomputable def stmts₁ : stmt → finset stmt
 | Q@halt             := {Q}
 
 theorem stmts₁_self {q} : q ∈ stmts₁ q :=
-by cases q; apply finset.mem_insert_self
+by cases q; apply_rules [finset.mem_insert_self, finset.mem_singleton_self]
 
 theorem stmts₁_trans {q₁ q₂} :
   q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ :=
 begin
   intros h₁₂ q₀ h₀₁,
   induction q₂ with _ _ q IH _ _ q IH _ _ q IH _ q IH;
     simp only [stmts₁] at h₁₂ ⊢;
-    simp only [finset.mem_insert, finset.insert_empty_eq_singleton,
-      finset.mem_singleton, finset.mem_union] at h₁₂,
+    simp only [finset.mem_insert, finset.mem_singleton, finset.mem_union] at h₁₂,
   iterate 4 {
     rcases h₁₂ with rfl | h₁₂,
     { unfold stmts₁ at h₀₁, exact h₀₁ },
@@ -1876,7 +1874,7 @@ theorem stmts₁_supports_stmt_mono {S q₁ q₂}
 begin
   induction q₂ with _ _ q IH _ _ q IH _ _ q IH _ q IH;
     simp only [stmts₁, supports_stmt, finset.mem_insert, finset.mem_union,
-      finset.insert_empty_eq_singleton, finset.mem_singleton] at h hs,
+      finset.mem_singleton] at h hs,
   iterate 4 { rcases h with rfl | h; [exact hs, exact IH h hs] },
   case TM2.stmt.branch : f q₁ q₂ IH₁ IH₂ {
     rcases h with rfl | h | h, exacts [hs, IH₁ h hs.1, IH₂ h hs.2] },
@@ -2200,14 +2198,14 @@ begin
           list.length_reverse, list.length_append, list.length_map] } },
     { split_ifs; rw [function.update_noteq h', ← proj_map_nth, hL],
       rw function.update_noteq h' } },
-  case TM2to1.st_act.peek : b f {
+  case TM2to1.st_act.peek : f {
     rw function.update_eq_self,
     use [L, hL], rw [tape.move_left_right], congr,
     cases e : S k, {refl},
     rw [list.length_cons, nat.iterate_succ', tape.move_right_left, tape.move_right_n_head,
       tape.mk'_nth_nat, add_bottom_nth_snd, stk_nth_val _ (hL k), e,
       list.reverse_cons, ← list.length_reverse, list.nth_concat_length], refl },
-  case TM2to1.st_act.pop : b f {
+  case TM2to1.st_act.pop : f {
     cases e : S k,
     { simp only [tape.mk'_head, list_blank.head_cons, tape.move_left_mk',
         list.length, tape.write_mk', list.head', nat.iterate_zero, list.tail_nil],
@@ -2385,24 +2383,22 @@ theorem tr_supports {S} (ss : TM2.supports M S) :
   { -- stack op
     rw TM2to1.supports_run at ss',
     simp only [TM2to1.tr_stmts₁_run, finset.mem_union,
-      finset.insert_empty_eq_singleton,
       finset.mem_insert, finset.mem_singleton] at sub,
-    have hgo := sub _ (or.inl $ or.inr rfl),
-    have hret := sub _ (or.inl $ or.inl rfl),
+    have hgo := sub _ (or.inl $ or.inl rfl),
+    have hret := sub _ (or.inl $ or.inr rfl),
     cases IH ss' (λ x hx, sub x $ or.inr hx) with IH₁ IH₂,
     refine ⟨by simp only [tr_normal_run, TM1.supports_stmt]; intros; exact hgo, λ l h, _⟩,
     rw [tr_stmts₁_run] at h,
     simp only [TM2to1.tr_stmts₁_run, finset.mem_union,
-      finset.insert_empty_eq_singleton,
       finset.mem_insert, finset.mem_singleton] at h,
     rcases h with ⟨rfl | rfl⟩ | h,
-    { unfold TM1.supports_stmt TM2to1.tr,
-      exact ⟨IH₁, λ _ _, hret⟩ },
     { unfold TM1.supports_stmt TM2to1.tr,
       rcases s with _|_|_,
       { exact ⟨λ _ _, hret, λ _ _, hgo⟩ },
       { exact ⟨λ _ _, hret, λ _ _, hgo⟩ },
       { exact ⟨⟨λ _ _, hret, λ _ _, hret⟩, λ _ _, hgo⟩ } },
+    { unfold TM1.supports_stmt TM2to1.tr,
+      exact ⟨IH₁, λ _ _, hret⟩ },
     { exact IH₂ _ h } },
   { -- load
     unfold TM2to1.tr_stmts₁ at ss' sub ⊢,

src/data/dfinsupp.lean

@@ -279,21 +279,21 @@ end
 /-- The function `single i b : Π₀ i, β i` sends `i` to `b`
 and all other points to `0`. -/
 def single (i : ι) (b : β i) : Π₀ i, β i :=
-mk (finset.singleton i) $ λ j, eq.rec_on (finset.mem_singleton.1 j.2).symm b
+mk {i} $ λ j, eq.rec_on (finset.mem_singleton.1 j.2).symm b
 
 @[simp] lemma single_apply {i i' b} :
   (single i b : Π₀ i, β i) i' = (if h : i = i' then eq.rec_on h b else 0) :=
 begin
   dsimp only [single],
   by_cases h : i = i',
-  { have h1 : i' ∈ finset.singleton i, { simp only [h, finset.mem_singleton] },
+  { have h1 : i' ∈ ({i} : finset ι) := finset.mem_singleton.2 h.symm,
     simp only [mk_apply, dif_pos h, dif_pos h1] },
-  { have h1 : i' ∉ finset.singleton i, { simp only [ne.symm h, finset.mem_singleton, not_false_iff] },
+  { have h1 : i' ∉ ({i} : finset ι) := finset.not_mem_singleton.2 (ne.symm h),
     simp only [mk_apply, dif_neg h, dif_neg h1] }
 end
 
 @[simp] lemma single_zero {i} : (single i 0 : Π₀ i, β i) = 0 :=
-quotient.sound $ λ j, if H : j ∈ finset.singleton i
+quotient.sound $ λ j, if H : j ∈ ({i} : finset _)
 then by dsimp only; rw [dif_pos H]; cases finset.mem_singleton.1 H; refl
 else dif_neg H
 

src/data/equiv/basic.lean

@@ -46,7 +46,7 @@ theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : equiv α β}, (e₁ : α → β) = e
   have g₁ = g₂, from funext $ assume x,
     have f₁ (g₁ x) = f₂ (g₂ x), from (r₁ x).trans (r₂ x).symm,
     have f₁ (g₁ x) = f₁ (g₂ x), by { subst f₂, exact this },
-    show g₁ x = g₂ x,           from injective_of_left_inverse l₁ this,
+    show g₁ x = g₂ x,           from l₁.injective this,
   by simp *
 
 @[ext] lemma ext (f g : equiv α β) (H : ∀ x, f x = g x) : f = g :=
@@ -70,10 +70,10 @@ lemma to_fun_as_coe (e : α ≃ β) (a : α) : e.to_fun a = e a := rfl
 lemma inv_fun_as_coe (e : α ≃ β) (b : β) : e.inv_fun b = e.symm b := rfl
 
 protected theorem injective : ∀ f : α ≃ β, injective f
-| ⟨f, g, h₁, h₂⟩ := injective_of_left_inverse h₁
+| ⟨f, g, h₁, h₂⟩ := h₁.injective
 
 protected theorem surjective : ∀ f : α ≃ β, surjective f
-| ⟨f, g, h₁, h₂⟩ := surjective_of_has_right_inverse ⟨_, h₂⟩
+| ⟨f, g, h₁, h₂⟩ := h₂.surjective
 
 protected theorem bijective (f : α ≃ β) : bijective f :=
 ⟨f.injective, f.surjective⟩
@@ -109,8 +109,8 @@ rfl
 @[simp] lemma symm_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
   (f.trans g).symm a = f.symm (g.symm a) := rfl
 
-@[simp] theorem apply_eq_iff_eq : ∀ (f : α ≃ β) (x y : α), f x = f y ↔ x = y
-| ⟨f₁, g₁, l₁, r₁⟩ x y := (injective_of_left_inverse l₁).eq_iff
+@[simp] theorem apply_eq_iff_eq (f : α ≃ β) (x y : α) : f x = f y ↔ x = y :=
+f.injective.eq_iff
 
 theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) (x : α) (y : β) :
   f x = y ↔ x = f.symm y :=
@@ -716,7 +716,7 @@ end
 def list_equiv_of_equiv {α β : Type*} : α ≃ β → list α ≃ list β
 | ⟨f, g, l, r⟩ :=
   by refine ⟨list.map f, list.map g, λ x, _, λ x, _⟩;
-     simp [id_of_left_inverse l, id_of_right_inverse r]
+     simp [l.comp_eq_id, r.comp_eq_id]
 
 def fin_equiv_subtype (n : ℕ) : fin n ≃ {m // m < n} :=
 ⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨x.1, x.2⟩, λ ⟨a, b⟩, rfl,λ ⟨a, b⟩, rfl⟩

src/data/equiv/mul_add.lean

@@ -77,7 +77,7 @@ def refl (M : Type*) [has_mul M] : M ≃* M :=
 /-- The inverse of an isomorphism is an isomorphism. -/
 @[symm, to_additive]
 def symm (h : M ≃* N) : N ≃* M :=
-{ map_mul' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
+{ map_mul' := λ n₁ n₂, h.left_inv.injective begin
     show h.to_equiv (h.to_equiv.symm (n₁ * n₂)) =
       h ((h.to_equiv.symm n₁) * (h.to_equiv.symm n₂)),
    rw h.map_mul,

src/data/fin_enum.lean

@@ -12,7 +12,7 @@ than `fintype` in that it assigns each element a rank in a finite
 enumeration.
 -/
 
-open finset (hiding singleton)
+open finset
 
 /-- `fin_enum α` means that `α` is finite and can be enumerated in some order,
   i.e. `α` has an explicit bijection with `fin n` for some n. -/
@@ -111,11 +111,11 @@ begin
       { exact or.inl hx },
       { exact or.inr (h _ hx) }  },
     intro h, existsi s \ ({xs_hd} : finset α),
-    simp only [and_imp, union_comm, mem_sdiff, insert_empty_eq_singleton, mem_singleton],
+    simp only [and_imp, union_comm, mem_sdiff, mem_singleton],
     simp only [or_iff_not_imp_left] at h,
     existsi h,
     by_cases xs_hd ∈ s,
-    { have : finset.singleton xs_hd ⊆ s, simp only [has_subset.subset, *, forall_eq, mem_singleton],
+    { have : {xs_hd} ⊆ s, simp only [has_subset.subset, *, forall_eq, mem_singleton],
       simp only [union_sdiff_of_subset this, or_true, finset.union_sdiff_of_subset, eq_self_iff_true], },
     { left, symmetry, simp only [sdiff_eq_self],
       intro a, simp only [and_imp, mem_inter, mem_singleton, not_mem_empty],