[Merged by Bors] - chore(*): bump to lean 3.34.0

counterexamples/phillips.lean

@@ -163,7 +163,7 @@ instance : inhabited (bounded_additive_measure α) :=
   additive' := λ s t hst, by simp,
   exists_bound := ⟨0, λ s, by simp⟩ }⟩
 
-instance : has_coe_to_fun (bounded_additive_measure α) := ⟨_, λ f, f.to_fun⟩
+instance : has_coe_to_fun (bounded_additive_measure α) (λ _, set α → ℝ) := ⟨λ f, f.to_fun⟩
 
 namespace bounded_additive_measure
 

leanpkg.toml

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

src/algebra/algebra/basic.lean

@@ -431,7 +431,7 @@ section semiring
 variables [comm_semiring R] [semiring A] [semiring B] [semiring C] [semiring D]
 variables [algebra R A] [algebra R B] [algebra R C] [algebra R D]
 
-instance : has_coe_to_fun (A →ₐ[R] B) := ⟨_, λ f, f.to_fun⟩
+instance : has_coe_to_fun (A →ₐ[R] B) (λ _, A → B) := ⟨alg_hom.to_fun⟩
 
 initialize_simps_projections alg_hom (to_fun → apply)
 
@@ -462,6 +462,8 @@ variables (φ : A →ₐ[R] B)
 theorem coe_fn_injective : @function.injective (A →ₐ[R] B) (A → B) coe_fn :=
 by { intros φ₁ φ₂ H, cases φ₁, cases φ₂, congr, exact H }
 
+theorem coe_fn_inj {φ₁ φ₂ : A →ₐ[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂ := coe_fn_injective.eq_iff
+
 theorem coe_ring_hom_injective : function.injective (coe : (A →ₐ[R] B) → (A →+* B)) :=
 λ φ₁ φ₂ H, coe_fn_injective $ show ((φ₁ : (A →+* B)) : A → B) = ((φ₂ : (A →+* B)) : A → B),
   from congr_arg _ H
@@ -716,7 +718,7 @@ variables [comm_semiring R] [semiring A₁] [semiring A₂] [semiring A₃]
 variables [algebra R A₁] [algebra R A₂] [algebra R A₃]
 variables (e : A₁ ≃ₐ[R] A₂)
 
-instance : has_coe_to_fun (A₁ ≃ₐ[R] A₂) := ⟨_, alg_equiv.to_fun⟩
+instance : has_coe_to_fun (A₁ ≃ₐ[R] A₂) (λ _, A₁ → A₂) := ⟨alg_equiv.to_fun⟩
 
 @[ext]
 lemma ext {f g : A₁ ≃ₐ[R] A₂} (h : ∀ a, f a = g a) : f = g :=

src/algebra/category/Algebra/basic.lean

@@ -34,8 +34,7 @@ attribute [instance] Algebra.is_ring Algebra.is_algebra
 
 namespace Algebra
 
-instance : has_coe_to_sort (Algebra R) :=
-{ S := Type v, coe := Algebra.carrier }
+instance : has_coe_to_sort (Algebra R) (Type v) := ⟨Algebra.carrier⟩
 
 instance : category (Algebra.{v} R) :=
 { hom   := λ A B, A →ₐ[R] B,

src/algebra/category/CommRing/basic.lean

@@ -36,7 +36,9 @@ instance bundled_hom : bundled_hom assoc_ring_hom :=
  λ M N P [semiring M] [semiring N] [semiring P], by exactI @ring_hom.comp M N P _ _ _,
  λ M N [semiring M] [semiring N], by exactI @ring_hom.coe_inj M N _ _⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] SemiRing
+attribute [derive [large_category, concrete_category]] SemiRing
+
+instance : has_coe_to_sort SemiRing Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled SemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [semiring R] : SemiRing := bundled.of R
@@ -70,7 +72,7 @@ namespace Ring
 
 instance : bundled_hom.parent_projection @ring.to_semiring := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] Ring
+attribute [derive [(λ Ring, has_coe_to_sort Ring Type*), large_category, concrete_category]] Ring
 
 /-- Construct a bundled Ring from the underlying type and typeclass. -/
 def of (R : Type u) [ring R] : Ring := bundled.of R
@@ -100,7 +102,9 @@ namespace CommSemiRing
 
 instance : bundled_hom.parent_projection @comm_semiring.to_semiring := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommSemiRing
+attribute [derive [large_category, concrete_category]] CommSemiRing
+
+instance : has_coe_to_sort CommSemiRing Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
@@ -131,7 +135,9 @@ namespace CommRing
 
 instance : bundled_hom.parent_projection @comm_ring.to_ring := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommRing
+attribute [derive [large_category, concrete_category]] CommRing
+
+instance : has_coe_to_sort CommRing Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled CommRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_ring R] : CommRing := bundled.of R

