feat(analysis/normed_space/pi_Lp): use typeclass inference for 1 ≤ p (

#9922)

In `measure_theory.Lp`, the exponent `(p : ℝ≥0∞)` is an explicit hypothesis, and typeclass inference finds `[fact (1 ≤ p)]` silently (with the help of some pre-built `fact_one_le_two_ennreal` etc for specific use cases).

Currently, in `pi_Lp`, the fact that `(hp : 1 ≤ p)` must be provided explicitly.  I propose changing over to the `fact` system as used `measure_theory.Lp` -- I think it looks a bit prettier in typical use cases.

src/analysis/inner_product_space/pi_L2.lean

@@ -17,7 +17,7 @@ This is recorded in this file as an inner product space instance on `pi_Lp 2`.
 
 ## Main definitions
 
-- `euclidean_space 𝕜 n`: defined to be `pi_Lp 2 _ (n → 𝕜)` for any `fintype n`, i.e., the space
+- `euclidean_space 𝕜 n`: defined to be `pi_Lp 2 (n → 𝕜)` for any `fintype n`, i.e., the space
   from functions to `n` to `𝕜` with the `L²` norm. We register several instances on it (notably
   that it is a finite-dimensional inner product space).
 
@@ -34,6 +34,8 @@ This is recorded in this file as an inner product space instance on `pi_Lp 2`.
 open real set filter is_R_or_C
 open_locale big_operators uniformity topological_space nnreal ennreal complex_conjugate
 
+local attribute [instance] fact_one_le_two_real
+
 noncomputable theory
 
 variables {ι : Type*}
@@ -43,10 +45,10 @@ local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 /-
  If `ι` is a finite type and each space `f i`, `i : ι`, is an inner product space,
 then `Π i, f i` is an inner product space as well. Since `Π i, f i` is endowed with the sup norm,
-we use instead `pi_Lp 2 one_le_two f` for the product space, which is endowed with the `L^2` norm.
+we use instead `pi_Lp 2 f` for the product space, which is endowed with the `L^2` norm.
 -/
 instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
-  [Π i, inner_product_space 𝕜 (f i)] : inner_product_space 𝕜 (pi_Lp 2 one_le_two f) :=
+  [Π i, inner_product_space 𝕜 (f i)] : inner_product_space 𝕜 (pi_Lp 2 f) :=
 { inner := λ x y, ∑ i, inner (x i) (y i),
   norm_sq_eq_inner :=
   begin
@@ -80,12 +82,12 @@ instance pi_Lp.inner_product_space {ι : Type*} [fintype ι] (f : ι → Type*)
     by simp only [finset.mul_sum, inner_smul_left] }
 
 @[simp] lemma pi_Lp.inner_apply {ι : Type*} [fintype ι] {f : ι → Type*}
-  [Π i, inner_product_space 𝕜 (f i)] (x y : pi_Lp 2 one_le_two f) :
+  [Π i, inner_product_space 𝕜 (f i)] (x y : pi_Lp 2 f) :
   ⟪x, y⟫ = ∑ i, ⟪x i, y i⟫ :=
 rfl
 
 lemma pi_Lp.norm_eq_of_L2 {ι : Type*} [fintype ι] {f : ι → Type*}
-  [Π i, inner_product_space 𝕜 (f i)] (x : pi_Lp 2 one_le_two f) :
+  [Π i, inner_product_space 𝕜 (f i)] (x : pi_Lp 2 f) :
   ∥x∥ = sqrt (∑ (i : ι), ∥x i∥ ^ 2) :=
 by { rw [pi_Lp.norm_eq_of_nat 2]; simp [sqrt_eq_rpow] }
 
@@ -94,7 +96,7 @@ by { rw [pi_Lp.norm_eq_of_nat 2]; simp [sqrt_eq_rpow] }
 space use `euclidean_space 𝕜 (fin n)`. -/
 @[reducible, nolint unused_arguments]
 def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
-  (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), 𝕜)
+  (n : Type*) [fintype n] : Type* := pi_Lp 2 (λ (i : n), 𝕜)
 
 lemma euclidean_space.norm_eq {𝕜 : Type*} [is_R_or_C 𝕜] {n : Type*} [fintype n]
   (x : euclidean_space 𝕜 n) : ∥x∥ = real.sqrt (∑ (i : n), ∥x i∥ ^ 2) :=
