chore(*): update to lean 3.15.0 (#2851)

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals (`{ foo := 42 }`).  There are two points where we need to pay attention:

1. Avoid sourcing (`{ ..e }` where e.g. `e : euclidean_domain α`) for fields like `add`, `mul`, `zero`, etc.  Instead write `{ add := (+), mul := (*), zero := 0, ..e }`.  The reason is that `{ ..e }` is equivalent to `{ mul := euclidean_domain.mul, ..e }`.  And `euclidean_domain.mul` should never be mentioned.

I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14.  For now, my advice is: if you get weird errors like "cannot unify `a * b` and `?m_1 * ?m_2` in a structure literal, add `mul := (*)`.

2. `refine { le := (≤), .. }; simp` is slower.  This is because references to `(≤)` are no longer reduced to `le` in the subgoals.  If a subgoal like `a ≤ b → b ≤ a → a = b` was stated for preorders (because `partial_order` extends `preorder`), then the `(≤)` will contain a `preorder` subterm.  This subterm also contains other subgoals (proofs of reflexivity and transitivity).  Therefore the goals are larger than you might expect:

```
∀ (a b : α),
    @has_le.le.{u} α
      (@preorder.to_has_le.{u} α
         (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le)
            (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b))))
      a
      b →
    @has_le.le.{u} α
      (@preorder.to_has_le.{u} α
         (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le)
            (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b))))
      b
      a →
    @eq.{u+1} α a b
```

Advice: in cases such as this, try `refine { le := (≤), .. }; abstract { simp }` to reduce the size of the (dependent) subgoals.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk>

leanpkg.toml

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

src/algebra/category/CommRing/adjunctions.lean

@@ -46,6 +46,7 @@ The free-forgetful adjunction for commutative rings.
 def adj : free ⊣ forget CommRing :=
 adjunction.mk_of_hom_equiv
 { hom_equiv := λ X R, hom_equiv,
-  hom_equiv_naturality_left_symm' := by {intros, ext, dsimp, apply eval₂_cast_comp} }
+  hom_equiv_naturality_left_symm' :=
+    by intros; ext; apply eval₂_cast_comp f ⇑(int.cast_ring_hom ↥Y) g x }
 
 end CommRing

src/algebra/euclidean_domain.lean

@@ -255,9 +255,9 @@ rwa [xgcd_aux_val, xgcd_val] at this
 instance (α : Type*) [e : euclidean_domain α] : integral_domain α :=
 by haveI := classical.dec_eq α; exact
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
-    λ a b (h : a * b = 0), or_iff_not_and_not.2 $ λ h0 : a ≠ 0 ∧ b ≠ 0,
-      h0.1 $ by rw [← mul_div_cancel a h0.2, h, zero_div],
-  ..e }
+    λ a b h, (or_iff_not_and_not.2 $ λ h0,
+      h0.1 $ by rw [← mul_div_cancel a h0.2, h, zero_div]),
+  zero := 0, add := (+), mul := (*), ..e }
 
 end gcd
 

src/algebra/free.lean

@@ -225,7 +225,8 @@ instance : is_lawful_traversable free_magma.{u} :=
     (λ x, by simp only [traverse_pure] with functor_norm)
     (λ x y ih1 ih2, by simp only [traverse_mul] with functor_norm; rw [ih1, ih2]),
   traverse_eq_map_id := λ α β f x, free_magma.rec_on'' x (λ _, rfl)
-    (λ x y ih1 ih2, by rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]; refl) }
+    (λ x y ih1 ih2, by rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]; refl),
+  .. free_magma.is_lawful_monad }
 
 end category
 
@@ -541,7 +542,8 @@ instance : is_lawful_traversable free_semigroup.{u} :=
     (λ x, by simp only [traverse_pure] with functor_norm)
     (λ x y ih1 ih2, by resetI; simp only [traverse_mul] with functor_norm; rw [ih1, ih2]),
   traverse_eq_map_id := λ α β f x, free_semigroup.rec_on x (λ _, rfl)
