chore(*): switch to lean 3.7.1c (#2106)

* fix(deprecated/group): remove dangerous instances

* Update Lean version to nightly.

* Remove composition instances for group homomorphisms.

* Remove dangerous is_submonoid instances.

* Flip instance arguments.

* Various Lean 3.7 fixes.

* Correctly use lemma.

* Use new elan 0.8.0 lean version name.

* Remove dangerous *.comp instances.

* Fix comp instance fallout.

* Fix more *.comp fallout

* Fix more *.comp fallout.

* More *.comp fallout.

* Fix *.comp fallout

* Fix *.comp fallout

* Port to has_attribute and copy_attribute changes.

* Fix monad_writer_adapter_trans instance.

* Revert 3.6 hacks.

* Update library note for *.comp morphisms.

* fix(scripts/deploy_docs.sh): use lean_version from mathlib leanpkg.toml

* Do not mention is_mul_hom.mul in library note.

* Update lean version to 3.7.0.

* Remove of_tactic'

* switch to 3.7.1c

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

leanpkg.toml

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

scripts/deploy_docs.sh

@@ -3,6 +3,8 @@ DEPLOY_NIGHTLY_GITHUB_USER=leanprover-community-bot
 set -e
 set -x
 
+lean_version="$(sed '/^lean_version/!d;s/.*"\(.*\)".*/\1/' leanpkg.toml)"
+
 git_hash="$(git log -1 --pretty=format:%h)"
 git clone https://github.com/leanprover-community/doc-gen.git
 cd doc-gen
@@ -17,8 +19,7 @@ rm -rf mathlib_docs/docs/
 # Force doc_gen project to match the Lean version used in CI.
 # If they are incompatible, something in doc_gen will fail to compile,
 # but this is better than trying to recompile all of mathlib.
-# short_lean_version is of the form 3.5.1 and set earlier in CI.
-elan override set "leanprover-community/lean:$short_lean_version"
+elan override set "$lean_version"
 
 python3 -m pip install --upgrade pip
 pip3 install markdown2 toml

src/algebra/direct_limit.lean

@@ -26,7 +26,7 @@ open lattice submodule
 
 variables {R : Type u} [ring R]
 variables {ι : Type v} [nonempty ι]
-variables [directed_order ι] [decidable_eq ι]
+variables [decidable_eq ι] [directed_order ι]
 variables (G : ι → Type w) [Π i, decidable_eq (G i)]
 
 /-- A directed system is a functor from the category (directed poset) to another category.
@@ -256,7 +256,8 @@ module.direct_limit.lift_of _ _ _
 @[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := is_add_group_hom.map_sub _ _ _
 
 lemma lift_unique (F : direct_limit G f → P) [is_add_group_hom F] (x) :
-  F x = lift G f P (λ i x, F $ of G f i x) (λ i j hij x, by rw of_f) x :=
+  F x = @lift _ _ _ _ G _ _ f _ _ P _ (λ i x, F $ of G f i x) (λ i, is_add_group_hom.comp _ _)
+    (λ i j hij x, by dsimp; rw of_f) x :=
 direct_limit.induction_on x $ λ i x, by rw lift_of
 
 end direct_limit
@@ -479,6 +480,7 @@ omit Hg
 @[simp] lemma lift_pow (x) (n : ℕ) : lift G f P g Hg (x ^ n) = lift G f P g Hg x ^ n :=
 (lift_hom G f P g Hg).map_pow x n
 
+local attribute [instance, priority 100] is_ring_hom.comp
 theorem lift_unique (F : direct_limit G f → P) [is_ring_hom F] (x) :
   F x = lift G f P (λ i x, F $ of G f i x) (λ i j hij x, by rw [of_f]) x :=
 direct_limit.induction_on x $ λ i x, by rw lift_of

src/algebra/direct_sum.lean

@@ -136,7 +136,9 @@ from dif_pos $ finset.mem_singleton_self i
 
 variables (ψ : direct_sum ι β → γ) [is_add_group_hom ψ]
 
-theorem to_group.unique (f : direct_sum ι β) : ψ f = to_group (λ i, ψ ∘ of β i) f :=
+theorem to_group.unique (f : direct_sum ι β) :
+  ψ f = @to_group _ _ _ _ _ _ (λ i, ψ ∘ of β i) (λ i, is_add_group_hom.comp (of β i) ψ) f :=
+by haveI : ∀ i, is_add_group_hom (ψ ∘ of β i) := (λ _, is_add_group_hom.comp _ _); exact
 direct_sum.induction_on f
   (by rw [is_add_group_hom.map_zero ψ, is_add_group_hom.map_zero (to_group (λ i, ψ ∘ of β i))])
   (λ i x, by rw [to_group_of])

src/algebra/euclidean_domain.lean

@@ -340,7 +340,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
     exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _) }
 
 @[priority 100] -- see Note [lower instance priority]
