Commit 2020-05-31 17:05 7c7e8669

chore(*): update to lean 3.15.0 (#2851) The main effect for mathlib comes from https://github.com/leanprover-community/lean/pull/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. Zulip thread.