refactor(analysis/calculus/times_cont_diff): massive refactor

src/algebra/ordered_ring.lean

@@ -514,6 +514,13 @@ by rw [←coe_nat n]; apply coe_ne_top
 @[simp] lemma top_ne_nat (n : nat) : (⊤ : with_top α) ≠ n :=
 by rw [←coe_nat n]; apply top_ne_coe
 
+lemma add_one_le_of_lt {i n : with_top ℕ} (h : i < n) : i + 1 ≤ n :=
+begin
+  cases n, { exact lattice.le_top },
+  cases i, { exact (not_le_of_lt h lattice.le_top).elim },
+  exact with_top.coe_le_coe.2 (with_top.coe_lt_coe.1 h)
+end
+
 @[elab_as_eliminator]
 lemma nat_induction {P : with_top ℕ → Prop} (a : with_top ℕ)
   (h0 : P 0) (hsuc : ∀n:ℕ, P n → P n.succ) (htop : (∀n : ℕ, P n) → P ⊤) : P a :=

src/analysis/normed_space/bounded_linear_maps.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot, Johannes Hölzl
 Continuous linear functions -- functions between normed vector spaces which are bounded and linear.
 -/
 import algebra.field
-import analysis.normed_space.operator_norm
+import analysis.normed_space.operator_norm analysis.normed_space.multilinear
 
 noncomputable theory
 open_locale classical filter
@@ -104,12 +104,7 @@ lemma sub (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g
 lemma comp {g : F → G}
   (hg : is_bounded_linear_map 𝕜 g) (hf : is_bounded_linear_map 𝕜 f) :
   is_bounded_linear_map 𝕜 (g ∘ f) :=
-let ⟨hlg, Mg, hMgp, hMg⟩ := hg in
-let ⟨hlf, Mf, hMfp, hMf⟩ := hf in
-((hlg.mk' _).comp (hlf.mk' _)).is_linear.with_bound (Mg * Mf) $ assume x,
-  calc ∥g (f x)∥ ≤ Mg * ∥f x∥ : hMg _
-    ... ≤ Mg * (Mf * ∥x∥) : mul_le_mul_of_nonneg_left (hMf _) (le_of_lt hMgp)
-    ... = Mg * Mf * ∥x∥   : (mul_assoc _ _ _).symm
+(hg.to_continuous_linear_map.comp hf.to_continuous_linear_map).is_bounded_linear_map
 
 lemma tendsto (x : E) (hf : is_bounded_linear_map 𝕜 f) : f →_{x} (f x) :=
 let ⟨hf, M, hMp, hM⟩ := hf in
@@ -150,10 +145,11 @@ end is_bounded_linear_map
 
 section
 set_option class.instance_max_depth 240
+variables {ι : Type*} [decidable_eq ι] [fintype ι]
 
+/-- Taking the cartesian product of two continuous linear maps is a bounded linear operation. -/
 lemma is_bounded_linear_map_prod_iso :
-  is_bounded_linear_map 𝕜 (λ(p : (E →L[𝕜] F) × (E →L[𝕜] G)),
-                            (continuous_linear_map.prod p.1 p.2 : (E →L[𝕜] (F × G)))) :=
+  is_bounded_linear_map 𝕜 (λ(p : (E →L[𝕜] F) × (E →L[𝕜] G)), (p.1.prod p.2 : (E →L[𝕜] (F × G)))) :=
 begin
   refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ 1 (λp, _),
   simp only [norm, one_mul],
@@ -168,27 +164,42 @@ begin
       mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg _) }
 end
 
