bump to nightly-2023-05-10-02

mathlib commit leanprover-community/mathlib@cc5dd62

Mathbin/Algebra/BigOperators/Fin.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.big_operators.fin
-! leanprover-community/mathlib commit ef997baa41b5c428be3fb50089a7139bf4ee886b
+! leanprover-community/mathlib commit cc5dd6244981976cc9da7afc4eee5682b037a013
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -428,20 +428,19 @@ theorem partialProd_left_inv {G : Type _} [Group G] (f : Fin (n + 1) → G) :
 
 /- warning: fin.partial_prod_right_inv -> Fin.partialProd_right_inv is a dubious translation:
 lean 3 declaration is
-  forall {n : Nat} {G : Type.{u1}} [_inst_2 : Group.{u1} G] (g : G) (f : (Fin n) -> G) (i : Fin n), Eq.{succ u1} G (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toHasMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2))))) (Inv.inv.{u1} G (DivInvMonoid.toHasInv.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) (SMul.smul.{u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) -> G) (Function.hasSMul.{0, u1, u1} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) G G (Mul.toSMul.{u1} G (MulOneClass.toHasMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)))))) g (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n f) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) (Fin n) (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (HasLiftT.mk.{1, 1} (Fin n) (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (CoeTCₓ.coe.{1, 1} (Fin n) (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (coeTrans.{1, 1, 1} (Fin n) Nat (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (Nat.castCoe.{0} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (AddMonoidWithOne.toNatCast.{0} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (Fin.addMonoidWithOne (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))) (NeZero.succ n)))) (Fin.coeToNat n)))) i))) (SMul.smul.{u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) -> G) (Function.hasSMul.{0, u1, u1} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) G G (Mul.toSMul.{u1} G (MulOneClass.toHasMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)))))) g (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n f) (Fin.succ n i))) (f i)
+  forall {n : Nat} {G : Type.{u1}} [_inst_2 : Group.{u1} G] (f : (Fin n) -> G) (i : Fin n), Eq.{succ u1} G (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toHasMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2))))) (Inv.inv.{u1} G (DivInvMonoid.toHasInv.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n f (coeFn.{1, 1} (OrderEmbedding.{0, 0} (Fin n) (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (Fin.hasLe n) (Fin.hasLe (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))))) (fun (_x : RelEmbedding.{0, 0} (Fin n) (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (LE.le.{0} (Fin n) (Fin.hasLe n)) (LE.le.{0} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (Fin.hasLe (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))))) => (Fin n) -> (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))))) (RelEmbedding.hasCoeToFun.{0, 0} (Fin n) (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (LE.le.{0} (Fin n) (Fin.hasLe n)) (LE.le.{0} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))) (Fin.hasLe (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))))) (Fin.castSucc n) i))) (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n f (Fin.succ n i))) (f i)
 but is expected to have type