src/algebra/category/FinVect.lean

@@ -31,7 +31,7 @@ universes u
 variables (K : Type u) [field K]
 
 /-- Define `FinVect` as the subtype of `Module.{u} K` of finite dimensional vector spaces. -/
-@[derive [category, has_coe_to_sort]]
+@[derive [category, λ α, has_coe_to_sort α (Sort*)]]
 def FinVect := { V : Module.{u} K // finite_dimensional K V }
 
 namespace FinVect
@@ -57,9 +57,8 @@ variables (V : FinVect K)
 def FinVect_dual : FinVect K :=
 ⟨Module.of K (module.dual K V), subspace.module.dual.finite_dimensional⟩
 
-instance : has_coe_to_fun (FinVect_dual K V) :=
-{ F := λ v, V → K,
-  coe := λ v, by { change V →ₗ[K] K at v, exact v, }, }
+instance : has_coe_to_fun (FinVect_dual K V) (λ _, V → K) :=
+{ coe := λ v, by { change V →ₗ[K] K at v, exact v, } }
 
 open category_theory.monoidal_category
 

src/algebra/category/Group/basic.lean

@@ -33,8 +33,10 @@ namespace Group
 @[to_additive]
 instance : bundled_hom.parent_projection group.to_monoid := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] Group
-attribute [to_additive] Group.has_coe_to_sort Group.large_category Group.concrete_category
+attribute [derive [large_category, concrete_category]] Group
+attribute [to_additive] Group.large_category Group.concrete_category
+
+@[to_additive] instance : has_coe_to_sort Group Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled `Group` from the underlying type and typeclass. -/
 @[to_additive] def of (X : Type u) [group X] : Group := bundled.of X
@@ -91,9 +93,11 @@ namespace CommGroup
 @[to_additive]
 instance : bundled_hom.parent_projection comm_group.to_group := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommGroup
-attribute [to_additive] CommGroup.has_coe_to_sort CommGroup.large_category
-  CommGroup.concrete_category
+attribute [derive [large_category, concrete_category]] CommGroup
+attribute [to_additive] CommGroup.large_category CommGroup.concrete_category
+
+@[to_additive] instance : has_coe_to_sort CommGroup Type* := bundled.has_coe_to_sort
+
 
 /-- Construct a bundled `CommGroup` from the underlying type and typeclass. -/
 @[to_additive] def of (G : Type u) [comm_group G] : CommGroup := bundled.of G

src/algebra/category/Module/adjunctions.lean

@@ -49,7 +49,7 @@ adjunction.mk_of_hom_equiv
 { hom_equiv := λ X M, (finsupp.lift M R X).to_equiv.symm,
   hom_equiv_naturality_left_symm' := λ _ _ M f g,
   finsupp.lhom_ext' (λ x, linear_map.ext_ring
-    (finsupp.sum_map_domain_index_add_monoid_hom (λ y, ((smul_add_hom R ↥M).flip) (g y))).symm) }
+    (finsupp.sum_map_domain_index_add_monoid_hom (λ y, ((smul_add_hom R M).flip) (g y))).symm) }
 
 instance : is_right_adjoint (forget (Module.{u} R)) := ⟨_, adj R⟩
 
@@ -59,61 +59,72 @@ namespace free
 variables [comm_ring R]
 local attribute [ext] tensor_product.ext
 