-lemma continuous_linear_map.is_bounded_linear_map_comp_left (g : continuous_linear_map 𝕜 F G) :
-  is_bounded_linear_map 𝕜 (λ(f : E →L[𝕜] F), continuous_linear_map.comp g f) :=
-begin
-  refine is_linear_map.with_bound ⟨λu v, _, λc u, _⟩
-    (∥g∥) (λu, continuous_linear_map.op_norm_comp_le _ _),
-  { ext x,
-    change g ((u+v) x) = g (u x) + g (v x),
-    have : (u+v) x = u x + v x := rfl,
-    rw [this, g.map_add] },
-  { ext x,
-    change g ((c • u) x) = c • g (u x),
-    have : (c • u) x = c • u x := rfl,
-    rw [this, continuous_linear_map.map_smul] }
-end
-
-lemma continuous_linear_map.is_bounded_linear_map_comp_right (f : continuous_linear_map 𝕜 E F) :
-  is_bounded_linear_map 𝕜 (λ(g : F →L[𝕜] G), continuous_linear_map.comp g f) :=
+/-- Taking the cartesian product of two continuous multilinear maps is a bounded linear operation. -/
+lemma is_bounded_linear_map_prod_multilinear
+  {E : ι → Type*} [∀i, normed_group (E i)] [∀i, normed_space 𝕜 (E i)] :
+  is_bounded_linear_map 𝕜
+  (λ p : (continuous_multilinear_map 𝕜 E F) × (continuous_multilinear_map 𝕜 E G), p.1.prod p.2) :=
+{ add := λ p₁ p₂, by { ext1 m, refl },
+  smul := λ c p, by { ext1 m, refl },
+  bound := ⟨1, zero_lt_one, λ p, begin
+    rw one_mul,
+    apply continuous_multilinear_map.op_norm_le_bound _ (norm_nonneg _) (λ m, _),
+    rw [continuous_multilinear_map.prod_apply, norm_prod_le_iff],
+    split,
+    { exact le_trans (p.1.le_op_norm m)
+        (mul_le_mul_of_nonneg_right (norm_fst_le p) (finset.prod_nonneg (λ i hi, norm_nonneg _))) },
+    { exact le_trans (p.2.le_op_norm m)
+        (mul_le_mul_of_nonneg_right (norm_snd_le p) (finset.prod_nonneg (λ i hi, norm_nonneg _))) },
+  end⟩ }
+
+/-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the
+continuous multilinear map `f (g m₁, ..., g mₙ)` is a bounded linear operation. -/
+lemma is_bounded_linear_map_continuous_multilinear_map_comp_linear (g : G →L[𝕜] E) :
+  is_bounded_linear_map 𝕜 (λ f : continuous_multilinear_map 𝕜 (λ (i : ι), E) F,
+    f.comp_continuous_linear_map 𝕜 E  g) :=
 begin