-  forall {n : Nat} {G : Type.{u1}} [_inst_2 : Group.{u1} G] (g : G) (f : (Fin n) -> G) (i : Fin n), Eq.{succ u1} G (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2))))) (Inv.inv.{u1} G (InvOneClass.toInv.{u1} G (DivInvOneMonoid.toInvOneClass.{u1} G (DivisionMonoid.toDivInvOneMonoid.{u1} G (Group.toDivisionMonoid.{u1} G _inst_2)))) (HSMul.hSMul.{u1, u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (instHSMul.{u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (Pi.instSMul.{0, u1, u1} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) G (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => G) (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => MulAction.toSMul.{u1, u1} G G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) (Monoid.toMulAction.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)))))) g (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n f) (Fin.castLT (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) n i (Nat.lt_succ_of_lt (Fin.val n i) n (Fin.isLt n i))))) (HSMul.hSMul.{u1, u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (instHSMul.{u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (Pi.instSMul.{0, u1, u1} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) G (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => G) (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => MulAction.toSMul.{u1, u1} G G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) (Monoid.toMulAction.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)))))) g (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n f) (Fin.succ n i))) (f i)
+  forall {n : Nat} {G : Type.{u1}} [_inst_2 : Group.{u1} G] (f : G) (i : (Fin n) -> G) (i_1 : Fin n), Eq.{succ u1} G (HMul.hMul.{u1, u1, u1} G G G (instHMul.{u1} G (MulOneClass.toMul.{u1} G (Monoid.toMulOneClass.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2))))) (Inv.inv.{u1} G (InvOneClass.toInv.{u1} G (DivInvOneMonoid.toInvOneClass.{u1} G (DivisionMonoid.toDivInvOneMonoid.{u1} G (Group.toDivisionMonoid.{u1} G _inst_2)))) (HSMul.hSMul.{u1, u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (instHSMul.{u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (Pi.instSMul.{0, u1, u1} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) G (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => G) (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => MulAction.toSMul.{u1, u1} G G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) (Monoid.toMulAction.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)))))) f (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n i) (Fin.castLT (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) n i_1 (Nat.lt_succ_of_lt (Fin.val n i_1) n (Fin.isLt n i_1))))) (HSMul.hSMul.{u1, u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (instHSMul.{u1, u1} G ((Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) -> G) (Pi.instSMul.{0, u1, u1} (Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) G (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => G) (fun (i : Fin (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))) => MulAction.toSMul.{u1, u1} G G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) (Monoid.toMulAction.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)))))) f (Fin.partialProd.{u1} G (DivInvMonoid.toMonoid.{u1} G (Group.toDivInvMonoid.{u1} G _inst_2)) n i) (Fin.succ n i_1))) (i i_1)
 Case conversion may be inaccurate. Consider using '#align fin.partial_prod_right_inv Fin.partialProd_right_invₓ'. -/
 @[to_additive]
-theorem partialProd_right_inv {G : Type _} [Group G] (g : G) (f : Fin n → G) (i : Fin n) :
-    ((g • partialProd f) i)⁻¹ * (g • partialProd f) i.succ = f i :=
+theorem partialProd_right_inv {G : Type _} [Group G] (f : Fin n → G) (i : Fin n) :
+    (partialProd f i.cast_succ)⁻¹ * partialProd f i.succ = f i :=
   by
   cases' i with i hn
   induction' i with i hi generalizing hn
-  · simp [← Fin.succ_mk, partial_prod_succ]
+  · simp [-Fin.succ_mk, partial_prod_succ]
   · specialize hi (lt_trans (Nat.lt_succ_self i) hn)
-    simp only [mul_inv_rev, Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk, smul_eq_mul,
-      Pi.smul_apply] at hi⊢
+    simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi⊢
     rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
     simp only [partial_prod_succ, mul_inv_rev, Fin.castSucc_mk]
     assoc_rw [hi, inv_mul_cancel_left]
@@ -460,15 +459,13 @@ theorem inv_partialProd_mul_eq_contractNth {G : Type _} [Group G] (g : Fin (n +
     (partialProd g (j.succ.succAbove k.cast_succ))⁻¹ * partialProd g (j.succAbove k).succ =
       j.contractNth Mul.mul g k :=
   by
-  have := partial_prod_right_inv (1 : G) g
-  simp only [one_smul, coe_eq_cast_succ] at this
   rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-  · rwa [succ_above_below, succ_above_below, this, contract_nth_apply_of_lt]
+  · rwa [succ_above_below, succ_above_below, partial_prod_right_inv, contract_nth_apply_of_lt]
     · assumption
     · rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe]
       exact le_of_lt h
   · rwa [succ_above_below, succ_above_above, partial_prod_succ, cast_succ_fin_succ, ← mul_assoc,
-      this, contract_nth_apply_of_eq]
+      partial_prod_right_inv, contract_nth_apply_of_eq]
     · simpa only [le_iff_coe_le_coe, ← h]
     · rw [cast_succ_lt_iff_succ_le, succ_le_succ_iff, le_iff_coe_le_coe]
       exact le_of_eq h

