bump to nightly-2023-03-11-22

mathlib commit leanprover-community/mathlib@3180fab
leanprover-community · Mar 11, 2023 · a8ee822 · a8ee822
1 parent 45969aa
commit a8ee822
Show file tree

Hide file tree

Showing 384 changed files with 4,322 additions and 4,314 deletions.
diff --git a/Mathbin/Algebra/AddTorsor.lean b/Mathbin/Algebra/AddTorsor.lean
@@ -570,7 +570,7 @@ def vaddConst (p : P) : G ≃ P where
 lean 3 declaration is
   forall {G : Type.{u1}} {P : Type.{u2}} [_inst_1 : AddGroup.{u1} G] [_inst_2 : AddTorsor.{u1, u2} G P _inst_1] (p : P), Eq.{max (succ u1) (succ u2)} (G -> P) (coeFn.{max 1 (max (succ u1) (succ u2)) (succ u2) (succ u1), max (succ u1) (succ u2)} (Equiv.{succ u1, succ u2} G P) (fun (_x : Equiv.{succ u1, succ u2} G P) => G -> P) (Equiv.hasCoeToFun.{succ u1, succ u2} G P) (Equiv.vaddConst.{u1, u2} G P _inst_1 _inst_2 p)) (fun (v : G) => VAdd.vadd.{u1, u2} G P (AddAction.toHasVadd.{u1, u2} G P (SubNegMonoid.toAddMonoid.{u1} G (AddGroup.toSubNegMonoid.{u1} G _inst_1)) (AddTorsor.toAddAction.{u1, u2} G P _inst_1 _inst_2)) v p)
 but is expected to have type
-  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : G), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : G) => P) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Equiv.{succ u2, succ u1} G P) G (fun (_x : G) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : G) => P) _x) (Equiv.instFunLikeEquiv.{succ u2, succ u1} G P) (Equiv.vaddConst.{u2, u1} G P _inst_1 _inst_2 p)) (fun (v : G) => HVAdd.hVAdd.{u2, u1, u1} G P ((fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : G) => P) v) (instHVAdd.{u2, u1} G P (AddAction.toVAdd.{u2, u1} G P (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G _inst_1)) (AddTorsor.toAddAction.{u2, u1} G P _inst_1 _inst_2))) v p)
+  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : G), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : G) => P) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Equiv.{succ u2, succ u1} G P) G (fun (_x : G) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : G) => P) _x) (Equiv.instFunLikeEquiv.{succ u2, succ u1} G P) (Equiv.vaddConst.{u2, u1} G P _inst_1 _inst_2 p)) (fun (v : G) => HVAdd.hVAdd.{u2, u1, u1} G P ((fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : G) => P) v) (instHVAdd.{u2, u1} G P (AddAction.toVAdd.{u2, u1} G P (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G _inst_1)) (AddTorsor.toAddAction.{u2, u1} G P _inst_1 _inst_2))) v p)
 Case conversion may be inaccurate. Consider using '#align equiv.coe_vadd_const Equiv.coe_vaddConstₓ'. -/
 @[simp]
 theorem coe_vaddConst (p : P) : ⇑(vaddConst p) = fun v => v +ᵥ p :=
