chore(*): switch to lean 3.10.0 (#2587)

There have been two changes in Lean 3.10 that have a significant effect on mathlib:

 - `rename'` has been moved to core.  Therefore `rename'` has been removed.

 - Given a term `⇑f x`, the simplifier can now rewrite in both `f` and `x`.  In many cases we had both `⇑f = ⇑f'` and `⇑f x = ⇑f' x` as simp lemmas; the latter is redundant now and has been removed (or just not marked simp anymore).  The new and improved congruence lemmas are also used by `convert` and `congr`, these tactics have become more powerful as well.

I've also sneaked in two related changes that I noticed while fixing the proofs affected by the changes above:

 - `@[to_additive, simp]` has been replaced by `@[simp, to_additive]` in the monoid localization file.  The difference is that `@[to_additive, simp]` only marks the multiplicative lemma as simp.

 - `def prod_comm : α × β ≃ β × α` (etc.) is no longer marked `@[simp]`.  Marking this kind of lemmas as simp causes the simplifier to unfold the definition of `prod_comm` (instead of just rewriting `α × β` to `β × α` in the `≃` simp relation).  This has become a bigger issue now since the simplifier can rewrite the `f` in `⇑f x`.

Co-authored-by: Jannis Limperg <jannis@limperg.de>

Author: gebner

leanpkg.toml

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

src/algebra/category/Group/Z_Module_equivalence.lean

@@ -22,11 +22,7 @@ instance : full (forget₂ (Module ℤ) AddCommGroup) :=
 { preimage := λ A B f,
   { to_fun := f,
     add := λ x y, add_monoid_hom.map_add f x y,
-    smul := λ n x,
-    begin
-      convert add_monoid_hom.map_int_module_smul f n x,
-      apply congr_arg, congr,
-    end } }
+    smul := λ n x, by convert add_monoid_hom.map_int_module_smul f n x } }
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
 instance : ess_surj (forget₂ (Module ℤ) AddCommGroup) :=

src/analysis/calculus/times_cont_diff.lean

@@ -1182,7 +1182,7 @@ lemma iterated_fderiv_within_zero_fun {n : ℕ} :
   iterated_fderiv 𝕜 n (λ x : E, (0 : F)) = 0 :=
 begin
   induction n with n IH,