-  refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ (∥f∥) (λg, _),
-  rw mul_comm,
-  exact continuous_linear_map.op_norm_comp_le _ _
+  refine is_linear_map.with_bound ⟨λ f₁ f₂, by { ext m, refl }, λ c f, by { ext m, refl }⟩
+    (∥g∥ ^ (fintype.card ι)) (λ f, _),
+  apply continuous_multilinear_map.op_norm_le_bound _ _ (λ m, _),
+  { apply_rules [mul_nonneg', pow_nonneg, norm_nonneg, norm_nonneg] },
+  calc ∥f (g ∘ m)∥ ≤
+    ∥f∥ * finset.univ.prod (λ (i : ι), ∥g (m i)∥) : f.le_op_norm _
+    ... ≤ ∥f∥ * finset.univ.prod (λ (i : ι), ∥g∥ * ∥m i∥) : begin
+      apply mul_le_mul_of_nonneg_left _ (norm_nonneg _),
+      exact finset.prod_le_prod (λ i hi, norm_nonneg _) (λ i hi, g.le_op_norm _)
+    end
+    ... = ∥g∥ ^ fintype.card ι * ∥f∥ * finset.univ.prod (λ (i : ι), ∥m i∥) :
+      by { simp [finset.prod_mul_distrib, finset.card_univ], ring }
 end
 
 end
@@ -221,6 +232,34 @@ calc f (x, y - z) = f (x, y + (-1 : 𝕜) • z) : by simp
 ... = f (x, y) + (-1 : 𝕜) • f (x, z) : by simp only [h.add_right, h.smul_right]
 ... = f (x, y) - f (x, z) : by simp
 
+lemma is_bounded_bilinear_map.is_bounded_linear_map_left (h : is_bounded_bilinear_map 𝕜 f) (y : F) :
+  is_bounded_linear_map 𝕜 (λ x, f (x, y)) :=
+{ add   := λ x x', h.add_left _ _ _,
+  smul  := λ c x, h.smul_left _ _ _,
+  bound := begin
+    rcases h.bound with ⟨C, C_pos, hC⟩,
+    refine ⟨C * (∥y∥ + 1), mul_pos' C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ x, _⟩,
+    have : ∥y∥ ≤ ∥y∥ + 1, by simp [zero_le_one],
+    calc ∥f (x, y)∥ ≤ C * ∥x∥ * ∥y∥ : hC x y
+    ... ≤ C * ∥x∥ * (∥y∥ + 1) :
+      by apply_rules [norm_nonneg, mul_le_mul_of_nonneg_left, le_of_lt C_pos, mul_nonneg']
+    ... = C * (∥y∥ + 1) * ∥x∥ : by ring
+  end }
+
+lemma is_bounded_bilinear_map.is_bounded_linear_map_right (h : is_bounded_bilinear_map 𝕜 f) (x : E) :
+  is_bounded_linear_map 𝕜 (λ y, f (x, y)) :=
+{ add   := λ y y', h.add_right _ _ _,
+  smul  := λ c y, h.smul_right _ _ _,
+  bound := begin
+    rcases h.bound with ⟨C, C_pos, hC⟩,
+    refine ⟨C * (∥x∥ + 1), mul_pos' C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ y, _⟩,
+    have : ∥x∥ ≤ ∥x∥ + 1, by simp [zero_le_one],
+    calc ∥f (x, y)∥ ≤ C * ∥x∥ * ∥y∥ : hC x y
+    ... ≤ C * (∥x∥ + 1) * ∥y∥ :
+      by apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, mul_le_mul_of_nonneg_left,
+                      le_of_lt C_pos]
+  end }
+
 lemma is_bounded_bilinear_map_smul :
   is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × E), p.1 • p.2) :=
 { add_left   := add_smul,
@@ -252,6 +291,14 @@ lemma is_bounded_bilinear_map_comp :
       ≤ ∥y∥ * ∥x∥ : continuous_linear_map.op_norm_comp_le _ _
     ... = 1 * ∥x∥ * ∥ y∥ : by ring ⟩ }
 
+lemma continuous_linear_map.is_bounded_linear_map_comp_left (g : continuous_linear_map 𝕜 F G) :
+  is_bounded_linear_map 𝕜 (λ(f : E →L[𝕜] F), continuous_linear_map.comp g f) :=
+is_bounded_bilinear_map_comp.is_bounded_linear_map_left _
+
+lemma continuous_linear_map.is_bounded_linear_map_comp_right (f : continuous_linear_map 𝕜 E F) :
+  is_bounded_linear_map 𝕜 (λ(g : F →L[𝕜] G), continuous_linear_map.comp g f) :=
+is_bounded_bilinear_map_comp.is_bounded_linear_map_right _
+
 lemma is_bounded_bilinear_map_apply :
   is_bounded_bilinear_map 𝕜 (λp : (E →L[𝕜] F) × E, p.1 p.2) :=
 { add_left   := by simp,
@@ -272,6 +319,25 @@ lemma is_bounded_bilinear_map_smul_right :
   smul_right := λc m f, by { ext z, simp [smul_smul, mul_comm] },
   bound      := ⟨1, zero_lt_one, λm f, by simp⟩ }
 
