bump to nightly-2023-05-18-10

mathlib commit leanprover-community/mathlib@c89fe2d

Mathbin/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

@@ -32,18 +32,26 @@ noncomputable section
 
 open CategoryTheory
 
+#print FundamentalGroup /-
 /-- The fundamental group is the automorphism group (vertex group) of the basepoint
 in the fundamental groupoid. -/
 def FundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) :=
   @Aut (FundamentalGroupoid X) _ x deriving Group, Inhabited
 #align fundamental_group FundamentalGroup
+-/
 
 namespace FundamentalGroup
 
 attribute [local instance] Path.Homotopic.setoid
 
 attribute [local reducible] FundamentalGroupoid
 
+/- warning: fundamental_group.fundamental_group_mul_equiv_of_path -> FundamentalGroup.fundamentalGroupMulEquivOfPath is a dubious translation:
+lean 3 declaration is
+  forall {X : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} X] {x₀ : X} {x₁ : X}, (Path.{u1} X _inst_1 x₀ x₁) -> (MulEquiv.{u1, u1} (FundamentalGroup.{u1} X _inst_1 x₀) (FundamentalGroup.{u1} X _inst_1 x₁) (MulOneClass.toHasMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (FundamentalGroup.group.{u1} X _inst_1 x₀))))) (MulOneClass.toHasMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (FundamentalGroup.group.{u1} X _inst_1 x₁))))))
+but is expected to have type
+  forall {X : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} X] {x₀ : X} {x₁ : X}, (Path.{u1} X _inst_1 x₀ x₁) -> (MulEquiv.{u1, u1} (FundamentalGroup.{u1} X _inst_1 x₀) (FundamentalGroup.{u1} X _inst_1 x₁) (MulOneClass.toMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (instGroupFundamentalGroup.{u1} X _inst_1 x₀))))) (MulOneClass.toMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (instGroupFundamentalGroup.{u1} X _inst_1 x₁))))))
+Case conversion may be inaccurate. Consider using '#align fundamental_group.fundamental_group_mul_equiv_of_path FundamentalGroup.fundamentalGroupMulEquivOfPathₓ'. -/
 /-- Get an isomorphism between the fundamental groups at two points given a path -/
 def fundamentalGroupMulEquivOfPath (p : Path x₀ x₁) :
     FundamentalGroup X x₀ ≃* FundamentalGroup X x₁ :=
@@ -52,31 +60,45 @@ def fundamentalGroupMulEquivOfPath (p : Path x₀ x₁) :
 
 variable (x₀ x₁)
 
+/- warning: fundamental_group.fundamental_group_mul_equiv_of_path_connected -> FundamentalGroup.fundamentalGroupMulEquivOfPathConnected is a dubious translation:
+lean 3 declaration is
+  forall {X : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} X] (x₀ : X) (x₁ : X) [_inst_3 : PathConnectedSpace.{u1} X _inst_1], MulEquiv.{u1, u1} (FundamentalGroup.{u1} X _inst_1 x₀) (FundamentalGroup.{u1} X _inst_1 x₁) (MulOneClass.toHasMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (FundamentalGroup.group.{u1} X _inst_1 x₀))))) (MulOneClass.toHasMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (FundamentalGroup.group.{u1} X _inst_1 x₁)))))
+but is expected to have type
+  forall {X : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} X] (x₀ : X) (x₁ : X) [_inst_3 : PathConnectedSpace.{u1} X _inst_1], MulEquiv.{u1, u1} (FundamentalGroup.{u1} X _inst_1 x₀) (FundamentalGroup.{u1} X _inst_1 x₁) (MulOneClass.toMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₀) (instGroupFundamentalGroup.{u1} X _inst_1 x₀))))) (MulOneClass.toMul.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Monoid.toMulOneClass.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (DivInvMonoid.toMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (Group.toDivInvMonoid.{u1} (FundamentalGroup.{u1} X _inst_1 x₁) (instGroupFundamentalGroup.{u1} X _inst_1 x₁)))))
+Case conversion may be inaccurate. Consider using '#align fundamental_group.fundamental_group_mul_equiv_of_path_connected FundamentalGroup.fundamentalGroupMulEquivOfPathConnectedₓ'. -/
 /-- The fundamental group of a path connected space is independent of the choice of basepoint. -/
 def fundamentalGroupMulEquivOfPathConnected [PathConnectedSpace X] :
     FundamentalGroup X x₀ ≃* FundamentalGroup X x₁ :=
   fundamentalGroupMulEquivOfPath (PathConnectedSpace.somePath x₀ x₁)
 #align fundamental_group.fundamental_group_mul_equiv_of_path_connected FundamentalGroup.fundamentalGroupMulEquivOfPathConnected
 