@@ -581,7 +581,7 @@ theorem coe_vaddConst (p : P) : ⇑(vaddConst p) = fun v => v +ᵥ p :=
 lean 3 declaration is
   forall {G : Type.{u1}} {P : Type.{u2}} [_inst_1 : AddGroup.{u1} G] [_inst_2 : AddTorsor.{u1, u2} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (P -> G) (coeFn.{max 1 (max (succ u2) (succ u1)) (succ u1) (succ u2), max (succ u2) (succ u1)} (Equiv.{succ u2, succ u1} P G) (fun (_x : Equiv.{succ u2, succ u1} P G) => P -> G) (Equiv.hasCoeToFun.{succ u2, succ u1} P G) (Equiv.symm.{succ u1, succ u2} G P (Equiv.vaddConst.{u1, u2} G P _inst_1 _inst_2 p))) (fun (p' : P) => VSub.vsub.{u1, u2} G P (AddTorsor.toHasVsub.{u1, u2} G P _inst_1 _inst_2) p' p)
 but is expected to have type
-  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : P), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => G) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u1, succ u2} (Equiv.{succ u1, succ u2} P G) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => G) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u2} P G) (Equiv.symm.{succ u2, succ u1} G P (Equiv.vaddConst.{u2, u1} G P _inst_1 _inst_2 p))) (fun (p' : P) => VSub.vsub.{u2, u1} G P (AddTorsor.toVSub.{u2, u1} G P _inst_1 _inst_2) p' p)
+  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : P), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => G) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u1, succ u2} (Equiv.{succ u1, succ u2} P G) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => G) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u2} P G) (Equiv.symm.{succ u2, succ u1} G P (Equiv.vaddConst.{u2, u1} G P _inst_1 _inst_2 p))) (fun (p' : P) => VSub.vsub.{u2, u1} G P (AddTorsor.toVSub.{u2, u1} G P _inst_1 _inst_2) p' p)
 Case conversion may be inaccurate. Consider using '#align equiv.coe_vadd_const_symm Equiv.coe_vaddConst_symmₓ'. -/
 @[simp]
 theorem coe_vaddConst_symm (p : P) : ⇑(vaddConst p).symm = fun p' => p' -ᵥ p :=
@@ -602,7 +602,7 @@ def constVSub (p : P) : P ≃ G where
 lean 3 declaration is
   forall {G : Type.{u1}} {P : Type.{u2}} [_inst_1 : AddGroup.{u1} G] [_inst_2 : AddTorsor.{u1, u2} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (P -> G) (coeFn.{max 1 (max (succ u2) (succ u1)) (succ u1) (succ u2), max (succ u2) (succ u1)} (Equiv.{succ u2, succ u1} P G) (fun (_x : Equiv.{succ u2, succ u1} P G) => P -> G) (Equiv.hasCoeToFun.{succ u2, succ u1} P G) (Equiv.constVSub.{u1, u2} G P _inst_1 _inst_2 p)) (VSub.vsub.{u1, u2} G P (AddTorsor.toHasVsub.{u1, u2} G P _inst_1 _inst_2) p)
 but is expected to have type
-  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : P), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => G) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u1, succ u2} (Equiv.{succ u1, succ u2} P G) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => G) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u2} P G) (Equiv.constVSub.{u2, u1} G P _inst_1 _inst_2 p)) ((fun (x._@.Mathlib.Algebra.AddTorsor._hyg.2806 : P) (x._@.Mathlib.Algebra.AddTorsor._hyg.2808 : P) => VSub.vsub.{u2, u1} G P (AddTorsor.toVSub.{u2, u1} G P _inst_1 _inst_2) x._@.Mathlib.Algebra.AddTorsor._hyg.2806 x._@.Mathlib.Algebra.AddTorsor._hyg.2808) p)
+  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : P), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => G) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u1, succ u2} (Equiv.{succ u1, succ u2} P G) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => G) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u2} P G) (Equiv.constVSub.{u2, u1} G P _inst_1 _inst_2 p)) ((fun (x._@.Mathlib.Algebra.AddTorsor._hyg.2809 : P) (x._@.Mathlib.Algebra.AddTorsor._hyg.2811 : P) => VSub.vsub.{u2, u1} G P (AddTorsor.toVSub.{u2, u1} G P _inst_1 _inst_2) x._@.Mathlib.Algebra.AddTorsor._hyg.2809 x._@.Mathlib.Algebra.AddTorsor._hyg.2811) p)
 Case conversion may be inaccurate. Consider using '#align equiv.coe_const_vsub Equiv.coe_constVSubₓ'. -/
 @[simp]
 theorem coe_constVSub (p : P) : ⇑(constVSub p) = (· -ᵥ ·) p :=
@@ -613,7 +613,7 @@ theorem coe_constVSub (p : P) : ⇑(constVSub p) = (· -ᵥ ·) p :=
 lean 3 declaration is
   forall {G : Type.{u1}} {P : Type.{u2}} [_inst_1 : AddGroup.{u1} G] [_inst_2 : AddTorsor.{u1, u2} G P _inst_1] (p : P), Eq.{max (succ u1) (succ u2)} (G -> P) (coeFn.{max 1 (max (succ u1) (succ u2)) (succ u2) (succ u1), max (succ u1) (succ u2)} (Equiv.{succ u1, succ u2} G P) (fun (_x : Equiv.{succ u1, succ u2} G P) => G -> P) (Equiv.hasCoeToFun.{succ u1, succ u2} G P) (Equiv.symm.{succ u2, succ u1} P G (Equiv.constVSub.{u1, u2} G P _inst_1 _inst_2 p))) (fun (v : G) => VAdd.vadd.{u1, u2} G P (AddAction.toHasVadd.{u1, u2} G P (SubNegMonoid.toAddMonoid.{u1} G (AddGroup.toSubNegMonoid.{u1} G _inst_1)) (AddTorsor.toAddAction.{u1, u2} G P _inst_1 _inst_2)) (Neg.neg.{u1} G (SubNegMonoid.toHasNeg.{u1} G (AddGroup.toSubNegMonoid.{u1} G _inst_1)) v) p)
 but is expected to have type
