bump to nightly-2023-05-24-12

mathlib commit leanprover-community/mathlib@8d33f09
leanprover-community · May 24, 2023 · 2a3e3db · 2a3e3db
1 parent bcb5c9b
commit 2a3e3db
Show file tree

Hide file tree

Showing 36 changed files with 2,097 additions and 455 deletions.
diff --git a/Mathbin/Algebra/Category/Group/FilteredColimits.lean b/Mathbin/Algebra/Category/Group/FilteredColimits.lean
diff --git a/Mathbin/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathbin/AlgebraicGeometry/PrimeSpectrum/Basic.lean
diff --git a/Mathbin/Analysis/BoxIntegral/Partition/Additive.lean b/Mathbin/Analysis/BoxIntegral/Partition/Additive.lean
diff --git a/Mathbin/Analysis/Calculus/Fderiv/Add.lean b/Mathbin/Analysis/Calculus/Fderiv/Add.lean
diff --git a/Mathbin/Analysis/Calculus/Fderiv/Comp.lean b/Mathbin/Analysis/Calculus/Fderiv/Comp.lean
diff --git a/Mathbin/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathbin/Analysis/Calculus/FormalMultilinearSeries.lean
diff --git a/Mathbin/Analysis/Complex/Basic.lean b/Mathbin/Analysis/Complex/Basic.lean
diff --git a/Mathbin/Analysis/LocallyConvex/WeakDual.lean b/Mathbin/Analysis/LocallyConvex/WeakDual.lean
@@ -159,7 +159,7 @@ variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [M
 variable [Nonempty ι] [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
 
 instance {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} : LocallyConvexSpace ℝ (WeakBilin B) :=
-  B.weakBilin_withSeminorms.to_locallyConvexSpace
+  B.weakBilin_withSeminorms.toLocallyConvexSpace
 
 end LocallyConvex
 
diff --git a/Mathbin/Analysis/LocallyConvex/WithSeminorms.lean b/Mathbin/Analysis/LocallyConvex/WithSeminorms.lean
diff --git a/Mathbin/Analysis/Normed/Group/Basic.lean b/Mathbin/Analysis/Normed/Group/Basic.lean
@@ -3205,14 +3205,14 @@ instance (priority := 100) SeminormedCommGroup.to_uniformGroup : UniformGroup E
 #align seminormed_add_comm_group.to_uniform_add_group SeminormedAddCommGroup.to_uniformAddGroup
 -/
 
-#print SeminormedCommGroup.to_topologicalGroup /-
+#print SeminormedCommGroup.toTopologicalGroup /-
 -- short-circuit type class inference
 -- See note [lower instance priority]
 @[to_additive]
-instance (priority := 100) SeminormedCommGroup.to_topologicalGroup : TopologicalGroup E :=
+instance (priority := 100) SeminormedCommGroup.toTopologicalGroup : TopologicalGroup E :=
   inferInstance
-#align seminormed_comm_group.to_topological_group SeminormedCommGroup.to_topologicalGroup
-#align seminormed_add_comm_group.to_topological_add_group SeminormedAddCommGroup.to_topologicalAddGroup
+#align seminormed_comm_group.to_topological_group SeminormedCommGroup.toTopologicalGroup
+#align seminormed_add_comm_group.to_topological_add_group SeminormedAddCommGroup.toTopologicalAddGroup
 -/
 
 #print cauchySeq_prod_of_eventually_eq /-

diff --git a/Mathbin/Analysis/Normed/Group/ControlledClosure.lean b/Mathbin/Analysis/Normed/Group/ControlledClosure.lean
diff --git a/Mathbin/Analysis/Normed/Group/Quotient.lean b/Mathbin/Analysis/Normed/Group/Quotient.lean
diff --git a/Mathbin/Analysis/Normed/MulAction.lean b/Mathbin/Analysis/Normed/MulAction.lean
diff --git a/Mathbin/Analysis/NormedSpace/Basic.lean b/Mathbin/Analysis/NormedSpace/Basic.lean
diff --git a/Mathbin/Analysis/NormedSpace/BoundedLinearMaps.lean b/Mathbin/Analysis/NormedSpace/BoundedLinearMaps.lean
diff --git a/Mathbin/Analysis/NormedSpace/ConformalLinearMap.lean b/Mathbin/Analysis/NormedSpace/ConformalLinearMap.lean
diff --git a/Mathbin/Analysis/NormedSpace/ContinuousLinearMap.lean b/Mathbin/Analysis/NormedSpace/ContinuousLinearMap.lean
diff --git a/Mathbin/Analysis/NormedSpace/FiniteDimension.lean b/Mathbin/Analysis/NormedSpace/FiniteDimension.lean
diff --git a/Mathbin/Analysis/NormedSpace/HahnBanach/Extension.lean b/Mathbin/Analysis/NormedSpace/HahnBanach/Extension.lean
diff --git a/Mathbin/Analysis/NormedSpace/Multilinear.lean b/Mathbin/Analysis/NormedSpace/Multilinear.lean
diff --git a/Mathbin/Analysis/NormedSpace/OperatorNorm.lean b/Mathbin/Analysis/NormedSpace/OperatorNorm.lean
diff --git a/Mathbin/Analysis/NormedSpace/Star/Mul.lean b/Mathbin/Analysis/NormedSpace/Star/Mul.lean
diff --git a/Mathbin/Analysis/SchwartzSpace.lean b/Mathbin/Analysis/SchwartzSpace.lean
@@ -597,7 +597,7 @@ instance : UniformAddGroup 𝓢(E, F) :=
   (schwartzSeminormFamily ℝ E F).AddGroupFilterBasis.UniformAddGroup
 
 instance : LocallyConvexSpace ℝ 𝓢(E, F) :=
-  (schwartz_withSeminorms ℝ E F).to_locallyConvexSpace
+  (schwartz_withSeminorms ℝ E F).toLocallyConvexSpace
 
 instance : TopologicalSpace.FirstCountableTopology 𝓢(E, F) :=
   (schwartz_withSeminorms ℝ E F).first_countable

diff --git a/Mathbin/Data/Fintype/Quotient.lean b/Mathbin/Data/Fintype/Quotient.lean
@@ -23,6 +23,7 @@ to a quotient of finite families.
 -/
 
 
+#print Quotient.finChoiceAux /-
 /-- An auxiliary function for `quotient.fin_choice`.  Given a
 collection of setoids indexed by a type `ι`, a (finite) list `l` of
 indices, and a function that for each `i ∈ l` gives a term of the
@@ -44,7 +45,14 @@ def Quotient.finChoiceAux {ι : Type _} [DecidableEq ι] {α : ι → Type _} [S
       exact h₁
     · exact h₂ _ _
 #align quotient.fin_choice_aux Quotient.finChoiceAux
+-/
 
+/- warning: quotient.fin_choice_aux_eq -> Quotient.finChoiceAux_eq is a dubious translation:
+lean 3 declaration is
+  forall {ι : Type.{u1}} [_inst_1 : DecidableEq.{succ u1} ι] {α : ι -> Type.{u2}} [S : forall (i : ι), Setoid.{succ u2} (α i)] (l : List.{u1} ι) (f : forall (i : ι), (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) -> (α i)), Eq.{max (succ u1) (succ u2)} (Quotient.{max (succ u1) (succ u2)} (forall (i : ι), (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) -> (α i)) (piSetoid.{succ u1, succ u2} ι (fun (i : ι) => (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) -> (α i)) (fun (i : ι) => piSetoid.{0, succ u2} (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) (fun (H : Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) => α i) (fun (i_1 : Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) => S i)))) (Quotient.finChoiceAux.{u1, u2} ι (fun (a : ι) (b : ι) => _inst_1 a b) (fun (i : ι) => α i) (fun (i : ι) => S i) l (fun (i : ι) (h : Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) => Quotient.mk'.{succ u2} (α i) (S i) (f i h))) (Quotient.mk'.{max (succ u1) (succ u2)} (forall (i : ι), (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) -> (α i)) (piSetoid.{succ u1, succ u2} ι (fun (i : ι) => (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) -> (α i)) (fun (i : ι) => piSetoid.{0, succ u2} (Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) (fun (H : Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) => α i) (fun (i_1 : Membership.Mem.{u1, u1} ι (List.{u1} ι) (List.hasMem.{u1} ι) i l) => S i))) f)
+but is expected to have type
+  forall {ι : Type.{u2}} [_inst_1 : DecidableEq.{succ u2} ι] {α : ι -> Type.{u1}} [S : forall (i : ι), Setoid.{succ u1} (α i)] (l : List.{u2} ι) (f : forall (i : ι), (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i)), Eq.{max (succ u2) (succ u1)} (Quotient.{max (succ u2) (succ u1)} (forall (i : ι), (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i)) (inferInstance.{max (succ u2) (succ u1)} (Setoid.{max (succ u2) (succ u1)} (forall (i : ι), (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i))) (piSetoid.{succ u2, succ u1} ι (fun (i : ι) => (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i)) (fun (i : ι) => piSetoid.{0, succ u1} (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) (fun (a._@.Mathlib.Data.Fintype.Quotient._hyg.57 : Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) => α i) (fun (i_1 : Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) => (fun (i : ι) => S i) i))))) (Quotient.finChoiceAux.{u2, u1} ι (fun (a : ι) (b : ι) => _inst_1 a b) (fun (i : ι) => α i) (fun (i : ι) => S i) l (fun (i : ι) (h : Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) => Quotient.mk.{succ u1} (α i) (S i) (f i h))) (Quotient.mk.{max (succ u2) (succ u1)} (forall (i : ι), (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i)) (inferInstance.{max (succ u2) (succ u1)} (Setoid.{max (succ u2) (succ u1)} (forall (i : ι), (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i))) (piSetoid.{succ u2, succ u1} ι (fun (i : ι) => (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) -> (α i)) (fun (i : ι) => piSetoid.{0, succ u1} (Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) (fun (a._@.Mathlib.Data.Fintype.Quotient._hyg.57 : Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) => α i) (fun (i_1 : Membership.mem.{u2, u2} ι (List.{u2} ι) (List.instMembershipList.{u2} ι) i l) => (fun (i : ι) => S i) i)))) f)
+Case conversion may be inaccurate. Consider using '#align quotient.fin_choice_aux_eq Quotient.finChoiceAux_eqₓ'. -/
 theorem Quotient.finChoiceAux_eq {ι : Type _} [DecidableEq ι] {α : ι → Type _}
     [S : ∀ i, Setoid (α i)] :
     ∀ (l : List ι) (f : ∀ i ∈ l, α i), (Quotient.finChoiceAux l fun i h => ⟦f i h⟧) = ⟦f⟧
@@ -56,6 +64,7 @@ theorem Quotient.finChoiceAux_eq {ι : Type _} [DecidableEq ι] {α : ι → Typ
     subst j; rfl
 #align quotient.fin_choice_aux_eq Quotient.finChoiceAux_eq
 
+#print Quotient.finChoice /-
 /-- Given a collection of setoids indexed by a fintype `ι` and a
 function that for each `i : ι` gives a term of the corresponding
 quotient type, then there is corresponding term in the quotient of the
@@ -74,7 +83,14 @@ def Quotient.finChoice {ι : Type _} [DecidableEq ι] [Fintype ι] {α : ι →
       congr 1; exact Quotient.sound h)
     (fun f => ⟦fun i => f i (Finset.mem_univ _)⟧) fun a b h => Quotient.sound fun i => h _ _
 #align quotient.fin_choice Quotient.finChoice
+-/
 
+/- warning: quotient.fin_choice_eq -> Quotient.finChoice_eq is a dubious translation:
+lean 3 declaration is
+  forall {ι : Type.{u1}} [_inst_1 : DecidableEq.{succ u1} ι] [_inst_2 : Fintype.{u1} ι] {α : ι -> Type.{u2}} [_inst_3 : forall (i : ι), Setoid.{succ u2} (α i)] (f : forall (i : ι), α i), Eq.{max (succ u1) (succ u2)} (Quotient.{max (succ u1) (succ u2)} (forall (i : ι), α i) (piSetoid.{succ u1, succ u2} ι (fun (i : ι) => α i) (fun (i : ι) => _inst_3 i))) (Quotient.finChoice.{u1, u2} ι (fun (a : ι) (b : ι) => _inst_1 a b) _inst_2 (fun (i : ι) => α i) (fun (i : ι) => _inst_3 i) (fun (i : ι) => Quotient.mk'.{succ u2} (α i) (_inst_3 i) (f i))) (Quotient.mk'.{max (succ u1) (succ u2)} (forall (i : ι), α i) (piSetoid.{succ u1, succ u2} ι (fun (i : ι) => α i) (fun (i : ι) => _inst_3 i)) f)
+but is expected to have type
+  forall {ι : Type.{u2}} [_inst_1 : DecidableEq.{succ u2} ι] [_inst_2 : Fintype.{u2} ι] {α : ι -> Type.{u1}} [_inst_3 : forall (i : ι), Setoid.{succ u1} (α i)] (f : forall (i : ι), α i), Eq.{max (succ u2) (succ u1)} (Quotient.{max (succ u2) (succ u1)} (forall (i : ι), α i) (inferInstance.{max (succ u2) (succ u1)} (Setoid.{max (succ u2) (succ u1)} (forall (i : ι), α i)) (piSetoid.{succ u2, succ u1} ι (fun (i : ι) => α i) (fun (i : ι) => _inst_3 i)))) (Quotient.finChoice.{u2, u1} ι (fun (a : ι) (b : ι) => _inst_1 a b) _inst_2 (fun (i : ι) => α i) (fun (i : ι) => _inst_3 i) (fun (i : ι) => Quotient.mk.{succ u1} (α i) (_inst_3 i) (f i))) (Quotient.mk.{max (succ u2) (succ u1)} (forall (i : ι), α i) (inferInstance.{max (succ u2) (succ u1)} (Setoid.{max (succ u2) (succ u1)} (forall (i : ι), α i)) (piSetoid.{succ u2, succ u1} ι (fun (i : ι) => α i) (fun (i : ι) => _inst_3 i))) f)
+Case conversion may be inaccurate. Consider using '#align quotient.fin_choice_eq Quotient.finChoice_eqₓ'. -/
 theorem Quotient.finChoice_eq {ι : Type _} [DecidableEq ι] [Fintype ι] {α : ι → Type _}
     [∀ i, Setoid (α i)] (f : ∀ i, α i) : (Quotient.finChoice fun i => ⟦f i⟧) = ⟦f⟧ :=
   by