-  { ext m, simp, refl },
+  { ext m, simp },
   { ext x m,
     rw [iterated_fderiv_succ_apply_left, IH],
     change (fderiv 𝕜 (λ (x : E), (0 : (E [×n]→L[𝕜] F))) x : E → (E [×n]→L[𝕜] F)) (m 0) (tail m) = _,

src/analysis/normed_space/multilinear.lean

@@ -1014,7 +1014,8 @@ begin
   have : x = 0 := subsingleton.elim _ _, subst this,
   refine le_antisymm (by simpa using f.le_op_norm 0) _,
   have : ∥continuous_multilinear_map.curry0 𝕜 G (f.uncurry0)∥ ≤ ∥f.uncurry0∥ :=
-    continuous_multilinear_map.op_norm_le_bound _ (norm_nonneg _) (λm, by simp),
+    continuous_multilinear_map.op_norm_le_bound _ (norm_nonneg _) (λm,
+      by simp [-continuous_multilinear_map.apply_zero_curry0]),
   simpa
 end
 

src/category_theory/limits/concrete_category.lean

@@ -30,7 +30,7 @@ local attribute [instance] concrete_category.has_coe_to_fun
    (G.map f) ((s.π.app j) x) = (s.π.app j') x :=
 begin
   convert congr_fun (congr_arg (λ k : s.X ⟶ G.obj j', (k : s.X → G.obj j')) (s.π.naturality f).symm) x;
-  { dsimp, simp },
+  { dsimp, simp [-cone.w] },
 end
 
 end cone
@@ -48,7 +48,7 @@ local attribute [instance] concrete_category.has_coe_to_fun
   (s.ι.app j') ((G.map f) x) = (s.ι.app j) x :=
 begin
   convert congr_fun (congr_arg (λ k : G.obj j ⟶ s.X, (k : G.obj j → s.X)) (s.ι.naturality f)) x;
-  { dsimp, simp },
+  { dsimp, simp [-nat_trans.naturality, -cocone.w] },
 end
 
 end cocone

src/data/equiv/basic.lean

@@ -129,8 +129,6 @@ lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
 
 @[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl }
 
-@[simp] theorem symm_symm_apply (e : α ≃ β) (a : α) : e.symm.symm a = e a := by { cases e, refl }
-
 @[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by { cases e, refl }
 
 @[simp] theorem refl_symm : (equiv.refl α).symm = equiv.refl α := rfl
@@ -322,20 +320,20 @@ def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
 ⟨λ _, punit.star, λ _, punit.star, λ u, by { cases u, refl }, λ u, by { cases u, reflexivity }⟩
 
 section
-@[simp] def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
+def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
 ⟨λ f, punit.star, λ u f, punit.star,
   λ f, by { funext x, cases f x, refl }, λ u, by { cases u, reflexivity }⟩
 
-@[simp] def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
+def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
 ⟨λ f, f punit.star, λ a u, a, λ f, by { funext x, cases x, refl }, λ u, rfl⟩
 
-@[simp] def empty_arrow_equiv_punit (α : Sort*) : (empty → α) ≃ punit.{u} :=
+def empty_arrow_equiv_punit (α : Sort*) : (empty → α) ≃ punit.{u} :=
 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by { cases u, refl }⟩
 
-@[simp] def pempty_arrow_equiv_punit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
+def pempty_arrow_equiv_punit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by { cases u, refl }⟩
 
-@[simp] def false_arrow_equiv_punit (α : Sort*) : (false → α) ≃ punit.{u} :=
+def false_arrow_equiv_punit (α : Sort*) : (false → α) ≃ punit.{u} :=
 calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.refl _)
              ... ≃ punit       : empty_arrow_equiv_punit _
 
@@ -350,37 +348,39 @@ end
   prod_congr e₁ e₂ (a, b) = (e₁ a, e₂ b) :=
 rfl
 
-@[simp] def prod_comm (α β : Sort*) : α × β ≃ β × α :=
+def prod_comm (α β : Sort*) : α × β ≃ β × α :=
 ⟨λ p, (p.2, p.1), λ p, (p.2, p.1), λ⟨a, b⟩, rfl, λ⟨a, b⟩, rfl⟩
 
-@[simp] def prod_assoc (α β γ : Sort*) : (α × β) × γ ≃ α × (β × γ) :=
+@[simp] lemma prod_comm_apply {α β} (a b) : prod_comm α β ⟨a, b⟩ = ⟨b, a⟩ := rfl
+
+def prod_assoc (α β γ : Sort*) : (α × β) × γ ≃ α × (β × γ) :=
 ⟨λ p, ⟨p.1.1, ⟨p.1.2, p.2⟩⟩, λp, ⟨⟨p.1, p.2.1⟩, p.2.2⟩, λ ⟨⟨a, b⟩, c⟩, rfl, λ ⟨a, ⟨b, c⟩⟩, rfl⟩
 
 @[simp] theorem prod_assoc_apply {α β γ : Sort*} (p : (α × β) × γ) :
   prod_assoc α β γ p = ⟨p.1.1, ⟨p.1.2, p.2⟩⟩ := rfl
 
 section
-@[simp] def prod_punit (α : Sort*) : α × punit.{u+1} ≃ α :=
+def prod_punit (α : Sort*) : α × punit.{u+1} ≃ α :=
 ⟨λ p, p.1, λ a, (a, punit.star), λ ⟨_, punit.star⟩, rfl, λ a, rfl⟩
 
 @[simp] theorem prod_punit_apply {α : Sort*} (a : α × punit.{u+1}) : prod_punit α a = a.1 := rfl
 
-@[simp] def punit_prod (α : Sort*) : punit.{u+1} × α ≃ α :=
+def punit_prod (α : Sort*) : punit.{u+1} × α ≃ α :=
 calc punit × α ≃ α × punit : prod_comm _ _
            ... ≃ α         : prod_punit _
 
 @[simp] theorem punit_prod_apply {α : Sort*} (a : punit.{u+1} × α) : punit_prod α a = a.2 := rfl
 
-@[simp] def prod_empty (α : Sort*) : α × empty ≃ empty :=
+def prod_empty (α : Sort*) : α × empty ≃ empty :=
 equiv_empty (λ ⟨_, e⟩, e.rec _)
 
-@[simp] def empty_prod (α : Sort*) : empty × α ≃ empty :=
+def empty_prod (α : Sort*) : empty × α ≃ empty :=
 equiv_empty (λ ⟨e, _⟩, e.rec _)
 
-@[simp] def prod_pempty (α : Sort*) : α × pempty ≃ pempty :=
+def prod_pempty (α : Sort*) : α × pempty ≃ pempty :=
 equiv_pempty (λ ⟨_, e⟩, e.rec _)
 
-@[simp] def pempty_prod (α : Sort*) : pempty × α ≃ pempty :=
+def pempty_prod (α : Sort*) : pempty × α ≃ pempty :=
 equiv_pempty (λ ⟨e, _⟩, e.rec _)
 end
 
@@ -421,13 +421,17 @@ noncomputable def Prop_equiv_bool : Prop ≃ bool :=
 ⟨λ p, @to_bool p (classical.prop_decidable _),
  λ b, b, λ p, by simp, λ b, by simp⟩
 
-@[simp] def sum_comm (α β : Sort*) : α ⊕ β ≃ β ⊕ α :=
+def sum_comm (α β : Sort*) : α ⊕ β ≃ β ⊕ α :=
 ⟨λ s, match s with inl a := inr a | inr b := inl b end,
  λ s, match s with inl b := inr b | inr a := inl a end,
  λ s, by cases s; refl,
  λ s, by cases s; refl⟩
 
-@[simp] def sum_assoc (α β γ : Sort*) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
+@[simp] lemma sum_comm_apply_inl (α β) (a) : sum_comm α β (sum.inl a) = sum.inr a := rfl
+@[simp] lemma sum_comm_apply_inr (α β) (b) : sum_comm α β (sum.inr b) = sum.inl b := rfl
+@[simp] lemma sum_comm_symm (α β) : (sum_comm α β).symm = sum_comm β α := by ext x; cases x; refl
+
+def sum_assoc (α β γ : Sort*) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
 ⟨λ s, match s with inl (inl a) := inl a | inl (inr b) := inr (inl b) | inr c := inr (inr c) end,
  λ s, match s with inl a := inl (inl a) | inr (inl b) := inl (inr b) | inr (inr c) := inr c end,
  λ s, by rcases s with ⟨_ | _⟩ | _; refl,
@@ -437,30 +441,42 @@ noncomputable def Prop_equiv_bool : Prop ≃ bool :=
 @[simp] theorem sum_assoc_apply_in2 {α β γ} (b) : sum_assoc α β γ (inl (inr b)) = inr (inl b) := rfl
 @[simp] theorem sum_assoc_apply_in3 {α β γ} (c) : sum_assoc α β γ (inr c) = inr (inr c) := rfl
 
-@[simp] def sum_empty (α : Sort*) : α ⊕ empty ≃ α :=
+def sum_empty (α : Sort*) : α ⊕ empty ≃ α :=
 ⟨λ s, match s with inl a := a | inr e := empty.rec _ e end,
  inl,
  λ s, by { rcases s with _ | ⟨⟨⟩⟩, refl },
  λ a, rfl⟩
 
-@[simp] def empty_sum (α : Sort*) : empty ⊕ α ≃ α :=
+@[simp] lemma sum_empty_apply_inl {α} (a) : sum_empty α (sum.inl a) = a := rfl
+
+def empty_sum (α : Sort*) : empty ⊕ α ≃ α :=
 (sum_comm _ _).trans $ sum_empty _
 
-@[simp] def sum_pempty (α : Sort*) : α ⊕ pempty ≃ α :=
+@[simp] lemma empty_sum_apply_inr {α} (a) : empty_sum α (sum.inr a) = a := rfl
+
+def sum_pempty (α : Sort*) : α ⊕ pempty ≃ α :=
 ⟨λ s, match s with inl a := a | inr e := pempty.rec _ e end,
  inl,
  λ s, by { rcases s with _ | ⟨⟨⟩⟩, refl },
  λ a, rfl⟩
 
-@[simp] def pempty_sum (α : Sort*) : pempty ⊕ α ≃ α :=
+@[simp] lemma sum_pempty_apply_inl {α} (a) : sum_pempty α (sum.inl a) = a := rfl
+
+def pempty_sum (α : Sort*) : pempty ⊕ α ≃ α :=
 (sum_comm _ _).trans $ sum_pempty _
 
-@[simp] def option_equiv_sum_punit (α : Sort*) : option α ≃ α ⊕ punit.{u+1} :=
+@[simp] lemma pempty_sum_apply_inr {α} (a) : pempty_sum α (sum.inr a) = a := rfl
+
+def option_equiv_sum_punit (α : Sort*) : option α ≃ α ⊕ punit.{u+1} :=
 ⟨λ o, match o with none := inr punit.star | some a := inl a end,
  λ s, match s with inr _ := none | inl a := some a end,
  λ o, by cases o; refl,
  λ s, by rcases s with _ | ⟨⟨⟩⟩; refl⟩
 
+@[simp] lemma option_equiv_sum_punit_none {α} : option_equiv_sum_punit α none = sum.inr () := rfl
+@[simp] lemma option_equiv_sum_punit_some {α} (a) :
+  option_equiv_sum_punit α (some a) = sum.inl a := rfl
+
 /-- The set of `x : option α` such that `is_some x` is equivalent to `α`. -/
 def option_is_some_equiv (α : Type*) : {x : option α // x.is_some} ≃ α :=
 { to_fun := λ o, option.get o.2,
@@ -592,7 +608,7 @@ def nat_equiv_nat_sum_punit : ℕ ≃ ℕ ⊕ punit.{u+1} :=
  λ n, begin cases n, repeat { refl } end,
  λ s, begin cases s with a u, { refl }, {cases u, { refl }} end⟩
 
-@[simp] def nat_sum_punit_equiv_nat : ℕ ⊕ punit.{u+1} ≃ ℕ :=
+def nat_sum_punit_equiv_nat : ℕ ⊕ punit.{u+1} ≃ ℕ :=
 nat_equiv_nat_sum_punit.symm
 
 def int_equiv_nat_sum_nat : ℤ ≃ ℕ ⊕ ℕ :=

src/data/finsupp.lean

@@ -928,8 +928,8 @@ lemma sum_comap_domain {α₁ α₂ β γ : Type*} [has_zero β] [add_comm_monoi
   (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set) :
   (comap_domain f l hf.inj_on).sum (g ∘ f) = l.sum g :=
 begin
-  unfold sum,
-  simp only [comap_domain, comap_domain_apply, finset.sum_preimage f _ _ (λ (x : α₂), g x (l x))],
+  simp [sum],
+  simp [comap_domain, finset.sum_preimage f _ _ (λ (x : α₂), g x (l x))]
 end
 
 lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid γ]

src/data/finsupp/pointwise.lean

@@ -53,8 +53,8 @@ instance [semiring β] : semigroup (α →₀ β) :=
   mul_assoc := λ f g h, by { ext, simp only [mul_apply, mul_assoc], }, }
 
 instance [ring β] : distrib (α →₀ β) :=
-{ left_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, left_distrib], },
-  right_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, right_distrib], },
+{ left_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, left_distrib] {proj := ff} },
+  right_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, right_distrib] {proj := ff} },
   ..(infer_instance : semigroup (α →₀ β)),
   ..(infer_instance : add_comm_group (α →₀ β)) }
 

