Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-15 21:05 1b85e3c2

View on Github →

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

https://github.com/leanprover-community/lean/pull/212 renames a bunch of tactic combinators. We change to using the new names.

Tactic case

https://github.com/leanprover-community/lean/pull/228 slightly changes the semantics of the case tactic. We fix the resulting breakage to be conform the new semantics.

Estimated changes

modified theorem equiv.apply_eq_iff_eq
modified theorem finset.card_eq_one
modified theorem finset.card_erase_le
modified theorem finset.card_erase_lt_of_mem
modified theorem finset.card_erase_of_mem
modified theorem finset.card_singleton
modified theorem finset.coe_singleton
modified theorem finset.fold_singleton
modified theorem finset.image_singleton
deleted theorem finset.inf_singleton'
modified theorem finset.inf_singleton
added theorem finset.infi_coe
modified theorem finset.map_singleton
deleted theorem finset.max_singleton'
modified theorem finset.max_singleton
modified theorem finset.mem_singleton
modified theorem finset.mem_singleton_self
deleted theorem finset.min_singleton'
modified theorem finset.min_singleton
modified theorem finset.ne_empty_of_mem
modified theorem finset.not_mem_singleton
modified theorem finset.powerset_empty
deleted def finset.singleton
modified theorem finset.singleton_bind
modified theorem finset.singleton_inj
modified theorem finset.singleton_ne_empty
modified theorem finset.singleton_val
deleted theorem finset.sup_singleton'
modified theorem finset.sup_singleton
added theorem finset.supr_coe
modified theorem infi_eq_infi_finset
modified theorem option.to_finset_some
modified theorem supr_eq_supr_finset
modified theorem fintype.univ_bool
modified theorem list.doubleton_eq
modified theorem list.singleton_eq
modified theorem set.singleton_def
modified theorem set.singleton_nonempty
deleted theorem Set.mem_singleton'
modified theorem Set.mem_singleton
modified theorem emetric.diam_insert