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>

Author: 4 people

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 ⊢,