chore(*): update to 3.41.0c (#12591)

kmill · kmill · commit c0a51cf2de54 · 2022-03-11T23:40:59.000Z
diff --git a/leanpkg.toml b/leanpkg.toml
@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.40.0"
+lean_version = "leanprover-community/lean:3.41.0"
 path = "src"
 
 [dependencies]
diff --git a/src/algebra/monoid_algebra/to_direct_sum.lean b/src/algebra/monoid_algebra/to_direct_sum.lean
@@ -165,7 +165,7 @@ def add_monoid_algebra_equiv_direct_sum [decidable_eq ι] [semiring M] [Π m : M
 /-- The additive version of `add_monoid_algebra.to_add_monoid_algebra`. Note that this is
 `noncomputable` because `add_monoid_algebra.has_add` is noncomputable. -/
 @[simps {fully_applied := ff}]
-noncomputable def add_monoid_algebra_add_equiv_direct_sum
+def add_monoid_algebra_add_equiv_direct_sum
   [decidable_eq ι] [semiring M] [Π m : M, decidable (m ≠ 0)] :
   add_monoid_algebra M ι ≃+ (⨁ i : ι, M) :=
 { to_fun := add_monoid_algebra.to_direct_sum, inv_fun := direct_sum.to_add_monoid_algebra,
@@ -175,7 +175,7 @@ noncomputable def add_monoid_algebra_add_equiv_direct_sum
 /-- The ring version of `add_monoid_algebra.to_add_monoid_algebra`. Note that this is
 `noncomputable` because `add_monoid_algebra.has_add` is noncomputable. -/
 @[simps {fully_applied := ff}]
-noncomputable def add_monoid_algebra_ring_equiv_direct_sum
+def add_monoid_algebra_ring_equiv_direct_sum
   [decidable_eq ι] [add_monoid ι] [semiring M]
   [Π m : M, decidable (m ≠ 0)] :
   add_monoid_algebra M ι ≃+* ⨁ i : ι, M :=
@@ -186,7 +186,7 @@ noncomputable def add_monoid_algebra_ring_equiv_direct_sum
 /-- The algebra version of `add_monoid_algebra.to_add_monoid_algebra`. Note that this is
 `noncomputable` because `add_monoid_algebra.has_add` is noncomputable. -/
 @[simps {fully_applied := ff}]
-noncomputable def add_monoid_algebra_alg_equiv_direct_sum
+def add_monoid_algebra_alg_equiv_direct_sum
   [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
   [Π m : A, decidable (m ≠ 0)] :
   add_monoid_algebra A ι ≃ₐ[R] ⨁ i : ι, A :=
diff --git a/src/analysis/convex/cone.lean b/src/analysis/convex/cone.lean
@@ -589,7 +589,7 @@ open_locale real_inner_product_space
 
 /-- The dual cone is the cone consisting of all points `y` such that for
 all points `x` in a given set `0 ≤ ⟪ x, y ⟫`. -/
-noncomputable def set.inner_dual_cone (s : set H) : convex_cone ℝ H :=
+def set.inner_dual_cone (s : set H) : convex_cone ℝ H :=
 { carrier := { y | ∀ x ∈ s, 0 ≤ ⟪ x, y ⟫ },
   smul_mem' := λ c hc y hy x hx,
   begin
diff --git a/src/analysis/normed_space/continuous_affine_map.lean b/src/analysis/normed_space/continuous_affine_map.lean
@@ -185,7 +185,7 @@ normed_group.of_core _
     end,
   norm_neg := λ f, by simp [norm_def], }
 
-noncomputable instance : normed_space 𝕜 (V →A[𝕜] W) :=
+instance : normed_space 𝕜 (V →A[𝕜] W) :=
 { norm_smul_le := λ t f, by simp only [norm_def, smul_cont_linear, coe_smul, pi.smul_apply,
     norm_smul, ← mul_max_of_nonneg _ _ (norm_nonneg t)], }
 
@@ -215,7 +215,7 @@ variables (𝕜 V W)
 /-- The space of affine maps between two normed spaces is linearly isometric to the product of the
 codomain with the space of linear maps, by taking the value of the affine map at `(0 : V)` and the
 linear part. -/
-noncomputable def to_const_prod_continuous_linear_map : (V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W) :=
+def to_const_prod_continuous_linear_map : (V →A[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W) :=
 { to_fun    := λ f, ⟨f 0, f.cont_linear⟩,
   inv_fun   := λ p, p.2.to_continuous_affine_map + const 𝕜 V p.1,
   left_inv  := λ f, by { ext, rw f.decomp, simp, },
diff --git a/src/analysis/normed_space/linear_isometry.lean b/src/analysis/normed_space/linear_isometry.lean
@@ -556,7 +556,7 @@ variables {R}
 variables (R E E₂ E₃)
 
 /-- The natural equivalence `(E × E₂) × E₃ ≃ E × (E₂ × E₃)` is a linear isometry. -/
-noncomputable def prod_assoc [module R E₂] [module R E₃] : (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃ :=
+def prod_assoc [module R E₂] [module R E₃] : (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃ :=
 { to_fun    := equiv.prod_assoc E E₂ E₃,
   inv_fun   := (equiv.prod_assoc E E₂ E₃).symm,
   map_add'  := by simp,
diff --git a/src/control/lawful_fix.lean b/src/control/lawful_fix.lean
@@ -183,7 +183,7 @@ lemma to_unit_cont (f : part α →o part α) (hc : continuous f) : continuous (
   erw [hc, chain.map_comp], refl
 end
 
-noncomputable instance : lawful_fix (part α) :=
+instance : lawful_fix (part α) :=
 ⟨λ f hc, show part.fix (to_unit_mono f) () = _, by rw part.fix_eq (to_unit_cont f hc); refl⟩
 
 end part
@@ -192,7 +192,7 @@ open sigma
 
 namespace pi
 
-noncomputable instance {β} : lawful_fix (α → part β) := ⟨λ f, part.fix_eq⟩
+instance {β} : lawful_fix (α → part β) := ⟨λ f, part.fix_eq⟩
 
 variables {γ : Π a : α, β a → Type*}
 
diff --git a/src/data/complex/is_R_or_C.lean b/src/data/complex/is_R_or_C.lean
@@ -766,7 +766,7 @@ end cleanup_lemmas
 section linear_maps
 
 /-- The real part in a `is_R_or_C` field, as a linear map. -/
-noncomputable def re_lm : K →ₗ[ℝ] ℝ :=
+def re_lm : K →ₗ[ℝ] ℝ :=
 { map_smul' := smul_re,  .. re }
 
 @[simp, is_R_or_C_simps] lemma re_lm_coe : (re_lm : K → ℝ) = re := rfl
@@ -792,7 +792,7 @@ end
 @[continuity] lemma continuous_re : continuous (re : K → ℝ) := re_clm.continuous
 
 /-- The imaginary part in a `is_R_or_C` field, as a linear map. -/
-noncomputable def im_lm : K →ₗ[ℝ] ℝ :=
+def im_lm : K →ₗ[ℝ] ℝ :=
 { map_smul' := smul_im,  .. im }
 
 @[simp, is_R_or_C_simps] lemma im_lm_coe : (im_lm : K → ℝ) = im := rfl
@@ -810,7 +810,7 @@ linear_map.mk_continuous im_lm 1 $ by
 @[continuity] lemma continuous_im : continuous (im : K → ℝ) := im_clm.continuous
 
 /-- Conjugate as an `ℝ`-algebra equivalence -/
-noncomputable def conj_ae : K ≃ₐ[ℝ] K :=
+def conj_ae : K ≃ₐ[ℝ] K :=
 { inv_fun := conj,
   left_inv := conj_conj,
   right_inv := conj_conj,
diff --git a/src/data/finsupp/to_dfinsupp.lean b/src/data/finsupp/to_dfinsupp.lean
@@ -172,7 +172,7 @@ def finsupp_equiv_dfinsupp [decidable_eq ι] [has_zero M] [Π m : M, decidable (
 /-- The additive version of `finsupp.to_finsupp`. Note that this is `noncomputable` because
 `finsupp.has_add` is noncomputable. -/
 @[simps {fully_applied := ff}]
-noncomputable def finsupp_add_equiv_dfinsupp
+def finsupp_add_equiv_dfinsupp
   [decidable_eq ι] [add_zero_class M] [Π m : M, decidable (m ≠ 0)] :
   (ι →₀ M) ≃+ (Π₀ i : ι, M) :=
 { to_fun := finsupp.to_dfinsupp, inv_fun := dfinsupp.to_finsupp,
@@ -184,7 +184,7 @@ variables (R)
 /-- The additive version of `finsupp.to_finsupp`. Note that this is `noncomputable` because
 `finsupp.has_add` is noncomputable. -/
 @[simps {fully_applied := ff}]
-noncomputable def finsupp_lequiv_dfinsupp
+def finsupp_lequiv_dfinsupp
   [decidable_eq ι] [semiring R] [add_comm_monoid M] [Π m : M, decidable (m ≠ 0)] [module R M] :
   (ι →₀ M) ≃ₗ[R] (Π₀ i : ι, M) :=
 { to_fun := finsupp.to_dfinsupp, inv_fun := dfinsupp.to_finsupp,
diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean
@@ -271,7 +271,7 @@ lemma supr_ennreal {α : Type*} [complete_lattice α] {f : ℝ≥0∞ → α} :
 @[simp] lemma top_add : ∞ + a = ∞ := top_add _
 
 /-- Coercion `ℝ≥0 → ℝ≥0∞` as a `ring_hom`. -/
-noncomputable def of_nnreal_hom : ℝ≥0 →+* ℝ≥0∞ :=
+def of_nnreal_hom : ℝ≥0 →+* ℝ≥0∞ :=
 ⟨coe, coe_one, λ _ _, coe_mul, coe_zero, λ _ _, coe_add⟩
 
 @[simp] lemma coe_of_nnreal_hom : ⇑of_nnreal_hom = coe := rfl
diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean
@@ -297,8 +297,12 @@ def finite_spanning_sets_in.pi {C : Π i, set (set (α i))}
 begin
   haveI := λ i, (hμ i).sigma_finite,
   haveI := fintype.encodable ι,
+  refine ⟨λ n, pi univ (λ i, (hμ i).set ((decode (ι → ℕ) n).iget i)), λ n, _, λ n, _, _⟩;
+  -- TODO (kmill) If this let comes before the refine, while the noncomputability checker
+  -- correctly sees this definition is computable, the Lean VM fails to see the binding is
+  -- computationally irrelevant. The `noncomputable theory` doesn't help because all it does
+  -- is insert `noncomputable` for you when necessary.
   let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget,
-  refine ⟨λ n, pi univ (λ i, (hμ i).set (e n i)), λ n, _, λ n, _, _⟩,
   { refine mem_image_of_mem _ (λ i _, (hμ i).set_mem _) },
   { calc measure.pi μ (pi univ (λ i, (hμ i).set (e n i)))
         ≤ measure.pi μ (pi univ (λ i, to_measurable (μ i) ((hμ i).set (e n i)))) :
diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
@@ -39,15 +39,15 @@ open topological_space set filter metric
 open_locale ennreal pointwise topological_space
 
 /-- The interval `[0,1]` as a compact set with non-empty interior. -/
-noncomputable def topological_space.positive_compacts.Icc01 : positive_compacts ℝ :=
+def topological_space.positive_compacts.Icc01 : positive_compacts ℝ :=
 { carrier := Icc 0 1,
   compact' := is_compact_Icc,
   interior_nonempty' := by simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one] }
 
 universe u
 
 /-- The set `[0,1]^ι` as a compact set with non-empty interior. -/
-noncomputable def topological_space.positive_compacts.pi_Icc01 (ι : Type*) [fintype ι] :
+def topological_space.positive_compacts.pi_Icc01 (ι : Type*) [fintype ι] :
   positive_compacts (ι → ℝ) :=
 { carrier := pi univ (λ i, Icc 0 1),
   compact' := is_compact_univ_pi (λ i, is_compact_Icc),
diff --git a/src/model_theory/direct_limit.lean b/src/model_theory/direct_limit.lean
@@ -224,7 +224,7 @@ end
 variables (L ι)
 
 /-- The canonical map from a component to the direct limit. -/
-noncomputable def of (i : ι) : G i ↪[L] direct_limit G f :=
+def of (i : ι) : G i ↪[L] direct_limit G f :=
 { to_fun := quotient.mk ∘ sigma.mk i,
   inj' := λ x y h, begin
     simp only [quotient.eq] at h,
@@ -264,7 +264,7 @@ variables (L ι G f)
 /-- The universal property of the direct limit: maps from the components to another module
 that respect the directed system structure (i.e. make some diagram commute) give rise
 to a unique map out of the direct limit. -/
-noncomputable def lift : direct_limit G f ↪[L] P :=
+def lift : direct_limit G f ↪[L] P :=
 { to_fun := quotient.lift (λ (x : Σ i, G i), (g x.1) x.2) (λ x y xy, begin
     simp only,
     obtain ⟨i, hx, hy⟩ := directed_of (≤) x.1 y.1,
diff --git a/src/ring_theory/polynomial/homogeneous.lean b/src/ring_theory/polynomial/homogeneous.lean
@@ -44,7 +44,7 @@ def is_homogeneous [comm_semiring R] (φ : mv_polynomial σ R) (n : ℕ) :=
 variables (σ R)
 
 /-- The submodule of homogeneous `mv_polynomial`s of degree `n`. -/
-noncomputable def homogeneous_submodule [comm_semiring R] (n : ℕ) :
+def homogeneous_submodule [comm_semiring R] (n : ℕ) :
   submodule R (mv_polynomial σ R) :=
 { carrier := { x | x.is_homogeneous n },
   smul_mem' := λ r a ha c hc, begin
diff --git a/src/ring_theory/witt_vector/teichmuller.lean b/src/ring_theory/witt_vector/teichmuller.lean
@@ -92,7 +92,7 @@ end
 /-- The Teichmüller lift of an element of `R` to `𝕎 R`.
 The `0`-th coefficient of `teichmuller p r` is `r`, and all others are `0`.
 This is a monoid homomorphism. -/
-noncomputable def teichmuller : R →* 𝕎 R :=
+def teichmuller : R →* 𝕎 R :=
 { to_fun := teichmuller_fun p,
   map_one' :=
   begin
diff --git a/src/tactic/slim_check.lean b/src/tactic/slim_check.lean
@@ -227,6 +227,6 @@ set_option trace.class_instances true
     trace!"\n[testable instance]{format.indent inst 2}" },
   code ← eval_expr (io punit) e,
   unsafe_run_io code,
-  admit }
+  tactic.admit }
 
 end tactic.interactive
diff --git a/src/topology/category/Compactum.lean b/src/topology/category/Compactum.lean
@@ -424,7 +424,7 @@ def full : full Compactum_to_CompHaus.{u} :=
 lemma faithful : faithful Compactum_to_CompHaus := {}
 
 /-- This definition is used to prove essential surjectivity of Compactum_to_CompHaus. -/
-noncomputable def iso_of_topological_space {D : CompHaus} :
+def iso_of_topological_space {D : CompHaus} :
   Compactum_to_CompHaus.obj (Compactum.of_topological_space D) ≅ D :=
 { hom :=
   { to_fun := id,