-    (λ x y ih1 ih2, by rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]; refl) }
+    (λ x y ih1 ih2, by rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]; refl),
+  .. free_semigroup.is_lawful_monad }
 
 end category
 

src/category_theory/elements.lean

@@ -44,6 +44,19 @@ instance category_of_elements (F : C ⥤ Type w) : category F.elements :=
   id := λ p, ⟨𝟙 p.1, by obviously⟩,
   comp := λ p q r f g, ⟨f.val ≫ g.val, by obviously⟩ }
 
+namespace category_of_elements
+
+@[ext]
+lemma ext (F : C ⥤ Type w) {x y : F.elements} (f g : x ⟶ y) (w : f.val = g.val) : f = g :=
+subtype.eq' w
+
+@[simp] lemma comp_val {F : C ⥤ Type w} {p q r : F.elements} {f : p ⟶ q} {g : q ⟶ r} :
+  (f ≫ g).val = f.val ≫ g.val := rfl
+
+@[simp] lemma id_val {F : C ⥤ Type w} {p : F.elements} : (𝟙 p : p ⟶ p).val = 𝟙 p.1 := rfl
+
+end category_of_elements
+
 omit 𝒞 -- We'll assume C has a groupoid structure, so temporarily forget its category structure
 -- to avoid conflicts.
 instance groupoid_of_elements [groupoid C] (F : C ⥤ Type w) : groupoid F.elements :=

src/category_theory/endomorphism.lean

@@ -60,7 +60,7 @@ namespace Aut
 instance : group (Aut X) :=
 by refine { one := iso.refl X,
             inv := iso.symm,
-            mul := flip iso.trans, .. } ; dunfold flip; obviously
+            mul := flip iso.trans, .. } ; simp [flip, (*), has_one.one]
 
 /--
 Units in the monoid of endomorphisms of an object

src/category_theory/types.lean

@@ -119,7 +119,7 @@ def ulift_functor : Type u ⥤ Type (max u v) :=
 @[simp] lemma ulift_functor_map {X Y : Type u} (f : X ⟶ Y) (x : ulift.{v} X) :
   ulift_functor.map f x = ulift.up (f x.down) := rfl
 
-instance ulift_functor_full : full ulift_functor :=
+instance ulift_functor_full : full.{u} ulift_functor :=
 { preimage := λ X Y f x, (f (ulift.up x)).down }
 instance ulift_functor_faithful : faithful ulift_functor :=
 { injectivity' := λ X Y f g p, funext $ λ x,

src/control/applicative.lean

@@ -126,11 +126,11 @@ instance {α} [has_one α] [has_mul α] : applicative (const α) :=
   seq := λ β γ f x, (f * x : α) }
 
 instance {α} [monoid α] : is_lawful_applicative (const α) :=
-by refine { .. }; intros; simp [mul_assoc]
+by refine { .. }; intros; simp [mul_assoc, (<$>), (<*>), pure]
 
 instance {α} [has_zero α] [has_add α] : applicative (add_const α) :=
 { pure := λ β x, (0 : α),
   seq := λ β γ f x, (f + x : α) }
 
 instance {α} [add_monoid α] : is_lawful_applicative (add_const α) :=
-by refine { .. }; intros; simp [add_assoc]
+by refine { .. }; intros; simp [add_assoc, (<$>), (<*>), pure]

src/control/fold.lean

@@ -171,8 +171,8 @@ open function (hiding const) is_monoid_hom
 def map_fold [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] :
   applicative_transformation (const α) (const β) :=
 { app := λ x, f,
-  preserves_seq'  := by { intros, simp only [map_mul f], },
-  preserves_pure' := by { intros, simp only [map_one f] } }
+  preserves_seq'  := by { intros, simp only [map_mul f, (<*>)], },
+  preserves_pure' := by { intros, simp only [map_one f, pure] } }
 
 def free.mk : α → free_monoid α := list.ret
 

src/control/traversable/instances.lean

@@ -43,7 +43,8 @@ instance : is_lawful_traversable option :=
 { id_traverse := @option.id_traverse,
   comp_traverse := @option.comp_traverse,
   traverse_eq_map_id := @option.traverse_eq_map_id,
-  naturality := @option.naturality }
+  naturality := @option.naturality,
+  .. option.is_lawful_monad }
 
 namespace list
 