+/-- The composition of a continuous linear map with a continuous multilinear map is a bounded
+bilinear operation. -/
+lemma is_bounded_bilinear_map_comp_multilinear {ι : Type*} {E : ι → Type*}
+[decidable_eq ι] [fintype ι] [∀i, normed_group (E i)] [∀i, normed_space 𝕜 (E i)] :
+  is_bounded_bilinear_map 𝕜 (λ p : (F →L[𝕜] G) × (continuous_multilinear_map 𝕜 E F),
+    p.1.comp_continuous_multilinear_map p.2) :=
+{ add_left   := λ g₁ g₂ f, by { ext m, refl },
+  smul_left  := λ c g f, by { ext m, refl },
+  add_right  := λ g f₁ f₂, by { ext m, simp },
+  smul_right := λ c g f, by { ext m, simp },
+  bound      := ⟨1, zero_lt_one, λ g f, begin
+    apply continuous_multilinear_map.op_norm_le_bound _ _ (λm, _),
+    { apply_rules [mul_nonneg, zero_le_one, norm_nonneg, norm_nonneg] },
+    calc ∥g (f m)∥ ≤ ∥g∥ * ∥f m∥ : g.le_op_norm _
+    ... ≤ ∥g∥ * (∥f∥ * finset.univ.prod (λ (i : ι), ∥m i∥)) :
+      mul_le_mul_of_nonneg_left (f.le_op_norm _) (norm_nonneg _)
+    ... = 1 * ∥g∥ * ∥f∥ * finset.univ.prod (λ (i : ι), ∥m i∥) : by ring
+    end⟩ }
+
 /-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
 `q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
 We define this function here a bounded linear map from `E × F` to `G`. The fact that this

src/analysis/normed_space/multilinear.lean

@@ -48,7 +48,7 @@ that we should deal with multilinear maps in several variables. The currying/unc
 constructions are based on those in `multilinear.lean`.
 
 From the mathematical point of view, all the results follow from the results on operator norm in
-one variable, by applying them to one variable after the other through curryfication. However, this
+one variable, by applying them to one variable after the other through currying. However, this
 is only well defined when there is an order on the variables (for instance on `fin n`) although
 the final result is independent of the order. While everything could be done following this
 approach, it turns out that direct proofs are easier and more efficient.
@@ -552,7 +552,7 @@ calc
   ∥f (snoc m x)∥ ≤ ∥f∥ * univ.prod (λ(i : fin n.succ), ∥snoc m x i∥) : f.le_op_norm _
   ... = ∥f∥ * univ.prod (λi, ∥m i∥) * ∥x∥ : by { rw prod_univ_cast_succ, simp [mul_assoc] }
 
-/-! #### Left curryfication -/
+/-! #### Left currying -/
 
 /-- Given a continuous linear map `f` from `E 0` to continuous multilinear maps on `n` variables,
 construct the corresponding continuous multilinear map on `n+1` variables obtained by concatenating
@@ -677,7 +677,7 @@ variables {𝕜 E E₂}
   (f : continuous_multilinear_map 𝕜 E E₂) (x : E 0) (v : Π (i : fin n), E i.succ) :
   (continuous_multilinear_curry_left_equiv 𝕜 E E₂).symm f x v = f (cons x v) := rfl
 
-/-! #### Right curryfication -/
+/-! #### Right currying -/
 
 /-- Given a continuous linear map `f` from continuous multilinear maps on `n` variables to
 continuous linear maps on `E 0`, construct the corresponding continuous multilinear map on `n+1`

src/geometry/manifold/basic_smooth_bundle.lean

@@ -90,10 +90,10 @@ base. We do not require the change of coordinates of the fibers to be linear, on
 Therefore, the fibers of the resulting bundle will not inherit a canonical vector space structure
 in general. -/
 structure basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-{E : Type u} [normed_group E] [normed_space 𝕜 E]
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
 {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
 (M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
-(F : Type u) [normed_group F] [normed_space 𝕜 F] :=
+(F : Type*) [normed_group F] [normed_space 𝕜 F] :=
 (coord_change      : atlas H M → atlas H M → H → F → F)
 (coord_change_self :
   ∀ i : atlas H M, ∀ x ∈ i.1.target, ∀ v, coord_change i i x v = v)
@@ -107,10 +107,10 @@ structure basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜
 namespace basic_smooth_bundle_core
 
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-{E : Type u} [normed_group E] [normed_space 𝕜 E]
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
 {H : Type*} [topological_space H] {I : model_with_corners 𝕜 E H}
 {M : Type*} [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
-{F : Type u} [normed_group F] [normed_space 𝕜 F]
+{F : Type*} [normed_group F] [normed_space 𝕜 F]
 (Z : basic_smooth_bundle_core I M F)
 
 /-- Fiber bundle core associated to a basic smooth bundle core -/
@@ -210,19 +210,14 @@ instance to_smooth_manifold :
   Z.to_topological_fiber_bundle_core.total_space :=
 begin
   /- We have to check that the charts belong to the smooth groupoid, i.e., they are smooth on their
-  source, and their inverses are smooth on the target. Since both objects are of the same type, it
+  source, and their inverses are smooth on the target. Since both objects are of the same kind, it
   suffices to prove the first statement in A below, and then glue back the pieces at the end. -/
   let J := model_with_corners.to_local_equiv (I.prod (model_with_corners_self 𝕜 F)),
   have A : ∀ (e e' : local_homeomorph M H) (he : e ∈ atlas H M) (he' : e' ∈ atlas H M),
     times_cont_diff_on 𝕜 ⊤
     (J.to_fun ∘ ((Z.chart he).symm.trans (Z.chart he')).to_fun ∘ J.inv_fun)
     (J.inv_fun ⁻¹' ((Z.chart he).symm.trans (Z.chart he')).source ∩ range J.to_fun),
   { assume e e' he he',
-    have U : unique_diff_on 𝕜
-             ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
-    { apply unique_diff_on.prod _ unique_diff_on_univ,
-      rw inter_comm,
-      exact I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
     have : J.inv_fun ⁻¹' ((chart Z he).symm.trans (chart Z he')).source ∩ range J.to_fun =
       (I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod univ,
     { have : range (λ (p : H × F), (I.to_fun (p.fst), id p.snd)) =
@@ -236,7 +231,7 @@ begin
       { exact λ⟨⟨hx1, hx2⟩, hx3⟩, ⟨⟨⟨hx1, e.map_target hx1⟩, hx2⟩, hx3⟩ } },
     rw this,
     -- check separately that the two components of the coordinate change are smooth
-    apply times_cont_diff_on.prod _ _ U,
+    apply times_cont_diff_on.prod,
     show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F), (I.to_fun ∘ e'.to_fun ∘ e.inv_fun ∘ I.inv_fun) p.1)
          ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
     { -- the coordinate change on the base is just a coordinate change for `M`, smooth since
@@ -247,8 +242,8 @@ begin
         (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) he he').1,
       have B : times_cont_diff_on 𝕜 ⊤ (λp : E × F, p.1)
         ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod univ) :=
-      times_cont_diff_fst.times_cont_diff_on U,
-      exact times_cont_diff_on.comp A B U (prod_subset_preimage_fst _ _) },
+      times_cont_diff_fst.times_cont_diff_on,
+      exact times_cont_diff_on.comp A B (prod_subset_preimage_fst _ _) },
     show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F),
       Z.coord_change ⟨chart_at H (e.inv_fun (I.inv_fun p.1)), _⟩ ⟨e', he'⟩
          ((chart_at H (e.inv_fun (I.inv_fun p.1))).to_fun (e.inv_fun (I.inv_fun p.1)))
@@ -261,7 +256,7 @@ begin
       cocycle as given in the definition of basic smooth bundles. -/
       have := Z.coord_change_smooth ⟨e, he⟩ ⟨e', he'⟩,
       rw model_with_corners.image at this,
-      apply times_cont_diff_on.congr this U,
+      apply times_cont_diff_on.congr this,
       rintros ⟨x, v⟩ hx,
       simp [local_equiv.trans_source] at hx,
       let f := chart_at H (e.inv_fun (I.inv_fun x)),
@@ -288,7 +283,7 @@ end basic_smooth_bundle_core
 section tangent_bundle
 
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-{E : Type u} [normed_group E] [normed_space 𝕜 E]
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
 {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
 (M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
 
@@ -328,7 +323,7 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
       symmetry,
       rw inter_comm,
       exact fderiv_within_inter N (I.unique_diff _ hx.2) },
-    apply times_cont_diff_on.congr C (unique_diff_on.prod B unique_diff_on_univ),
+    apply times_cont_diff_on.congr C,
     rintros ⟨x, v⟩ hx,
     have E : x ∈ I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun,
       by simpa using hx,

src/geometry/manifold/mfderiv.lean

@@ -996,8 +996,8 @@ begin
     (I.to_fun ∘ ((chart_at H x).symm.trans e).to_fun ∘ I.inv_fun)
     (I.inv_fun ⁻¹' ((chart_at H x).symm.trans e).source ∩ range I.to_fun) :=
     this.1,
-  have B := A.2 _ zero_one (I.to_fun ((chart_at H x).to_fun x)) mem,
-  simp only [local_homeomorph.trans_to_fun, iterated_fderiv_within_zero, local_homeomorph.symm_to_fun] at B,
+  have B := A.differentiable_on (by simp) (I.to_fun ((chart_at H x).to_fun x)) mem,
+  simp only [local_homeomorph.trans_to_fun, local_homeomorph.symm_to_fun] at B,
   rw [inter_comm, differentiable_within_at_inter
     (mem_nhds_sets (I.continuous_inv_fun _ (local_homeomorph.open_source _)) mem.1)] at B,
   simpa [written_in_ext_chart_at, ext_chart_at]
@@ -1022,11 +1022,11 @@ begin
     (I.to_fun ∘ (e.symm.trans (chart_at H (e.inv_fun x))).to_fun ∘ I.inv_fun)
     (I.inv_fun ⁻¹' (e.symm.trans (chart_at H (e.inv_fun x))).source ∩ range I.to_fun) :=
     this.1,
-  have B := A.2 _ zero_one (I.to_fun x) mem,
-  simp only [local_homeomorph.trans_to_fun, iterated_fderiv_within_zero, local_homeomorph.symm_to_fun] at B,
+  have B := A.differentiable_on (by simp) (I.to_fun x) mem,
+  simp only [local_homeomorph.trans_to_fun, local_homeomorph.symm_to_fun] at B,
   rw [inter_comm, differentiable_within_at_inter
     (mem_nhds_sets (I.continuous_inv_fun _ (local_homeomorph.open_source _)) mem.1)] at B,
-  simpa [written_in_ext_chart_at, ext_chart_at],
+  simpa [written_in_ext_chart_at, ext_chart_at]
 end
 
 lemma mdifferentiable_on_atlas_inv_fun (h : e ∈ atlas H M) :
@@ -1252,10 +1252,10 @@ end local_homeomorph.mdifferentiable
 section unique_mdiff
 
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-{E : Type u} [normed_group E] [normed_space 𝕜 E]
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
 {H : Type*} [topological_space H] {I : model_with_corners 𝕜 E H}
 {M : Type*} [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
-{E' : Type u} [normed_group E'] [normed_space 𝕜 E']
+{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
 {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
 {M' : Type*} [topological_space M'] [manifold H' M']
 {s : set M}
@@ -1375,7 +1375,7 @@ begin
   exact this.unique_diff_on _
 end
 
-variables {F : Type u} [normed_group F] [normed_space 𝕜 F]
+variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
 (Z : basic_smooth_bundle_core I M F)
 
 /-- In a smooth fiber bundle constructed from core, the preimage under the projection of a set with