@@ -119,7 +121,7 @@ from `E` to `pi_Lp 2` of the subspaces equipped with the `L2` inner product. -/
 def direct_sum.submodule_is_internal.isometry_L2_of_orthogonal_family
   [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.submodule_is_internal V)
   (hV' : orthogonal_family 𝕜 V) :
-  E ≃ₗᵢ[𝕜] pi_Lp 2 one_le_two (λ i, V i) :=
+  E ≃ₗᵢ[𝕜] pi_Lp 2 (λ i, V i) :=
 begin
   let e₁ := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ i, V i),
   let e₂ := linear_equiv.of_bijective _ hV.injective hV.surjective,

src/analysis/normed_space/pi_Lp.lean

@@ -18,10 +18,9 @@ We give instances of this construction for emetric spaces, metric spaces, normed
 spaces.
 
 To avoid conflicting instances, all these are defined on a copy of the original Pi type, named
-`pi_Lp p hp α`, where `hp : 1 ≤ p`. This assumption is included in the definition of the type
-to make sure that it is always available to typeclass inference to construct the instances.
+`pi_Lp p α`. The assumpion `[fact (1 ≤ p)]` is required for the metric and normed space instances.
 
-We ensure that the topology and uniform structure on `pi_Lp p hp α` are (defeq to) the product
+We ensure that the topology and uniform structure on `pi_Lp p α` are (defeq to) the product
 topology and product uniformity, to be able to use freely continuity statements for the coordinate
 functions, for instance.
 
@@ -58,29 +57,30 @@ variables {ι : Type*}
 /-- A copy of a Pi type, on which we will put the `L^p` distance. Since the Pi type itself is
 already endowed with the `L^∞` distance, we need the type synonym to avoid confusing typeclass
 resolution. Also, we let it depend on `p`, to get a whole family of type on which we can put
-different distances, and we provide the assumption `hp` in the definition, to make it available
-to typeclass resolution when it looks for a distance on `pi_Lp p hp α`. -/
+different distances. -/
 @[nolint unused_arguments]
-def pi_Lp {ι : Type*} (p : ℝ) (hp : 1 ≤ p) (α : ι → Type*) : Type* := Π (i : ι), α i
+def pi_Lp {ι : Type*} (p : ℝ) (α : ι → Type*) : Type* := Π (i : ι), α i
 
-instance {ι : Type*} (p : ℝ) (hp : 1 ≤ p) (α : ι → Type*) [∀ i, inhabited (α i)] :
-  inhabited (pi_Lp p hp α) :=
+instance {ι : Type*} (p : ℝ) (α : ι → Type*) [∀ i, inhabited (α i)] : inhabited (pi_Lp p α) :=
 ⟨λ i, default (α i)⟩
 
+lemma fact_one_le_one_real : fact ((1:ℝ) ≤ 1) := ⟨rfl.le⟩
+lemma fact_one_le_two_real : fact ((1:ℝ) ≤ 2) := ⟨one_le_two⟩
+
 namespace pi_Lp
 
-variables (p : ℝ) (hp : 1 ≤ p) (α : ι → Type*) (β : ι → Type*)
+variables (p : ℝ) [fact_one_le_p : fact (1 ≤ p)] (α : ι → Type*) (β : ι → Type*)
 
-/-- Canonical bijection between `pi_Lp p hp α` and the original Pi type. We introduce it to be able
+/-- Canonical bijection between `pi_Lp p α` and the original Pi type. We introduce it to be able
 to compare the `L^p` and `L^∞` distances through it. -/
-protected def equiv : pi_Lp p hp α ≃ Π (i : ι), α i :=
+protected def equiv : pi_Lp p α ≃ Π (i : ι), α i :=
 equiv.refl _
 
 section
 /-!
 ### The uniformity on finite `L^p` products is the product uniformity
 
-In this section, we put the `L^p` edistance on `pi_Lp p hp α`, and we check that the uniformity
+In this section, we put the `L^p` edistance on `pi_Lp p α`, and we check that the uniformity
 coming from this edistance coincides with the product uniformity, by showing that the canonical
 map to the Pi type (with the `L^∞` distance) is a uniform embedding, as it is both Lipschitz and
 antiLipschitz.