@@ -76,11 +77,12 @@ protected lemma naturality {α β} (f : α → F β) (x : list α) :
 by induction x; simp! * with functor_norm
 open nat
 
-instance : is_lawful_traversable list :=
+instance : is_lawful_traversable.{u} list :=
 { id_traverse := @list.id_traverse,
   comp_traverse := @list.comp_traverse,
   traverse_eq_map_id := @list.traverse_eq_map_id,
-  naturality := @list.naturality }
+  naturality := @list.naturality,
+  .. list.is_lawful_monad }
 end
 
 section traverse
@@ -160,6 +162,7 @@ instance {σ : Type u} : is_lawful_traversable.{u} (sum σ) :=
 { id_traverse := @sum.id_traverse σ,
   comp_traverse := @sum.comp_traverse σ,
   traverse_eq_map_id := @sum.traverse_eq_map_id σ,
-  naturality := @sum.naturality σ }
+  naturality := @sum.naturality σ,
+  .. sum.is_lawful_monad }
 
 end sum

src/data/erased.lean

@@ -2,27 +2,43 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
-
-A type for VM-erased data.
 -/
 import data.equiv.basic
 
+universes u
+
+/-!
+# A type for VM-erased data
+
+This file defines a type `erased α` which is classically isomorphic to `α`,
+but erased in the VM. That is, at runtime every value of `erased α` is
+represented as `0`, just like types and proofs.
+-/
+
 /-- `erased α` is the same as `α`, except that the elements
   of `erased α` are erased in the VM in the same way as types
   and proofs. This can be used to track data without storing it
   literally. -/
-def erased (α : Sort*) : Sort* :=
+def erased (α : Sort u) : Sort (max 1 u) :=
 Σ' s : α → Prop, ∃ a, (λ b, a = b) = s
 
 namespace erased
 
+/-- Erase a value. -/
 @[inline] def mk {α} (a : α) : erased α := ⟨λ b, a = b, a, rfl⟩
 
+/-- Extracts the erased value, noncomputably. -/
 noncomputable def out {α} : erased α → α
 | ⟨s, h⟩ := classical.some h
 
-@[reducible] def out_type (a : erased Sort*) : Sort* := out a
+/--
+Extracts the erased value, if it is a type.
+
+Note: `(mk a).out` is not definitionally equal to `a`.
+-/
+@[reducible] def out_type (a : erased (Sort u)) : Sort u := out a
 
+/-- Extracts the erased value, if it is a proof. -/
 theorem out_proof {p : Prop} (a : erased p) : p := out a
 
 @[simp] theorem out_mk {α} (a : α) : (mk a).out = a :=
@@ -35,34 +51,63 @@ end
 @[simp] theorem mk_out {α} : ∀ (a : erased α), mk (out a) = a
 | ⟨s, h⟩ := by simp [mk]; congr; exact classical.some_spec h
 
+@[ext] lemma out_inj {α} (a b : erased α) (h : a.out = b.out) : a = b :=
+by simpa using congr_arg mk h
+
+/-- Equivalence between `erased α` and `α`. -/
 noncomputable def equiv (α) : erased α ≃ α :=
 ⟨out, mk, mk_out, out_mk⟩
 
-instance (α : Type*) : has_repr (erased α) := ⟨λ _, "erased"⟩
+instance (α : Type u) : has_repr (erased α) := ⟨λ _, "erased"⟩
+instance (α : Type u) : has_to_string (erased α) := ⟨λ _, "erased"⟩
+meta instance (α : Type u) : has_to_format (erased α) := ⟨λ _, ("erased" : format)⟩
 