Mathbin/Algebra/Category/Group/EquivalenceGroupAddGroup.lean

@@ -26,72 +26,92 @@ open CategoryTheory
 
 namespace GroupCat
 
+#print GroupCat.toAddGroupCat /-
 /-- The functor `Group ⥤ AddGroup` by sending `X ↦ additive X` and `f ↦ f`.
 -/
 @[simps]
-def toAddGroup : GroupCat ⥤ AddGroupCat
+def toAddGroupCat : GroupCat ⥤ AddGroupCat
     where
   obj X := AddGroupCat.of (Additive X)
   map X Y := MonoidHom.toAdditive
-#align Group.to_AddGroup GroupCat.toAddGroup
+#align Group.to_AddGroup GroupCat.toAddGroupCat
+-/
 
 end GroupCat
 
 namespace CommGroupCat
 
+#print CommGroupCat.toAddCommGroupCat /-
 /-- The functor `CommGroup ⥤ AddCommGroup` by sending `X ↦ additive X` and `f ↦ f`.
 -/
 @[simps]
-def toAddCommGroup : CommGroupCat ⥤ AddCommGroupCat
+def toAddCommGroupCat : CommGroupCat ⥤ AddCommGroupCat
     where
   obj X := AddCommGroupCat.of (Additive X)
   map X Y := MonoidHom.toAdditive
-#align CommGroup.to_AddCommGroup CommGroupCat.toAddCommGroup
+#align CommGroup.to_AddCommGroup CommGroupCat.toAddCommGroupCat
+-/
 
 end CommGroupCat
 
 namespace AddGroupCat
 
+#print AddGroupCat.toGroupCat /-
 /-- The functor `AddGroup ⥤ Group` by sending `X ↦ multiplicative Y` and `f ↦ f`.
 -/
 @[simps]
-def toGroup : AddGroupCat ⥤ GroupCat
+def toGroupCat : AddGroupCat ⥤ GroupCat
     where
   obj X := GroupCat.of (Multiplicative X)
   map X Y := AddMonoidHom.toMultiplicative
-#align AddGroup.to_Group AddGroupCat.toGroup
+#align AddGroup.to_Group AddGroupCat.toGroupCat
+-/
 
 end AddGroupCat
 
 namespace AddCommGroupCat
 
+#print AddCommGroupCat.toCommGroupCat /-
 /-- The functor `AddCommGroup ⥤ CommGroup` by sending `X ↦ multiplicative Y` and `f ↦ f`.
 -/
 @[simps]
-def toCommGroup : AddCommGroupCat ⥤ CommGroupCat
+def toCommGroupCat : AddCommGroupCat ⥤ CommGroupCat
     where
   obj X := CommGroupCat.of (Multiplicative X)
   map X Y := AddMonoidHom.toMultiplicative
-#align AddCommGroup.to_CommGroup AddCommGroupCat.toCommGroup
+#align AddCommGroup.to_CommGroup AddCommGroupCat.toCommGroupCat
+-/
 
 end AddCommGroupCat
 
+/- warning: Group_AddGroup_equivalence -> groupAddGroupEquivalence is a dubious translation:
+lean 3 declaration is
+  CategoryTheory.Equivalence.{u1, u1, succ u1, succ u1} GroupCat.{u1} GroupCat.largeCategory.{u1} AddGroupCat.{u1} AddGroupCat.largeCategory.{u1}
+but is expected to have type
+  CategoryTheory.Equivalence.{u1, u1, succ u1, succ u1} GroupCat.{u1} AddGroupCat.{u1} GroupCat.largeCategory.{u1} AddGroupCat.largeCategory.{u1}
+Case conversion may be inaccurate. Consider using '#align Group_AddGroup_equivalence groupAddGroupEquivalenceₓ'. -/
 /-- The equivalence of categories between `Group` and `AddGroup`
 -/
 @[simps]
 def groupAddGroupEquivalence : GroupCat ≌ AddGroupCat :=