@@ -92,15 +92,16 @@ explaining why having definitionally the right uniformity is often important.
 -/
 
 variables [∀ i, emetric_space (α i)] [∀ i, pseudo_emetric_space (β i)] [fintype ι]
+include fact_one_le_p
 
-/-- Endowing the space `pi_Lp p hp β` with the `L^p` pseudoedistance. This definition is not
+/-- Endowing the space `pi_Lp p β` with the `L^p` pseudoedistance. This definition is not
 satisfactory, as it does not register the fact that the topology and the uniform structure coincide
 with the product one. Therefore, we do not register it as an instance. Using this as a temporary
 pseudoemetric space instance, we will show that the uniform structure is equal (but not defeq) to
 the product one, and then register an instance in which we replace the uniform structure by the
 product one using this pseudoemetric space and `pseudo_emetric_space.replace_uniformity`. -/
-def pseudo_emetric_aux : pseudo_emetric_space (pi_Lp p hp β) :=
-have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+def pseudo_emetric_aux : pseudo_emetric_space (pi_Lp p β) :=
+have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
 { edist          := λ f g, (∑ (i : ι), (edist (f i) (g i)) ^ p) ^ (1/p),
   edist_self     := λ f, by simp [edist, ennreal.zero_rpow_of_pos pos,
                                   ennreal.zero_rpow_of_pos (inv_pos.2 pos)],
@@ -111,34 +112,34 @@ have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
     begin
       apply ennreal.rpow_le_rpow _ (one_div_nonneg.2 $ le_of_lt pos),
       refine finset.sum_le_sum (λ i hi, _),
-      exact ennreal.rpow_le_rpow (edist_triangle _ _ _) (le_trans zero_le_one hp)
+      exact ennreal.rpow_le_rpow (edist_triangle _ _ _) (le_trans zero_le_one fact_one_le_p.out)
     end
     ... ≤
     (∑ (i : ι), edist (f i) (g i) ^ p) ^ (1 / p) + (∑ (i : ι), edist (g i) (h i) ^ p) ^ (1 / p) :
-      ennreal.Lp_add_le _ _ _ hp }
+      ennreal.Lp_add_le _ _ _ fact_one_le_p.out }
 
-/-- Endowing the space `pi_Lp p hp α` with the `L^p` edistance. This definition is not satisfactory,
+/-- Endowing the space `pi_Lp p α` with the `L^p` edistance. This definition is not satisfactory,
 as it does not register the fact that the topology and the uniform structure coincide with the
 product one. Therefore, we do not register it as an instance. Using this as a temporary emetric
-space instance, we will show that the uniform structure is equal (but not defeq) to the product one,
-and then register an instance in which we replace the uniform structure by the product one using
-this emetric space and `emetric_space.replace_uniformity`. -/
-def emetric_aux : emetric_space (pi_Lp p hp α) :=
+space instance, we will show that the uniform structure is equal (but not defeq) to the product
+one, and then register an instance in which we replace the uniform structure by the product one
+using this emetric space and `emetric_space.replace_uniformity`. -/
+def emetric_aux : emetric_space (pi_Lp p α) :=
 { eq_of_edist_eq_zero := λ f g hfg,
   begin
-    have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
-    letI h := pseudo_emetric_aux p hp α,
+    have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
+    letI h := pseudo_emetric_aux p α,
     have h : edist f g = (∑ (i : ι), (edist (f i) (g i)) ^ p) ^ (1/p) := rfl,
     simp [h, ennreal.rpow_eq_zero_iff, pos, asymm pos, finset.sum_eq_zero_iff_of_nonneg] at hfg,
     exact funext hfg
   end,
-  ..pseudo_emetric_aux p hp α }
+  ..pseudo_emetric_aux p α }
 
 local attribute [instance] pi_Lp.emetric_aux pi_Lp.pseudo_emetric_aux
 