+/-- Computably produce an erased value from a proof of nonemptiness. -/
 def choice {α} (h : nonempty α) : erased α := mk (classical.choice h)
 
-theorem nonempty_iff {α} : nonempty (erased α) ↔ nonempty α :=
+@[simp] theorem nonempty_iff {α} : nonempty (erased α) ↔ nonempty α :=
 ⟨λ ⟨a⟩, ⟨a.out⟩, λ ⟨a⟩, ⟨mk a⟩⟩
 
-instance {α} [h : nonempty α] : nonempty (erased α) :=
-erased.nonempty_iff.2 h
+instance {α} [h : nonempty α] : inhabited (erased α) :=
+⟨choice h⟩
 
-instance {α} [h : inhabited α] : inhabited (erased α) :=
-⟨mk (default _)⟩
+/--
+`(>>=)` operation on `erased`.
 
+This is a separate definition because `α` and `β` can live in different
+universes (the universe is fixed in `monad`).
+-/
 def bind {α β} (a : erased α) (f : α → erased β) : erased β :=
 ⟨λ b, (f a.out).1 b, (f a.out).2⟩
 
 @[simp] theorem bind_eq_out {α β} (a f) : @bind α β a f = f a.out :=
 by delta bind bind._proof_1; cases f a.out; refl
 
+/--
+Collapses two levels of erasure.
+-/
 def join {α} (a : erased (erased α)) : erased α := bind a id
 
 @[simp] theorem join_eq_out {α} (a) : @join α a = a.out := bind_eq_out _ _
 
-instance : monad erased := { pure := @mk, bind := @bind }
+/--
+`(<$>)` operation on `erased`.
+
+This is a separate definition because `α` and `β` can live in different
+universes (the universe is fixed in `functor`).
+-/
+def map {α β} (f : α → β) (a : erased α) : erased β :=
+bind a (mk ∘ f)
+
+@[simp] theorem map_out {α β} {f : α → β} (a : erased α) : (a.map f).out = f a.out :=
+by simp [map]
+
+instance : monad erased := { pure := @mk, bind := @bind, map := @map }
+
+@[simp] lemma pure_def {α} : (pure : α → erased α) = @mk _ := rfl
+@[simp] lemma bind_def {α β} : ((>>=) : erased α → (α → erased β) → erased β) = @bind _ _ := rfl
+@[simp] lemma map_def {α β} : ((<$>) : (α → β) → erased α → erased β) = @map _ _ := rfl
 
-instance : is_lawful_monad erased := by refine {..}; intros; simp
+instance : is_lawful_monad erased := by refine {..}; intros; ext; simp
 
 end erased

src/data/list/defs.lean

@@ -172,15 +172,6 @@ def lookmap (f : α → option α) : list α → list α
   | none   := a :: lookmap l
   end
 
-def map_with_index_core (f : ℕ → α → β) : ℕ → list α → list β
-| k []      := []
-| k (a::as) := f k a::(map_with_index_core (k+1) as)
-
-/-- Given a function `f : ℕ → α → β` and `as : list α`, `as = [a₀, a₁, ...]`, returns the list
-`[f 0 a₀, f 1 a₁, ...]`. -/
-def map_with_index (f : ℕ → α → β) (as : list α) : list β :=
-map_with_index_core f 0 as
-
 /-- `indexes_of a l` is the list of all indexes of `a` in `l`.
 
      indexes_of a [a, b, a, a] = [0, 2, 3] -/

src/data/multiset.lean

@@ -3025,6 +3025,8 @@ namespace multiset
 instance : functor multiset :=
 { map := @map }
 
+@[simp] lemma fmap_def {α' β'} {s : multiset α'} (f : α' → β') : f <$> s = s.map f := rfl
+
 instance : is_lawful_functor multiset :=
 by refine { .. }; intros; simp
 
@@ -3058,10 +3060,12 @@ instance : monad multiset :=
   bind := @bind,
   .. multiset.functor }
 