-  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : G), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : G) => P) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Equiv.{succ u2, succ u1} G P) G (fun (_x : G) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : G) => P) _x) (Equiv.instFunLikeEquiv.{succ u2, succ u1} G P) (Equiv.symm.{succ u1, succ u2} P G (Equiv.constVSub.{u2, u1} G P _inst_1 _inst_2 p))) (fun (v : G) => HVAdd.hVAdd.{u2, u1, u1} G P P (instHVAdd.{u2, u1} G P (AddAction.toVAdd.{u2, u1} G P (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G _inst_1)) (AddTorsor.toAddAction.{u2, u1} G P _inst_1 _inst_2))) (Neg.neg.{u2} G (NegZeroClass.toNeg.{u2} G (SubNegZeroMonoid.toNegZeroClass.{u2} G (SubtractionMonoid.toSubNegZeroMonoid.{u2} G (AddGroup.toSubtractionMonoid.{u2} G _inst_1)))) v) p)
+  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] (p : P), Eq.{max (succ u2) (succ u1)} (forall (ᾰ : G), (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : G) => P) ᾰ) (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Equiv.{succ u2, succ u1} G P) G (fun (_x : G) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : G) => P) _x) (Equiv.instFunLikeEquiv.{succ u2, succ u1} G P) (Equiv.symm.{succ u1, succ u2} P G (Equiv.constVSub.{u2, u1} G P _inst_1 _inst_2 p))) (fun (v : G) => HVAdd.hVAdd.{u2, u1, u1} G P P (instHVAdd.{u2, u1} G P (AddAction.toVAdd.{u2, u1} G P (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G _inst_1)) (AddTorsor.toAddAction.{u2, u1} G P _inst_1 _inst_2))) (Neg.neg.{u2} G (NegZeroClass.toNeg.{u2} G (SubNegZeroMonoid.toNegZeroClass.{u2} G (SubtractionMonoid.toSubNegZeroMonoid.{u2} G (AddGroup.toSubtractionMonoid.{u2} G _inst_1)))) v) p)
 Case conversion may be inaccurate. Consider using '#align equiv.coe_const_vsub_symm Equiv.coe_constVSub_symmₓ'. -/
 @[simp]
 theorem coe_constVSub_symm (p : P) : ⇑(constVSub p).symm = fun v => -v +ᵥ p :=