+/-- (Implementation detail) The unitor for `free R`. -/
+def ε : 𝟙_ (Module.{u} R) ⟶ (free R).obj (𝟙_ (Type u)) :=
+finsupp.lsingle punit.star
+
+/-- (Implementation detail) The tensorator for `free R`. -/
+def μ (α β : Type u) : (free R).obj α ⊗ (free R).obj β ⟶ (free R).obj (α ⊗ β) :=
+(finsupp_tensor_finsupp' R α β).to_linear_map
+
+lemma μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') :
+  ((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y') =
+    (μ R X X') ≫ (free R).map (f ⊗ g) :=
+begin
+  intros,
+  ext x x' ⟨y, y'⟩,
+  dsimp [μ],
+  simp_rw [finsupp.map_domain_single, finsupp_tensor_finsupp'_single_tmul_single, mul_one,
+    finsupp.map_domain_single, category_theory.tensor_apply],
+end
+
+lemma left_unitality (X : Type u) :
+  (λ_ ((free R).obj X)).hom =
+  (ε R ⊗ 𝟙 ((free R).obj X)) ≫ μ R (𝟙_ (Type u)) X ≫ map (free R).obj (λ_ X).hom :=
+begin
+  intros,
+  ext,
+  dsimp [ε, μ],
+  simp_rw [finsupp_tensor_finsupp'_single_tmul_single,
+    Module.monoidal_category.left_unitor_hom_apply, finsupp.smul_single', mul_one,
+    finsupp.map_domain_single, category_theory.left_unitor_hom_apply],
+end
+
+lemma right_unitality (X : Type u) :
+  (ρ_ ((free R).obj X)).hom =
+  (𝟙 ((free R).obj X) ⊗ ε R) ≫ μ R X (𝟙_ (Type u)) ≫ map (free R).obj (ρ_ X).hom :=
+begin
+  intros,
+  ext,
+  dsimp [ε, μ],
+  simp_rw [finsupp_tensor_finsupp'_single_tmul_single,
+    Module.monoidal_category.right_unitor_hom_apply, finsupp.smul_single', mul_one,
+    finsupp.map_domain_single, category_theory.right_unitor_hom_apply],
+end
+
+lemma associativity (X Y Z : Type u) :
+  (μ R X Y ⊗ 𝟙 ((free R).obj Z)) ≫ μ R (X ⊗ Y) Z ≫ map (free R).obj (α_ X Y Z).hom =
+  (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
+    (𝟙 ((free R).obj X) ⊗ μ R Y Z) ≫ μ R X (Y ⊗ Z) :=
+begin
+  intros,
+  ext,
+  dsimp [μ],
+  simp_rw [finsupp_tensor_finsupp'_single_tmul_single, finsupp.map_domain_single, mul_one,
+    category_theory.associator_hom_apply],
+end
+
 /-- The free R-module functor is lax monoidal. -/
 -- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
 instance : lax_monoidal.{u} (free R).obj :=
 { -- Send `R` to `punit →₀ R`
-  ε := finsupp.lsingle punit.star,
+  ε := ε R,
   -- Send `(α →₀ R) ⊗ (β →₀ R)` to `α × β →₀ R`
-  μ := λ α β, (finsupp_tensor_finsupp' R α β).to_linear_map,
-  μ_natural' := begin
-    intros,
-    ext x x' ⟨y, y'⟩,
-    -- This is rather tedious: it's a terminal simp, with no arguments,
-    -- but between the four of them it is too slow.
-    simp only [tensor_product.mk_apply, mul_one, tensor_apply, monoidal_category.hom_apply,
-      Module.free_map, Module.coe_comp, map_functorial_obj,
-      linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
-      function.comp_app,
-      finsupp.lmap_domain_apply, finsupp.map_domain_single,
-      finsupp_tensor_finsupp'_single_tmul_single, finsupp.lsingle_apply],
-  end,
-  left_unitality' := begin
-    intros,
-    ext,
-    simp only [tensor_product.mk_apply, mul_one,
-      Module.id_apply, Module.free_map, Module.coe_comp, map_functorial_obj,
-      Module.monoidal_category.hom_apply, left_unitor_hom_apply,
-      Module.monoidal_category.left_unitor_hom_apply,
-      linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
-      function.comp_app,
-      finsupp.lmap_domain_apply, finsupp.smul_single', finsupp.map_domain_single,
-      finsupp_tensor_finsupp'_single_tmul_single, finsupp.lsingle_apply],
-  end,
-  right_unitality' := begin
-    intros,
-    ext,
-    simp only [tensor_product.mk_apply, mul_one,
-      Module.id_apply, Module.free_map, Module.coe_comp, map_functorial_obj,
-      Module.monoidal_category.hom_apply, right_unitor_hom_apply,
-      Module.monoidal_category.right_unitor_hom_apply,
-      linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
-      function.comp_app,
-      finsupp.lmap_domain_apply, finsupp.smul_single', finsupp.map_domain_single,
-      finsupp_tensor_finsupp'_single_tmul_single, finsupp.lsingle_apply],
-  end,
-  associativity' := begin
-    intros,
-    ext,
-    simp only [tensor_product.mk_apply, mul_one,
-      Module.id_apply, Module.free_map, Module.coe_comp, map_functorial_obj,
-      Module.monoidal_category.hom_apply, associator_hom_apply,
-      Module.monoidal_category.associator_hom_apply,
-      linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
-      function.comp_app,
-      finsupp.lmap_domain_apply, finsupp.smul_single', finsupp.map_domain_single,
-      finsupp_tensor_finsupp'_single_tmul_single, finsupp.lsingle_apply],
-  end, }
+  μ := μ R,
+  μ_natural' := λ X Y X' Y' f g, μ_natural R f g,
+  left_unitality' := left_unitality R,
+  right_unitality' := right_unitality R,
+  associativity' := associativity R, }
 
 end free
 

src/algebra/category/Module/basic.lean

@@ -70,8 +70,7 @@ attribute [instance] Module.is_add_comm_group Module.is_module
 
 namespace Module
 
-instance : has_coe_to_sort (Module.{v} R) :=
-{ S := Type v, coe := Module.carrier }
+instance : has_coe_to_sort (Module.{v} R) (Type v) := ⟨Module.carrier⟩
 
 instance Module_category : category (Module.{v} R) :=
 { hom   := λ M N, M →ₗ[R] N,

src/algebra/category/Mon/basic.lean

@@ -45,8 +45,10 @@ instance bundled_hom : bundled_hom assoc_monoid_hom :=
  λ M N P [monoid M] [monoid N] [monoid P], by exactI @monoid_hom.comp M N P _ _ _,
  λ M N [monoid M] [monoid N], by exactI @monoid_hom.coe_inj M N _ _⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] Mon
-attribute [to_additive] Mon.has_coe_to_sort Mon.large_category Mon.concrete_category
+attribute [derive [large_category, concrete_category]] Mon
+attribute [to_additive] Mon.large_category Mon.concrete_category
+
+@[to_additive] instance : has_coe_to_sort Mon Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled `Mon` from the underlying type and typeclass. -/
 @[to_additive]
@@ -87,8 +89,10 @@ namespace CommMon
 @[to_additive]
 instance : bundled_hom.parent_projection comm_monoid.to_monoid := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommMon
-attribute [to_additive] CommMon.has_coe_to_sort CommMon.large_category CommMon.concrete_category
+attribute [derive [large_category, concrete_category]] CommMon
+attribute [to_additive] CommMon.large_category CommMon.concrete_category
+
+@[to_additive] instance : has_coe_to_sort CommMon Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled `CommMon` from the underlying type and typeclass. -/
 @[to_additive]

src/algebra/category/Semigroup/basic.lean

@@ -42,8 +42,10 @@ namespace Magma
 instance bundled_hom : bundled_hom @mul_hom :=
 ⟨@mul_hom.to_fun, @mul_hom.id, @mul_hom.comp, @mul_hom.coe_inj⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] Magma
-attribute [to_additive] Magma.has_coe_to_sort Magma.large_category Magma.concrete_category
+attribute [derive [large_category, concrete_category]] Magma
+attribute [to_additive] Magma.large_category Magma.concrete_category
+
+@[to_additive] instance : has_coe_to_sort Magma Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled `Magma` from the underlying type and typeclass. -/
 @[to_additive]
@@ -81,9 +83,10 @@ namespace Semigroup
 @[to_additive]
 instance : bundled_hom.parent_projection semigroup.to_has_mul := ⟨⟩
 
-attribute [derive [has_coe_to_sort, large_category, concrete_category]] Semigroup
-attribute [to_additive] Semigroup.has_coe_to_sort Semigroup.large_category
-  Semigroup.concrete_category
+attribute [derive [large_category, concrete_category]] Semigroup
+attribute [to_additive] Semigroup.large_category Semigroup.concrete_category
+
+@[to_additive] instance : has_coe_to_sort Semigroup Type* := bundled.has_coe_to_sort
 
 /-- Construct a bundled `Semigroup` from the underlying type and typeclass. -/
 @[to_additive]

src/algebra/direct_sum/basic.lean

@@ -31,9 +31,12 @@ variables (ι : Type v) [dec_ι : decidable_eq ι] (β : ι → Type w)
 /-- `direct_sum β` is the direct sum of a family of additive commutative monoids `β i`.
 
 Note: `open_locale direct_sum` will enable the notation `⨁ i, β i` for `direct_sum β`. -/
-@[derive [has_coe_to_fun, add_comm_monoid, inhabited]]
+@[derive [add_comm_monoid, inhabited]]
 def direct_sum [Π i, add_comm_monoid (β i)] : Type* := Π₀ i, β i
 
+instance [Π i, add_comm_monoid (β i)] : has_coe_to_fun (direct_sum ι β) (λ _, Π i : ι, β i) :=
+dfinsupp.has_coe_to_fun
+
 localized "notation `⨁` binders `, ` r:(scoped f, direct_sum _ f) := r" in direct_sum
 
 namespace direct_sum

src/algebra/group/hom.lean

@@ -147,17 +147,17 @@ lemma monoid_with_zero_hom.coe_eq_to_zero_hom
   (f : zero_hom M N) = f.to_zero_hom := rfl
 
 @[to_additive]
-instance {mM : has_one M} {mN : has_one N} : has_coe_to_fun (one_hom M N) :=
-⟨_, one_hom.to_fun⟩
+instance {mM : has_one M} {mN : has_one N} : has_coe_to_fun (one_hom M N) (λ _, M → N) :=
+⟨one_hom.to_fun⟩
 @[to_additive]
-instance {mM : has_mul M} {mN : has_mul N} : has_coe_to_fun (mul_hom M N) :=
-⟨_, mul_hom.to_fun⟩
+instance {mM : has_mul M} {mN : has_mul N} : has_coe_to_fun (mul_hom M N) (λ _, M → N) :=
+⟨mul_hom.to_fun⟩
 @[to_additive]
-instance {mM : mul_one_class M} {mN : mul_one_class N} : has_coe_to_fun (M →* N) :=
-⟨_, monoid_hom.to_fun⟩
+instance {mM : mul_one_class M} {mN : mul_one_class N} : has_coe_to_fun (M →* N) (λ _, M → N) :=
+⟨monoid_hom.to_fun⟩
 instance {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
-  has_coe_to_fun (monoid_with_zero_hom M N) :=
-⟨_, monoid_with_zero_hom.to_fun⟩
+  has_coe_to_fun (monoid_with_zero_hom M N) (λ _, M → N) :=
+⟨monoid_with_zero_hom.to_fun⟩
 
 -- these must come after the coe_to_fun definitions
 initialize_simps_projections zero_hom (to_fun → apply)
@@ -567,7 +567,7 @@ instance : monoid (monoid.End M) :=
 
 instance : inhabited (monoid.End M) := ⟨1⟩
 
-instance : has_coe_to_fun (monoid.End M) := ⟨_, monoid_hom.to_fun⟩
+instance : has_coe_to_fun (monoid.End M) (λ _, M → M) := ⟨monoid_hom.to_fun⟩
 
 end End
 
@@ -594,7 +594,7 @@ instance : monoid (add_monoid.End A) :=
 
 instance : inhabited (add_monoid.End A) := ⟨1⟩
 
-instance : has_coe_to_fun (add_monoid.End A) := ⟨_, add_monoid_hom.to_fun⟩
+instance : has_coe_to_fun (add_monoid.End A) (λ _, A → A) := ⟨add_monoid_hom.to_fun⟩
 
 end End