+@[simp] lemma pure_def {α} : (pure : α → multiset α) = (λ x, x::0) := rfl
+@[simp] lemma bind_def {α β} : (>>=) = @bind α β := rfl
+
 instance : is_lawful_monad multiset :=
-{ bind_pure_comp_eq_map := λ α β f s, multiset.induction_on s rfl $ λ a s ih,
-    by rw [bind_cons, map_cons, bind_zero, add_zero],
-  pure_bind := λ α β x f, by simp only [cons_bind, zero_bind, add_zero],
+{ bind_pure_comp_eq_map := λ α β f s, multiset.induction_on s rfl $ λ a s ih, by simp,
+  pure_bind := λ α β x f, by simp,
   bind_assoc := @bind_assoc }
 
 open functor
@@ -3080,9 +3084,7 @@ by funext; simp [functor.map]
 
 lemma id_traverse {α : Type*} (x : multiset α) :
   traverse id.mk x = x :=
-quotient.induction_on x
-(by { intro, rw [traverse,quotient.lift_beta,function.comp],
-      simp, congr })
+quotient.induction_on x begin intro, simp [traverse], refl end
 
 lemma comp_traverse {G H : Type* → Type*}
                [applicative G] [applicative H]

src/data/padics/hensel.lean

@@ -88,7 +88,7 @@ parameters {p : ℕ} [fact p.prime] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
 include hnorm
 
 /-- `T` is an auxiliary value that is used to control the behavior of the polynomial `F`. -/
-private def T : ℝ := ∥(F.eval a).val / ((F.derivative.eval a).val)^2∥
+private def T : ℝ := ∥(F.eval a / (F.derivative.eval a)^2 : ℚ_[p])∥
 
 private lemma deriv_sq_norm_pos : 0 < ∥F.derivative.eval a∥ ^ 2 :=
 lt_of_le_of_lt (norm_nonneg _) hnorm
@@ -104,7 +104,7 @@ lt_of_le_of_ne (norm_nonneg _) (ne.symm deriv_norm_ne_zero)
 private lemma deriv_ne_zero : F.derivative.eval a ≠ 0 := mt norm_eq_zero.2 deriv_norm_ne_zero
 
 private lemma T_def : T = ∥F.eval a∥ / ∥F.derivative.eval a∥^2 :=
-calc T = ∥(F.eval a).val∥ / ∥((F.derivative.eval a).val)^2∥ : normed_field.norm_div _ _
+calc T = ∥F.eval a∥ / ∥((F.derivative.eval a)^2 : ℚ_[p])∥ : normed_field.norm_div _ _
    ... = ∥F.eval a∥ / ∥(F.derivative.eval a)^2∥ : by simp [norm, padic_norm_z]
    ... = ∥F.eval a∥ / ∥(F.derivative.eval a)∥^2 : by simp [pow, monoid.pow]
 
@@ -162,7 +162,7 @@ have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) :
 have F.derivative.eval z * (-z1) = -F.eval z, from calc
   F.derivative.eval z * (-z1)
     = (F.derivative.eval z) * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ : by rw [hzeq]
-... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp
+... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp [subtype.coe_ext]
 ... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) : subtype.ext.2 $ by simp
 ... = -(F.eval z) : by simp [mul_div_cancel' _ hdzne'],
 have heq : F.eval z' = q * z1^2, by simpa [this, hz'] using hq,
@@ -223,7 +223,7 @@ private lemma newton_seq_norm_le (n : ℕ) :
 
 private lemma newton_seq_norm_eq (n : ℕ) :
   ∥newton_seq (n+1) - newton_seq n∥ = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ :=
-by induction n; simp [sub_eq_add_neg, add_left_comm, add_assoc, newton_seq, newton_seq_aux, ih_n]
+by simp [newton_seq, newton_seq_aux, ih_n, sub_eq_add_neg, add_comm]
 
 private lemma newton_seq_succ_dist (n : ℕ) :
   ∥newton_seq (n+1) - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=