src/data/list/defs.lean

@@ -105,18 +105,6 @@ def take_while (p : α → Prop) [decidable_pred p] : list α → list α
 | []     := []
 | (a::l) := if p a then a :: take_while l else []
 
-/-- `after p xs` is the suffix of `xs` after the first element that satisfies
-  `p`, not including that element.
-
-  ```lean
-  after      (eq 1)       [0, 1, 2, 3] = [2, 3]
-  drop_while (not ∘ eq 1) [0, 1, 2, 3] = [1, 2, 3]
-  ```
--/
-def after (p : α → Prop) [decidable_pred p] : list α → list α
-| [] := []
-| (x :: xs) := if p x then xs else after xs
-
 /-- Fold a function `f` over the list from the left, returning the list
   of partial results.
 

src/data/list/sigma.lean

@@ -103,12 +103,12 @@ lemma mem_ext {l₀ l₁ : list (sigma β)}
   (nd₀ : l₀.nodup) (nd₁ : l₁.nodup)
   (h : ∀ x, x ∈ l₀ ↔ x ∈ l₁) : l₀ ~ l₁ :=
 begin
-  induction l₀ with x xs generalizing l₁; cases l₁ with x ys,
+  induction l₀ with x xs generalizing l₁; cases l₁ with y ys,
   { constructor },
   iterate 2
-  { specialize h x, simp at h,
+  { specialize h x <|> specialize h y, simp at h,
     cases h },
-  simp at nd₀ nd₁, rename x y, classical,
+  simp at nd₀ nd₁, classical,
   cases nd₀, cases nd₁,
   by_cases h' : x = y,
   { subst y, constructor, apply l₀_ih ‹ _ › ‹ nodup ys ›,