-lemma lipschitz_with_equiv : lipschitz_with 1 (pi_Lp.equiv p hp β) :=
+lemma lipschitz_with_equiv : lipschitz_with 1 (pi_Lp.equiv p β) :=
 begin
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
   have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (ne_of_gt pos),
   assume x y,
   simp only [edist, forall_prop_of_true, one_mul, finset.mem_univ, finset.sup_le_iff,
@@ -155,23 +156,23 @@ begin
 end
 
 lemma antilipschitz_with_equiv :
-  antilipschitz_with ((fintype.card ι : ℝ≥0) ^ (1/p)) (pi_Lp.equiv p hp β) :=
+  antilipschitz_with ((fintype.card ι : ℝ≥0) ^ (1/p)) (pi_Lp.equiv p β) :=
 begin
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
   have nonneg : 0 ≤ 1 / p := one_div_nonneg.2 (le_of_lt pos),
   have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (ne_of_gt pos),
   assume x y,
   simp [edist, -one_div],
   calc (∑ (i : ι), edist (x i) (y i) ^ p) ^ (1 / p) ≤
-  (∑ (i : ι), edist (pi_Lp.equiv p hp β x) (pi_Lp.equiv p hp β y) ^ p) ^ (1 / p) :
+  (∑ (i : ι), edist (pi_Lp.equiv p β x) (pi_Lp.equiv p β y) ^ p) ^ (1 / p) :
   begin
     apply ennreal.rpow_le_rpow _ nonneg,
     apply finset.sum_le_sum (λ i hi, _),
     apply ennreal.rpow_le_rpow _ (le_of_lt pos),
     exact finset.le_sup (finset.mem_univ i)
   end
   ... = (((fintype.card ι : ℝ≥0)) ^ (1/p) : ℝ≥0) *
-    edist (pi_Lp.equiv p hp β x) (pi_Lp.equiv p hp β y) :
+    edist (pi_Lp.equiv p β x) (pi_Lp.equiv p β y) :
   begin
     simp only [nsmul_eq_mul, finset.card_univ, ennreal.rpow_one, finset.sum_const,
       ennreal.mul_rpow_of_nonneg _ _ nonneg, ←ennreal.rpow_mul, cancel],
@@ -182,13 +183,13 @@ begin
 end
 
 lemma aux_uniformity_eq :
-  𝓤 (pi_Lp p hp β) = @uniformity _ (Pi.uniform_space _) :=
+  𝓤 (pi_Lp p β) = @uniformity _ (Pi.uniform_space _) :=
 begin
-  have A : uniform_inducing (pi_Lp.equiv p hp β) :=
-    (antilipschitz_with_equiv p hp β).uniform_inducing
-    (lipschitz_with_equiv p hp β).uniform_continuous,
-  have : (λ (x : pi_Lp p hp β × pi_Lp p hp β),
-    ((pi_Lp.equiv p hp β) x.fst, (pi_Lp.equiv p hp β) x.snd)) = id,
+  have A : uniform_inducing (pi_Lp.equiv p β) :=
+    (antilipschitz_with_equiv p β).uniform_inducing
+    (lipschitz_with_equiv p β).uniform_continuous,
+  have : (λ (x : pi_Lp p β × pi_Lp p β),
+    ((pi_Lp.equiv p β) x.fst, (pi_Lp.equiv p β) x.snd)) = id,
     by ext i; refl,
   rw [← A.comap_uniformity, this, comap_id]
 end
@@ -197,33 +198,36 @@ end
 
 /-! ### Instances on finite `L^p` products -/
 
-instance uniform_space [∀ i, uniform_space (β i)] : uniform_space (pi_Lp p hp β) :=
+instance uniform_space [∀ i, uniform_space (β i)] : uniform_space (pi_Lp p β) :=
 Pi.uniform_space _
 
 variable [fintype ι]
+include fact_one_le_p
 
 /-- pseudoemetric space instance on the product of finitely many pseudoemetric spaces, using the
 `L^p` pseudoedistance, and having as uniformity the product uniformity. -/
-instance [∀ i, pseudo_emetric_space (β i)] : pseudo_emetric_space (pi_Lp p hp β) :=
-(pseudo_emetric_aux p hp β).replace_uniformity (aux_uniformity_eq p hp β).symm
+instance [∀ i, pseudo_emetric_space (β i)] : pseudo_emetric_space (pi_Lp p β) :=
+(pseudo_emetric_aux p β).replace_uniformity (aux_uniformity_eq p β).symm
 
 /-- emetric space instance on the product of finitely many emetric spaces, using the `L^p`
 edistance, and having as uniformity the product uniformity. -/
-instance [∀ i, emetric_space (α i)] : emetric_space (pi_Lp p hp α) :=
-(emetric_aux p hp α).replace_uniformity (aux_uniformity_eq p hp α).symm
+instance [∀ i, emetric_space (α i)] : emetric_space (pi_Lp p α) :=
+(emetric_aux p α).replace_uniformity (aux_uniformity_eq p α).symm
 
-protected lemma edist {p : ℝ} {hp : 1 ≤ p} {β : ι → Type*}
-  [∀ i, pseudo_emetric_space (β i)] (x y : pi_Lp p hp β) :
+omit fact_one_le_p
+protected lemma edist {p : ℝ} [fact (1 ≤ p)] {β : ι → Type*}
+  [∀ i, pseudo_emetric_space (β i)] (x y : pi_Lp p β) :
   edist x y = (∑ (i : ι), (edist (x i) (y i)) ^ p) ^ (1/p) := rfl
+include fact_one_le_p
 
 /-- pseudometric space instance on the product of finitely many psuedometric spaces, using the
 `L^p` distance, and having as uniformity the product uniformity. -/
-instance [∀ i, pseudo_metric_space (β i)] : pseudo_metric_space (pi_Lp p hp β) :=
+instance [∀ i, pseudo_metric_space (β i)] : pseudo_metric_space (pi_Lp p β) :=
 begin
   /- we construct the instance from the pseudo emetric space instance to avoid checking again that
   the uniformity is the same as the product uniformity, but we register nevertheless a nice formula
   for the distance -/
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
   refine pseudo_emetric_space.to_pseudo_metric_space_of_dist
     (λf g, (∑ (i : ι), (dist (f i) (g i)) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _),
   { simp [pi_Lp.edist, ennreal.rpow_eq_top_iff, asymm pos, pos,
@@ -236,12 +240,12 @@ end
 
 /-- metric space instance on the product of finitely many metric spaces, using the `L^p` distance,
 and having as uniformity the product uniformity. -/
-instance [∀ i, metric_space (α i)] : metric_space (pi_Lp p hp α) :=
+instance [∀ i, metric_space (α i)] : metric_space (pi_Lp p α) :=
 begin
   /- we construct the instance from the emetric space instance to avoid checking again that the
   uniformity is the same as the product uniformity, but we register nevertheless a nice formula
   for the distance -/
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
   refine emetric_space.to_metric_space_of_dist
     (λf g, (∑ (i : ι), (dist (f i) (g i)) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _),
   { simp [pi_Lp.edist, ennreal.rpow_eq_top_iff, asymm pos, pos,
@@ -252,39 +256,43 @@ begin
           ennreal.to_real_sum A, dist_edist] }
 end
 
-protected lemma dist {p : ℝ} {hp : 1 ≤ p} {β : ι → Type*}
-  [∀ i, pseudo_metric_space (β i)] (x y : pi_Lp p hp β) :
+omit fact_one_le_p
+protected lemma dist {p : ℝ} [fact (1 ≤ p)] {β : ι → Type*}
+  [∀ i, pseudo_metric_space (β i)] (x y : pi_Lp p β) :
   dist x y = (∑ (i : ι), (dist (x i) (y i)) ^ p) ^ (1/p) := rfl
+include fact_one_le_p
 
 /-- seminormed group instance on the product of finitely many normed groups, using the `L^p`
 norm. -/
-instance semi_normed_group [∀i, semi_normed_group (β i)] : semi_normed_group (pi_Lp p hp β) :=
+instance semi_normed_group [∀i, semi_normed_group (β i)] : semi_normed_group (pi_Lp p β) :=
 { norm := λf, (∑ (i : ι), norm (f i) ^ p) ^ (1/p),
   dist_eq := λ x y, by { simp [pi_Lp.dist, dist_eq_norm, sub_eq_add_neg] },
   .. pi.add_comm_group }
 
 /-- normed group instance on the product of finitely many normed groups, using the `L^p` norm. -/
-instance normed_group [∀i, normed_group (α i)] : normed_group (pi_Lp p hp α) :=
-{ ..pi_Lp.semi_normed_group p hp α }
+instance normed_group [∀i, normed_group (α i)] : normed_group (pi_Lp p α) :=
+{ ..pi_Lp.semi_normed_group p α }
 
-lemma norm_eq {p : ℝ} {hp : 1 ≤ p} {β : ι → Type*}
-  [∀i, semi_normed_group (β i)] (f : pi_Lp p hp β) :
+omit fact_one_le_p
+lemma norm_eq {p : ℝ} [fact (1 ≤ p)] {β : ι → Type*}
+  [∀i, semi_normed_group (β i)] (f : pi_Lp p β) :
   ∥f∥ = (∑ (i : ι), ∥f i∥ ^ p) ^ (1/p) := rfl
 
-lemma norm_eq_of_nat {p : ℝ} {hp : 1 ≤ p} {β : ι → Type*}
-  [∀i, semi_normed_group (β i)] (n : ℕ) (h : p = n) (f : pi_Lp p hp β) :
+lemma norm_eq_of_nat {p : ℝ} [fact (1 ≤ p)] {β : ι → Type*}
+  [∀i, semi_normed_group (β i)] (n : ℕ) (h : p = n) (f : pi_Lp p β) :
   ∥f∥ = (∑ (i : ι), ∥f i∥ ^ n) ^ (1/(n : ℝ)) :=
 by simp [norm_eq, h, real.sqrt_eq_rpow, ←real.rpow_nat_cast]
+include fact_one_le_p
 
 variables (𝕜 : Type*) [normed_field 𝕜]
 
 /-- The product of finitely many seminormed spaces is a seminormed space, with the `L^p` norm. -/
 instance semi_normed_space [∀i, semi_normed_group (β i)] [∀i, semi_normed_space 𝕜 (β i)] :
-  semi_normed_space 𝕜 (pi_Lp p hp β) :=
+  semi_normed_space 𝕜 (pi_Lp p β) :=
 { norm_smul_le :=
   begin
     assume c f,
-    have : p * (1 / p) = 1 := mul_div_cancel' 1 (ne_of_gt (lt_of_lt_of_le zero_lt_one hp)),
+    have : p * (1 / p) = 1 := mul_div_cancel' 1 (lt_of_lt_of_le zero_lt_one fact_one_le_p.out).ne',
     simp only [pi_Lp.norm_eq, norm_smul, mul_rpow, norm_nonneg, ←finset.mul_sum, pi.smul_apply],
     rw [mul_rpow (rpow_nonneg_of_nonneg (norm_nonneg _) _), ← rpow_mul (norm_nonneg _),
         this, rpow_one],
@@ -294,13 +302,13 @@ instance semi_normed_space [∀i, semi_normed_group (β i)] [∀i, semi_normed_s
 
 /-- The product of finitely many normed spaces is a normed space, with the `L^p` norm. -/
 instance normed_space [∀i, normed_group (α i)] [∀i, normed_space 𝕜 (α i)] :
-  normed_space 𝕜 (pi_Lp p hp α) :=
-{ ..pi_Lp.semi_normed_space p hp α 𝕜 }
+  normed_space 𝕜 (pi_Lp p α) :=
+{ ..pi_Lp.semi_normed_space p α 𝕜 }
 
 /- Register simplification lemmas for the applications of `pi_Lp` elements, as the usual lemmas
 for Pi types will not trigger. -/
-variables {𝕜 p hp α}
-[∀i, semi_normed_group (β i)] [∀i, semi_normed_space 𝕜 (β i)] (c : 𝕜) (x y : pi_Lp p hp β) (i : ι)
+variables {𝕜 p α}
+[∀i, semi_normed_group (β i)] [∀i, semi_normed_space 𝕜 (β i)] (c : 𝕜) (x y : pi_Lp p β) (i : ι)
 
 @[simp] lemma add_apply : (x + y) i = x i + y i := rfl
 @[simp] lemma sub_apply : (x - y) i = x i - y i := rfl

src/geometry/manifold/instances/real.lean

@@ -40,6 +40,7 @@ typeclass. We provide it as `[fact (x < y)]`.
 noncomputable theory
 open set function
 open_locale manifold
+local attribute [instance] fact_one_le_two_real
 
 /--
 The half-space in `ℝ^n`, used to model manifolds with boundary. We only define it when