Update Lean and Mathlib to the port-complete tag

leanpkg.toml

@@ -1,8 +1,8 @@
 [package]
 name = "lftcm2020"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.50.3"
+lean_version = "leanprover-community/lean:3.51.1"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "9dba31df156d9d65b9d78db449542ca73d147c68"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "573eea921b01c49712ac02471911df0719297349"}

src/demos/category_theory.lean

@@ -4,14 +4,14 @@ import category_theory.functor.basic
 import algebra.category.Group.images
 import algebra.category.Group.colimits
 import algebra.category.Group.abelian
-import algebra.category.Module.monoidal
+import algebra.category.Module.monoidal.basic
 import algebra.category.Ring.basic
 
 import category_theory.abelian.basic
 import category_theory.limits.shapes.finite_limits
 
 import topology.instances.real
-import topology.category.Top.limits
+import topology.category.Top.limits.basic
 import topology.category.UniformSpace
 
 

src/exercises_sources/friday/analysis.lean

@@ -4,8 +4,11 @@ import analysis.normed_space.pi_Lp
 import analysis.calculus.iterated_deriv
 import analysis.calculus.mean_value
 import analysis.calculus.implicit
+import analysis.calculus.deriv.inv
+import analysis.special_functions.exp_deriv
 import measure_theory.integral.bochner
-import measure_theory.measure.lebesgue
+import measure_theory.measure.lebesgue.eq_haar
+import measure_theory.integral.set_integral
 import linear_algebra.matrix.trace
 
 

src/exercises_sources/friday/manifolds.lean

@@ -521,11 +521,11 @@ to use the library
 section you_should_probably_skip_this
 
 /- If `M` is a manifold modelled on a vector space `E`, then the underlying type for the tangent
-bundle is just `Σ (x : M), tangent_space x M` (i.e., the disjoint union of the tangent spaces,
+bundle is effectively `Σ (x : M), tangent_space x M` (i.e., the disjoint union of the tangent spaces,
 indexed by `x` -- this is a basic object in dependent type theory). And `tangent_space x M`
 is just (a copy of) `E` by definition. -/
 
-lemma tangent_bundle_myℝ_is_prod : tangent_bundle 𝓡1 myℝ = Σ (x : myℝ), ℝ :=
+lemma tangent_bundle_myℝ_is_prod : tangent_bundle 𝓡1 myℝ = bundle.total_space ℝ (λ x : myℝ, ℝ) :=
 sorry
 
 /- This means that you can specify a point in the tangent bundle as a pair `⟨x, v⟩`.

src/exercises_sources/thursday/linear_algebra.lean

@@ -166,7 +166,7 @@ Hints:
   `mul_self_nonneg` and `mul_self_eq_zero`.
 -/
 noncomputable instance : normed_add_comm_group (n → ℝ):=
-@inner_product_space.of_core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
+@inner_product_space.core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
 sorry
 
 noncomputable instance : inner_product_space ℝ (n → ℝ) :=

src/solutions/friday/manifolds.lean

@@ -590,11 +590,11 @@ to use the library
 section you_should_probably_skip_this
 
 /- If `M` is a manifold modelled on a vector space `E`, then the underlying type for the tangent
-bundle is just `Σ (x : M), tangent_space x M` (i.e., the disjoint union of the tangent spaces,
+bundle is effectively `Σ (x : M), tangent_space x M` (i.e., the disjoint union of the tangent spaces,
 indexed by `x` -- this is a basic object in dependent type theory). And `tangent_space x M`
 is just (a copy of) `E` by definition. -/
 
-lemma tangent_bundle_myℝ_is_prod : tangent_bundle 𝓡1 myℝ = Σ (x : myℝ), ℝ :=
+lemma tangent_bundle_myℝ_is_prod : tangent_bundle 𝓡1 myℝ = bundle.total_space ℝ (λ x : myℝ, ℝ) :=
 /- inline sorry -/rfl/- inline sorry -/
 
 /- This means that you can specify a point in the tangent bundle as a pair `⟨x, v⟩`.
@@ -1016,7 +1016,7 @@ begin
   { rcases x with ⟨x', h'⟩,
     simp at h',
     simp [h'] },
-  { have A : unique_mdiff_within_at 𝓡1 (Icc (0 : ℝ) 1) (⟨(x : ℝ), v⟩ : tangent_bundle 𝓡1 ℝ).fst,
+  { have A : unique_mdiff_within_at 𝓡1 (Icc (0 : ℝ) 1) (⟨(x : ℝ), v⟩ : tangent_bundle 𝓡1 ℝ).proj,
     { rw unique_mdiff_within_at_iff_unique_diff_within_at,
       apply unique_diff_on_Icc_zero_one _ x.2 },
     change (tangent_map (𝓡∂ 1) 𝓡1 g (tangent_map_within 𝓡1 (𝓡∂ 1) f (Icc 0 1) ⟨x, v⟩)).snd = v,

src/solutions/thursday/linear_algebra.lean

@@ -235,7 +235,7 @@ Hints:
   `mul_self_nonneg` and `mul_self_eq_zero`.
 -/
 noncomputable instance : normed_add_comm_group (n → ℝ):=
-@inner_product_space.of_core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
+@inner_product_space.core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
 -- sorry
 { inner := dot_product,
   nonneg_re := λ x, finset.sum_nonneg (λ i _, mul_self_nonneg _),