@@ -716,7 +716,7 @@ theorem pointReflection_involutive (x : P) : Involutive (pointReflection x : P
 lean 3 declaration is
   forall {G : Type.{u1}} {P : Type.{u2}} [_inst_1 : AddGroup.{u1} G] [_inst_2 : AddTorsor.{u1, u2} G P _inst_1] {x : P} {y : P}, (Function.Injective.{succ u1, succ u1} G G (bit0.{u1} G (AddZeroClass.toHasAdd.{u1} G (AddMonoid.toAddZeroClass.{u1} G (SubNegMonoid.toAddMonoid.{u1} G (AddGroup.toSubNegMonoid.{u1} G _inst_1)))))) -> (Iff (Eq.{succ u2} P (coeFn.{succ u2, succ u2} (Equiv.Perm.{succ u2} P) (fun (_x : Equiv.{succ u2, succ u2} P P) => P -> P) (Equiv.hasCoeToFun.{succ u2, succ u2} P P) (Equiv.pointReflection.{u1, u2} G P _inst_1 _inst_2 x) y) y) (Eq.{succ u2} P y x))
 but is expected to have type
-  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] {x : P} {y : P}, (Function.Injective.{succ u2, succ u2} G G (bit0.{u2} G (AddZeroClass.toAdd.{u2} G (AddMonoid.toAddZeroClass.{u2} G (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G _inst_1)))))) -> (Iff (Eq.{succ u1} ((fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => P) y) (FunLike.coe.{succ u1, succ u1, succ u1} (Equiv.Perm.{succ u1} P) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => P) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u1} P P) (Equiv.pointReflection.{u2, u1} G P _inst_1 _inst_2 x) y) y) (Eq.{succ u1} P y x))
+  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_1 : AddGroup.{u2} G] [_inst_2 : AddTorsor.{u2, u1} G P _inst_1] {x : P} {y : P}, (Function.Injective.{succ u2, succ u2} G G (bit0.{u2} G (AddZeroClass.toAdd.{u2} G (AddMonoid.toAddZeroClass.{u2} G (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G _inst_1)))))) -> (Iff (Eq.{succ u1} ((fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => P) y) (FunLike.coe.{succ u1, succ u1, succ u1} (Equiv.Perm.{succ u1} P) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => P) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u1} P P) (Equiv.pointReflection.{u2, u1} G P _inst_1 _inst_2 x) y) y) (Eq.{succ u1} P y x))
 Case conversion may be inaccurate. Consider using '#align equiv.point_reflection_fixed_iff_of_injective_bit0 Equiv.pointReflection_fixed_iff_of_injective_bit0ₓ'. -/
 /-- `x` is the only fixed point of `point_reflection x`. This lemma requires
 `x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument. -/
@@ -732,7 +732,7 @@ omit G
 lean 3 declaration is
   forall {G : Type.{u1}} {P : Type.{u2}} [_inst_3 : AddCommGroup.{u1} G] [_inst_4 : AddTorsor.{u1, u2} G P (AddCommGroup.toAddGroup.{u1} G _inst_3)], (Function.Injective.{succ u1, succ u1} G G (bit0.{u1} G (AddZeroClass.toHasAdd.{u1} G (AddMonoid.toAddZeroClass.{u1} G (SubNegMonoid.toAddMonoid.{u1} G (AddGroup.toSubNegMonoid.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_3))))))) -> (forall (y : P), Function.Injective.{succ u2, succ u2} P P (fun (x : P) => coeFn.{succ u2, succ u2} (Equiv.Perm.{succ u2} P) (fun (_x : Equiv.{succ u2, succ u2} P P) => P -> P) (Equiv.hasCoeToFun.{succ u2, succ u2} P P) (Equiv.pointReflection.{u1, u2} G P (AddCommGroup.toAddGroup.{u1} G _inst_3) _inst_4 x) y))
 but is expected to have type
-  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_3 : AddCommGroup.{u2} G] [_inst_4 : AddTorsor.{u2, u1} G P (AddCommGroup.toAddGroup.{u2} G _inst_3)], (Function.Injective.{succ u2, succ u2} G G (bit0.{u2} G (AddZeroClass.toAdd.{u2} G (AddMonoid.toAddZeroClass.{u2} G (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G (AddCommGroup.toAddGroup.{u2} G _inst_3))))))) -> (forall (y : P), Function.Injective.{succ u1, succ u1} P ((fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => P) y) (fun (x : P) => FunLike.coe.{succ u1, succ u1, succ u1} (Equiv.Perm.{succ u1} P) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.805 : P) => P) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u1} P P) (Equiv.pointReflection.{u2, u1} G P (AddCommGroup.toAddGroup.{u2} G _inst_3) _inst_4 x) y))
+  forall {G : Type.{u2}} {P : Type.{u1}} [_inst_3 : AddCommGroup.{u2} G] [_inst_4 : AddTorsor.{u2, u1} G P (AddCommGroup.toAddGroup.{u2} G _inst_3)], (Function.Injective.{succ u2, succ u2} G G (bit0.{u2} G (AddZeroClass.toAdd.{u2} G (AddMonoid.toAddZeroClass.{u2} G (SubNegMonoid.toAddMonoid.{u2} G (AddGroup.toSubNegMonoid.{u2} G (AddCommGroup.toAddGroup.{u2} G _inst_3))))))) -> (forall (y : P), Function.Injective.{succ u1, succ u1} P ((fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => P) y) (fun (x : P) => FunLike.coe.{succ u1, succ u1, succ u1} (Equiv.Perm.{succ u1} P) P (fun (_x : P) => (fun (x._@.Mathlib.Logic.Equiv.Defs._hyg.808 : P) => P) _x) (Equiv.instFunLikeEquiv.{succ u1, succ u1} P P) (Equiv.pointReflection.{u2, u1} G P (AddCommGroup.toAddGroup.{u2} G _inst_3) _inst_4 x) y))
 Case conversion may be inaccurate. Consider using '#align equiv.injective_point_reflection_left_of_injective_bit0 Equiv.injective_pointReflection_left_of_injective_bit0ₓ'. -/
 theorem injective_pointReflection_left_of_injective_bit0 {G P : Type _} [AddCommGroup G]
     [AddTorsor G P] (h : Injective (bit0 : G → G)) (y : P) :