-  Equivalence.mk GroupCat.toAddGroup AddGroupCat.toGroup
+  Equivalence.mk GroupCat.toAddGroupCat AddGroupCat.toGroupCat
     (NatIso.ofComponents (fun X => MulEquiv.toGroupCatIso (MulEquiv.multiplicativeAdditive X))
       fun X Y f => rfl)
     (NatIso.ofComponents (fun X => AddEquiv.toAddGroupCatIso (AddEquiv.additiveMultiplicative X))
       fun X Y f => rfl)
 #align Group_AddGroup_equivalence groupAddGroupEquivalence
 
+/- warning: CommGroup_AddCommGroup_equivalence -> commGroupAddCommGroupEquivalence is a dubious translation:
+lean 3 declaration is
+  CategoryTheory.Equivalence.{u1, u1, succ u1, succ u1} CommGroupCat.{u1} CommGroupCat.largeCategory.{u1} AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}
+but is expected to have type
+  CategoryTheory.Equivalence.{u1, u1, succ u1, succ u1} CommGroupCat.{u1} AddCommGroupCat.{u1} CommGroupCat.largeCategory.{u1} AddCommGroupCat.largeCategory.{u1}
+Case conversion may be inaccurate. Consider using '#align CommGroup_AddCommGroup_equivalence commGroupAddCommGroupEquivalenceₓ'. -/
 /-- The equivalence of categories between `CommGroup` and `AddCommGroup`.
 -/
 @[simps]
 def commGroupAddCommGroupEquivalence : CommGroupCat ≌ AddCommGroupCat :=
-  Equivalence.mk CommGroupCat.toAddCommGroup AddCommGroupCat.toCommGroup
+  Equivalence.mk CommGroupCat.toAddCommGroupCat AddCommGroupCat.toCommGroupCat
     (NatIso.ofComponents (fun X => MulEquiv.toCommGroupCatIso (MulEquiv.multiplicativeAdditive X))
       fun X Y f => rfl)
     (NatIso.ofComponents

Mathbin/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.translations
-! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
+! leanprover-community/mathlib commit 7d34004e19699895c13c86b78ae62bbaea0bc893
 ! 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.ContinuedFractions.Translations
 /-!
 # Basic Translation Lemmas Between Structures Defined for Computing Continued Fractions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 This is a collection of simple lemmas between the different structures used for the computation

Mathbin/Algebra/MonoidAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.monoid_algebra.basic
-! leanprover-community/mathlib commit f69db8cecc668e2d5894d7e9bfc491da60db3b9f
+! leanprover-community/mathlib commit 949dc57e616a621462062668c9f39e4e17b64b69
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -369,8 +369,8 @@ instance [Monoid R] [Semiring k] [DistribMulAction R k] [FaithfulSMul R k] [None
     FaithfulSMul R (MonoidAlgebra k G) :=
   Finsupp.faithfulSMul
 
-instance [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction S k] [SMul R S]
-    [IsScalarTower R S k] : IsScalarTower R S (MonoidAlgebra k G) :=
+instance [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :
+    IsScalarTower R S (MonoidAlgebra k G) :=
   Finsupp.isScalarTower G k
 
 instance [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction S k]

Mathbin/Analysis/Calculus/BumpFunctionInner.lean

@@ -597,7 +597,7 @@ protected theorem integrable_normed : Integrable (f.normed μ) μ :=
   f.Integrable.div_const _
 #align cont_diff_bump.integrable_normed ContDiffBump.integrable_normed
 
-variable [μ.IsOpenPosMeasure]
+variable [μ.OpenPosMeasure]
 
 theorem integral_pos : 0 < ∫ x, f x ∂μ :=
   by