-instance field.to_euclidean_domain {K : Type u} [field K] [decidable_eq K] : euclidean_domain K :=
+instance field.to_euclidean_domain {K : Type u} [decidable_eq K] [field K] : euclidean_domain K :=
 { quotient := (/),
   remainder := λ a b, if b = 0 then a else 0,
   quotient_zero := div_zero,

src/algebra/ordered_group.lean

@@ -746,7 +746,6 @@ def to_decidable_linear_ordered_comm_group
   le_antisymm := @le_antisymm _ _,
   le_total := nonneg_total_iff.1 nonneg_total,
   decidable_le := by apply_instance,
-  decidable_eq := by apply_instance,
   decidable_lt := by apply_instance,
   ..@nonneg_comm_group.to_ordered_comm_group _ s }
 

src/algebra/ordered_ring.lean

@@ -346,7 +346,6 @@ def to_decidable_linear_ordered_comm_ring
   [comm : @is_commutative α (*)]
   : decidable_linear_ordered_comm_ring α :=
 { decidable_le := by apply_instance,
-  decidable_eq := by apply_instance,
   decidable_lt := by apply_instance,
   mul_comm := is_commutative.comm (*),
   ..@linear_nonneg_ring.to_linear_ordered_ring _ s }

src/algebra/ring.lean

@@ -155,8 +155,8 @@ variables (f : α → β) [is_semiring_hom f] {x y : α}
 instance id : is_semiring_hom (@id α) := by refine {..}; intros; refl
 
 /-- The composition of two semiring homomorphisms is a semiring homomorphism. -/