+#print FundamentalGroup.toArrow /-
 /-- An element of the fundamental group as an arrow in the fundamental groupoid. -/
 abbrev toArrow {X : TopCat} {x : X} (p : FundamentalGroup X x) : x ⟶ x :=
   p.Hom
 #align fundamental_group.to_arrow FundamentalGroup.toArrow
+-/
 
+#print FundamentalGroup.toPath /-
 /-- An element of the fundamental group as a quotient of homotopic paths. -/
 abbrev toPath {X : TopCat} {x : X} (p : FundamentalGroup X x) : Path.Homotopic.Quotient x x :=
   toArrow p
 #align fundamental_group.to_path FundamentalGroup.toPath
+-/
 
+#print FundamentalGroup.fromArrow /-
 /-- An element of the fundamental group, constructed from an arrow in the fundamental groupoid. -/
 abbrev fromArrow {X : TopCat} {x : X} (p : x ⟶ x) : FundamentalGroup X x :=
   ⟨p, CategoryTheory.Groupoid.inv p⟩
 #align fundamental_group.from_arrow FundamentalGroup.fromArrow
+-/
 
+#print FundamentalGroup.fromPath /-
 /-- An element of the fundamental gorup, constructed from a quotient of homotopic paths. -/
 abbrev fromPath {X : TopCat} {x : X} (p : Path.Homotopic.Quotient x x) : FundamentalGroup X x :=
   fromArrow p
 #align fundamental_group.from_path FundamentalGroup.fromPath
+-/
 
 end FundamentalGroup
 

Mathbin/AlgebraicTopology/FundamentalGroupoid/Punit.lean

@@ -39,6 +39,12 @@ instance {x y : FundamentalGroupoid PUnit} : Subsingleton (x ⟶ y) :=
   · congr <;> apply PUnit.eq_punit
   apply Quotient.subsingleton
 
+/- warning: fundamental_groupoid.punit_equiv_discrete_punit -> FundamentalGroupoid.punitEquivDiscretePunit is a dubious translation:
+lean 3 declaration is
+  CategoryTheory.Equivalence.{u1, u2, u1, u2} (FundamentalGroupoid.{u1} PUnit.{succ u1}) (CategoryTheory.Groupoid.toCategory.{u1, u1} (FundamentalGroupoid.{u1} PUnit.{succ u1}) (FundamentalGroupoid.CategoryTheory.groupoid.{u1} PUnit.{succ u1} PUnit.topologicalSpace.{u1})) (CategoryTheory.Discrete.{u2} PUnit.{succ u2}) (CategoryTheory.discreteCategory.{u2} PUnit.{succ u2})
+but is expected to have type
+  CategoryTheory.Equivalence.{u1, u2, u1, u2} (FundamentalGroupoid.{u1} PUnit.{succ u1}) (CategoryTheory.Discrete.{u2} PUnit.{succ u2}) (CategoryTheory.Groupoid.toCategory.{u1, u1} (FundamentalGroupoid.{u1} PUnit.{succ u1}) (FundamentalGroupoid.instGroupoidFundamentalGroupoid.{u1} PUnit.{succ u1} instTopologicalSpacePUnit.{u1})) (CategoryTheory.discreteCategory.{u2} PUnit.{succ u2})
+Case conversion may be inaccurate. Consider using '#align fundamental_groupoid.punit_equiv_discrete_punit FundamentalGroupoid.punitEquivDiscretePunitₓ'. -/
 /-- Equivalence of groupoids between fundamental groupoid of punit and punit -/
 def punitEquivDiscretePunit : FundamentalGroupoid PUnit.{u + 1} ≌ Discrete PUnit.{v + 1} :=
   Equivalence.mk (Functor.star _) ((CategoryTheory.Functor.const _).obj PUnit.unit)

Mathbin/Analysis/Normed/Group/Completion.lean

@@ -49,7 +49,7 @@ theorem norm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)
 #align uniform_space.completion.norm_coe UniformSpace.Completion.norm_coe
 
 instance [SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E) :=
-  { Completion.addCommGroup, Completion.metricSpace with
+  { Completion.addCommGroup, Completion.instMetricSpace with
     dist_eq := by
       intro x y
       apply completion.induction_on₂ x y <;> clear x y