bump to nightly-2023-03-22-02

mathlib commit leanprover-community/mathlib@dd6388c

Mathbin/Algebra/DirectSum/Finsupp.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module algebra.direct_sum.finsupp
-! leanprover-community/mathlib commit aca0874a9ce95510752f4075f80f273172e9b177
+! leanprover-community/mathlib commit aa3a420527e0fbfd0f6615b95b761254a9166e12
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Data.Finsupp.ToDfinsupp
 /-!
 # Results on direct sums and finitely supported functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 1. The linear equivalence between finitely supported functions `ι →₀ M` and
 the direct sum of copies of `M` indexed by `ι`.
 -/

Mathbin/Algebra/FreeAlgebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Adam Topaz
 
 ! This file was ported from Lean 3 source module algebra.free_algebra
-! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
+! leanprover-community/mathlib commit aa3a420527e0fbfd0f6615b95b761254a9166e12
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.MonoidAlgebra.Basic
 /-!
 # Free Algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a commutative semiring `R`, and a type `X`, we construct the free unital, associative
 `R`-algebra on `X`.
 
@@ -386,7 +389,7 @@ irreducible_def lift : (X → A) ≃ (FreeAlgebra R X →ₐ[R] A) :=
 
 /- warning: free_algebra.lift_aux_eq -> FreeAlgebra.liftAux_eq is a dubious translation:
 lean 3 declaration is
-  forall (R : Type.{u1}) [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}} {A : Type.{u3}} [_inst_2 : Semiring.{u3} A] [_inst_3 : Algebra.{u1, u3} R A _inst_1 _inst_2] (f : X -> A), Eq.{max (succ (max u1 u2)) (succ u3)} (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3) (_Private.1865498249.liftAux.{u1, u2, u3} R _inst_1 X A _inst_2 _inst_3 f) (coeFn.{max 1 (max (max (succ u2) (succ u3)) (succ (max u1 u2)) (succ u3)) (max (succ (max u1 u2)) (succ u3)) (succ u2) (succ u3), max (max (succ u2) (succ u3)) (succ (max u1 u2)) (succ u3)} (Equiv.{max (succ u2) (succ u3), max (succ (max u1 u2)) (succ u3)} (X -> A) (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) (fun (_x : Equiv.{max (succ u2) (succ u3), max (succ (max u1 u2)) (succ u3)} (X -> A) (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) => (X -> A) -> (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) (Equiv.hasCoeToFun.{max (succ u2) (succ u3), max (succ (max u1 u2)) (succ u3)} (X -> A) (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) (FreeAlgebra.lift.{u1, u2, u3} R _inst_1 X A _inst_2 _inst_3) f)
+  forall (R : Type.{u1}) [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}} {A : Type.{u3}} [_inst_2 : Semiring.{u3} A] [_inst_3 : Algebra.{u1, u3} R A _inst_1 _inst_2] (f : X -> A), Eq.{max (succ (max u1 u2)) (succ u3)} (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3) (_Private.3391014519.liftAux.{u1, u2, u3} R _inst_1 X A _inst_2 _inst_3 f) (coeFn.{max 1 (max (max (succ u2) (succ u3)) (succ (max u1 u2)) (succ u3)) (max (succ (max u1 u2)) (succ u3)) (succ u2) (succ u3), max (max (succ u2) (succ u3)) (succ (max u1 u2)) (succ u3)} (Equiv.{max (succ u2) (succ u3), max (succ (max u1 u2)) (succ u3)} (X -> A) (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) (fun (_x : Equiv.{max (succ u2) (succ u3), max (succ (max u1 u2)) (succ u3)} (X -> A) (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) => (X -> A) -> (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) (Equiv.hasCoeToFun.{max (succ u2) (succ u3), max (succ (max u1 u2)) (succ u3)} (X -> A) (AlgHom.{u1, max u1 u2, u3} R (FreeAlgebra.{u1, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) _inst_2 (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) _inst_3)) (FreeAlgebra.lift.{u1, u2, u3} R _inst_1 X A _inst_2 _inst_3) f)
 but is expected to have type
   forall (R : Type.{u3}) [_inst_1 : CommSemiring.{u3} R] {X : Type.{u2}} {A : Type.{u1}} [_inst_2 : Semiring.{u1} A] [_inst_3 : Algebra.{u3, u1} R A _inst_1 _inst_2] (f : X -> A), Eq.{max (max (succ u3) (succ u2)) (succ u1)} (AlgHom.{u3, max u2 u3, u1} R (FreeAlgebra.{u3, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_2 (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_3) (_private.Mathlib.Algebra.FreeAlgebra.0.FreeAlgebra.liftAux.{u3, u2, u1} R _inst_1 X A _inst_2 _inst_3 f) (FunLike.coe.{max (max (succ u3) (succ u1)) (succ u2), max (succ u1) (succ u2), max (max (succ u3) (succ u1)) (succ u2)} (Equiv.{max (succ u2) (succ u1), max (succ u1) (succ (max u2 u3))} (X -> A) (AlgHom.{u3, max u2 u3, u1} R (FreeAlgebra.{u3, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_2 (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_3)) (X -> A) (fun (_x : X -> A) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : X -> A) => AlgHom.{u3, max u2 u3, u1} R (FreeAlgebra.{u3, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_2 (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_3) _x) (Equiv.instFunLikeEquiv.{max (succ u1) (succ u2), max (max (succ u3) (succ u1)) (succ u2)} (X -> A) (AlgHom.{u3, max u2 u3, u1} R (FreeAlgebra.{u3, u2} R _inst_1 X) A _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_2 (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u3, u2} R _inst_1 X) _inst_3)) (FreeAlgebra.lift.{u3, u2, u1} R _inst_1 X A _inst_2 _inst_3) f)
 Case conversion may be inaccurate. Consider using '#align free_algebra.lift_aux_eq FreeAlgebra.liftAux_eqₓ'. -/

Mathbin/Algebra/Order/CompleteField.lean

@@ -178,7 +178,7 @@ end CutMap
 -/
 
 
-section InducedMap
+section [anonymous]
 
 variable (α β γ) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β]
   [ConditionallyCompleteLinearOrderedField γ]
@@ -257,7 +257,7 @@ theorem inducedMap_inv_self (b : β) : inducedMap γ β (inducedMap β γ b) = b
 
 theorem inducedMap_add (x y : α) : inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y :=
   by
-  rw [induced_map, cut_map_add]
+  rw [[anonymous], cut_map_add]
   exact
     csupₛ_add (cut_map_nonempty β x) (cut_map_bdd_above β x) (cut_map_nonempty β y)
       (cut_map_bdd_above β y)
@@ -372,7 +372,7 @@ fields. -/
 instance : Unique (β ≃+*o γ) :=
   uniqueOfSubsingleton <| inducedOrderRingIso β γ
 
-end InducedMap
+end [anonymous]
 
 end LinearOrderedField