-@[priority 10] -- see Note [low priority instance on morphisms]
-instance comp {γ} [semiring γ] (g : β → γ) [is_semiring_hom g] :
+-- see Note [no instance on morphisms]
+lemma comp {γ} [semiring γ] (g : β → γ) [is_semiring_hom g] :
   is_semiring_hom (g ∘ f) :=
 { map_zero := by simp [map_zero f]; exact map_zero g,
   map_one := by simp [map_one f]; exact map_one g,
@@ -303,8 +303,8 @@ by simp [sub_eq_add_neg, map_add f, map_neg f]
 instance id : is_ring_hom (@id α) := by refine {..}; intros; refl
 
 /-- The composition of two ring homomorphisms is a ring homomorphism. -/
-@[priority 10] -- see Note [low priority instance on morphisms]
-instance comp {γ} [ring γ] (g : β → γ) [is_ring_hom g] :
+-- see Note [no instance on morphisms]
+lemma comp {γ} [ring γ] (g : β → γ) [is_ring_hom g] :
   is_ring_hom (g ∘ f) :=
 { map_add := λ x y, by simp [map_add f]; rw map_add g; refl,
   map_mul := λ x y, by simp [map_mul f]; rw map_mul g; refl,

src/analysis/normed_space/banach.lean

@@ -157,7 +157,7 @@ begin
     ... = 2 * C * ∥y∥ + 0 : by rw [add_zero, mul_assoc]
     ... ≤ 2 * C * ∥y∥ + ∥y∥ : add_le_add (le_refl _) (norm_nonneg _)
     ... = (2 * C + 1) * ∥y∥ : by ring,
-  have fsumeq : ∀n:ℕ, f((range n).sum u) = y - (h^[n]) y,
+  have fsumeq : ∀n:ℕ, f((finset.range n).sum u) = y - (h^[n]) y,
   { assume n,
     induction n with n IH,
     { simp [f.map_zero] },

src/analysis/normed_space/real_inner_product.lean

@@ -58,16 +58,6 @@ export has_inner (inner)
 
 section prio
 
-/-- A local instance providing a `has_sizeof (module α β)` instance, without
-initiating any typeclass search. -/
--- HACK: work around automatically generated module.has_sizeof instance
--- with [ring α] and [add_comm_group β] arguments
-protected def module.has_sizeof' {α β} {r : ring α} {g : add_comm_group β} :
-  has_sizeof (module α β) :=
-⟨λ _, 0⟩
-
-local attribute [instance] module.has_sizeof'
-
 set_option default_priority 100 -- see Note [default priority]
 -- see Note[vector space definition] for why we extend `module`.
 /--

src/category/monad/writer.lean

@@ -156,8 +156,8 @@ Currently that is not a problem, as there are almost no instances of `monad_func
 
 see Note [lower instance priority] -/
 @[nolint dangerous_instance, priority 100]
-instance monad_writer_adapter_trans {n n' : Type u → Type v} [monad_functor m m' n n']
-  [monad_writer_adapter ω ω' m m'] : monad_writer_adapter ω ω' n n' :=
+instance monad_writer_adapter_trans {n n' : Type u → Type v} [monad_writer_adapter ω ω' m m']
+  [monad_functor m m' n n'] : monad_writer_adapter ω ω' n n' :=
 ⟨λ α f, monad_map (λ α, (adapt_writer f : m α → m' α))⟩
 
 instance [monad m] : monad_writer_adapter ω ω' (writer_t ω m) (writer_t ω' m) :=

src/category_theory/limits/preserves.lean

@@ -76,9 +76,9 @@ instance preserves_colimits_of_shape_subsingleton (J : Type v) [small_category J
 by { split, intros, cases a, cases b, congr }
 
 instance preserves_limits_subsingleton (F : C ⥤ D) : subsingleton (preserves_limits F) :=
-by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsingleton.elim }
+by { split, intros, cases a, cases b, cc }
 instance preserves_colimits_subsingleton (F : C ⥤ D) : subsingleton (preserves_colimits F) :=
-by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsingleton.elim }
+by { split, intros, cases a, cases b, cc }
 
 omit 𝒟
 instance id_preserves_limits : preserves_limits (𝟭 C) :=
@@ -159,9 +159,9 @@ instance reflects_colimits_of_shape_subsingleton (J : Type v) [small_category J]
 by { split, intros, cases a, cases b, congr }
 
 instance reflects_limits_subsingleton (F : C ⥤ D) : subsingleton (reflects_limits F) :=
-by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsingleton.elim }
+by { split, intros, cases a, cases b, cc }
 instance reflects_colimits_subsingleton (F : C ⥤ D) : subsingleton (reflects_colimits F) :=
-by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsingleton.elim }
+by { split, intros, cases a, cases b, cc }
 
 @[priority 100] -- see Note [lower instance priority]
 instance reflects_limit_of_reflects_limits_of_shape (K : J ⥤ C) (F : C ⥤ D)

src/category_theory/monad/limits.lean

@@ -222,7 +222,7 @@ omit 𝒥
 
 section
 
-def has_limits_of_reflective (R : D ⥤ C) [reflective R] [has_limits.{v₁} C] : has_limits.{v₁} D :=
+def has_limits_of_reflective (R : D ⥤ C) [has_limits.{v₁} C] [reflective R] : has_limits.{v₁} D :=
 { has_limits_of_shape := λ J 𝒥, by exactI
   { has_limit := λ F, monadic_creates_limits F R } }
 

src/data/fintype.lean

@@ -49,37 +49,37 @@ open finset function
 
 namespace fintype
 
-instance decidable_pi_fintype {α} {β : α → Type*} [fintype α] [∀a, decidable_eq (β a)] :
+instance decidable_pi_fintype {α} {β : α → Type*} [∀a, decidable_eq (β a)] [fintype α] :
   decidable_eq (Πa, β a) :=
 assume f g, decidable_of_iff (∀ a ∈ fintype.elems α, f a = g a)
   (by simp [function.funext_iff, fintype.complete])
 
-instance decidable_forall_fintype [fintype α] {p : α → Prop} [decidable_pred p] :
+instance decidable_forall_fintype {p : α → Prop} [decidable_pred p] [fintype α] :
   decidable (∀ a, p a) :=
 decidable_of_iff (∀ a ∈ @univ α _, p a) (by simp)
 
-instance decidable_exists_fintype [fintype α] {p : α → Prop} [decidable_pred p] :
+instance decidable_exists_fintype {p : α → Prop} [decidable_pred p] [fintype α] :
   decidable (∃ a, p a) :=
 decidable_of_iff (∃ a ∈ @univ α _, p a) (by simp)
 
-instance decidable_eq_equiv_fintype [fintype α] [decidable_eq β] :
+instance decidable_eq_equiv_fintype [decidable_eq β] [fintype α] :
   decidable_eq (α ≃ β) :=
 λ a b, decidable_of_iff (a.1 = b.1) ⟨λ h, equiv.ext _ _ (congr_fun h), congr_arg _⟩
 
-instance decidable_injective_fintype [fintype α] [decidable_eq α] [decidable_eq β] :
+instance decidable_injective_fintype [decidable_eq α] [decidable_eq β] [fintype α] :
   decidable_pred (injective : (α → β) → Prop) := λ x, by unfold injective; apply_instance
 
-instance decidable_surjective_fintype [fintype α] [fintype β] [decidable_eq β] :
+instance decidable_surjective_fintype [decidable_eq β] [fintype α] [fintype β] :
   decidable_pred (surjective : (α → β) → Prop) := λ x, by unfold surjective; apply_instance
 
-instance decidable_bijective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :
+instance decidable_bijective_fintype [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
   decidable_pred (bijective : (α → β) → Prop) := λ x, by unfold bijective; apply_instance
 
-instance decidable_left_inverse_fintype [fintype α] [decidable_eq α] (f : α → β) (g : β → α) :
+instance decidable_left_inverse_fintype [decidable_eq α] [fintype α] (f : α → β) (g : β → α) :
   decidable (function.right_inverse f g) :=
 show decidable (∀ x, g (f x) = x), by apply_instance
 
-instance decidable_right_inverse_fintype [fintype β] [decidable_eq β] (f : α → β) (g : β → α) :
+instance decidable_right_inverse_fintype [decidable_eq β] [fintype β] (f : α → β) (g : β → α) :
   decidable (function.left_inverse f g) :=
 show decidable (∀ x, f (g x) = x), by apply_instance
 
@@ -466,7 +466,7 @@ fintype.subtype (univ.filter (∈ s)) (by simp)
 
 /-- A dependent product of fintypes, indexed by a fintype, is a fintype. -/
 instance pi.fintype {α : Type*} {β : α → Type*}
-  [fintype α] [decidable_eq α] [∀a, fintype (β a)] : fintype (Πa, β a) :=
+  [decidable_eq α] [fintype α] [∀a, fintype (β a)] : fintype (Πa, β a) :=
 @fintype.of_equiv _ _
   ⟨univ.pi $ λa:α, @univ (β a) _,
     λ f, finset.mem_pi.2 $ λ a ha, mem_univ _⟩
@@ -530,7 +530,7 @@ fintype.of_surjective quotient.mk (λ x, quotient.induction_on x (λ x, ⟨x, rf
 instance finset.fintype [fintype α] : fintype (finset α) :=
 ⟨univ.powerset, λ x, finset.mem_powerset.2 (finset.subset_univ _)⟩
 
-instance subtype.fintype [fintype α] (p : α → Prop) [decidable_pred p] : fintype {x // p x} :=
+instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
 set_fintype _
 
 theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] :
@@ -546,20 +546,20 @@ instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fi
   fintype (Σ' a, β a) :=
 fintype.of_equiv _ (equiv.psigma_equiv_sigma _).symm
 
-instance psigma.fintype_prop_left {α : Prop} {β : α → Type*} [∀ a, fintype (β a)] [decidable α] :
+instance psigma.fintype_prop_left {α : Prop} {β : α → Type*} [decidable α] [∀ a, fintype (β a)] :
   fintype (Σ' a, β a) :=
 if h : α then fintype.of_equiv (β h) ⟨λ x, ⟨h, x⟩, psigma.snd, λ _, rfl, λ ⟨_, _⟩, rfl⟩
 else ⟨∅, λ x, h x.1⟩
 
-instance psigma.fintype_prop_right {α : Type*} {β : α → Prop} [fintype α] [∀ a, decidable (β a)] :
+instance psigma.fintype_prop_right {α : Type*} {β : α → Prop} [∀ a, decidable (β a)] [fintype α] :
   fintype (Σ' a, β a) :=
 fintype.of_equiv {a // β a} ⟨λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, rfl, λ ⟨x, y⟩, rfl⟩
 
 instance psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [∀ a, decidable (β a)] :
   fintype (Σ' a, β a) :=
 if h : ∃ a, β a then ⟨{⟨h.fst, h.snd⟩}, λ ⟨_, _⟩, by simp⟩ else ⟨∅, λ ⟨x, y⟩, h ⟨x, y⟩⟩
 
-instance set.fintype [fintype α] [decidable_eq α] : fintype (set α) :=
+instance set.fintype [decidable_eq α] [fintype α] : fintype (set α) :=
 pi.fintype
 
 instance pfun_fintype (p : Prop) [decidable p] (α : p → Type*)

src/data/mv_polynomial.lean

@@ -418,13 +418,16 @@ instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f g) :=
   map_mul := λ p q, eval₂_mul _ _ }
 end
 
+section
+local attribute [instance, priority 10] is_semiring_hom.comp
 lemma eval₂_comp_left {γ} [comm_semiring γ]
   (k : β → γ) [is_semiring_hom k]
   (f : α → β) [is_semiring_hom f] (g : σ → β)
   (p) : k (eval₂ f g p) = eval₂ (k ∘ f) (k ∘ g) p :=
 by apply mv_polynomial.induction_on p; simp [
   eval₂_add, is_semiring_hom.map_add k,
   eval₂_mul, is_semiring_hom.map_mul k] {contextual := tt}
+end
 
 @[simp] lemma eval₂_eta (p : mv_polynomial σ α) : eval₂ C X p = p :=
 by apply mv_polynomial.induction_on p;
@@ -502,6 +505,10 @@ def map : mv_polynomial σ α → mv_polynomial σ β := eval₂ (C ∘ f) X
 
 variables [is_semiring_hom f]
 
+instance is_semiring_hom_C_f :
+  is_semiring_hom ((C : β → mv_polynomial σ β) ∘ f) :=
+is_semiring_hom.comp _ _
+
 @[simp] theorem map_monomial (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
 (eval₂_monomial _ _).trans monomial_eq.symm
 
@@ -861,7 +868,7 @@ lemma eval₂_sub : (p - q).eval₂ f g = p.eval₂ f g - q.eval₂ f g := is_ri
 @[simp] lemma eval₂_neg : (-p).eval₂ f g = -(p.eval₂ f g) := is_ring_hom.map_neg _
 
 lemma hom_C (f : mv_polynomial σ ℤ → β) [is_ring_hom f] (n : ℤ) : f (C n) = (n : β) :=
-congr_fun (int.eq_cast' (f ∘ C)) n
+congr_fun (@int.eq_cast' _ _ (f ∘ C) (is_ring_hom.comp _ _)) n
 
 /-- A ring homomorphism f : Z[X_1, X_2, ...] → R
 is determined by the evaluations f(X_1), f(X_2), ... -/
@@ -900,6 +907,9 @@ section map
 variables [comm_ring β]
 variables (f : α → β) [is_ring_hom f]
 
+instance is_ring_hom_C_f : is_ring_hom ((C : β → mv_polynomial σ β) ∘ f) :=
+is_ring_hom.comp _ _
+
 instance map.is_ring_hom : is_ring_hom (map f : mv_polynomial σ α → mv_polynomial σ β) :=
 eval₂.is_ring_hom _ _
 

src/data/polynomial.lean

@@ -10,6 +10,8 @@ import data.finsupp algebra.gcd_domain ring_theory.euclidean_domain tactic.ring_
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
+local attribute [instance, priority 10] is_semiring_hom.comp is_ring_hom.comp
+
 /-- `polynomial α` is the type of univariate polynomials over `α`.
 
 Polynomials should be seen as (semi-)rings with the additional constructor `X`.
@@ -559,6 +561,9 @@ def map : polynomial α → polynomial β := eval₂ (C ∘ f) X
 
 variables [is_semiring_hom f]
 
+instance is_semiring_hom_C_f : is_semiring_hom (C ∘ f) :=
+is_semiring_hom.comp _ _
+
 @[simp] lemma map_C : (C a).map f = C (f a) := eval₂_C _ _
 
 @[simp] lemma map_X : X.map f = X := eval₂_X _ _