bump to nightly-2023-05-24-06

mathlib commit leanprover-community/mathlib@8d33f09
leanprover-community · May 24, 2023 · fbc7b47 · fbc7b47
1 parent b22bf34
commit fbc7b47
Show file tree

Hide file tree

Showing 401 changed files with 3,351 additions and 3,157 deletions.
diff --git a/Mathbin/Algebra/Algebra/Basic.lean b/Mathbin/Algebra/Algebra/Basic.lean
diff --git a/Mathbin/Algebra/Algebra/Bilinear.lean b/Mathbin/Algebra/Algebra/Bilinear.lean
diff --git a/Mathbin/Algebra/Algebra/Equiv.lean b/Mathbin/Algebra/Algebra/Equiv.lean
diff --git a/Mathbin/Algebra/Algebra/Hom.lean b/Mathbin/Algebra/Algebra/Hom.lean
diff --git a/Mathbin/Algebra/Algebra/Prod.lean b/Mathbin/Algebra/Algebra/Prod.lean
diff --git a/Mathbin/Algebra/Algebra/RestrictScalars.lean b/Mathbin/Algebra/Algebra/RestrictScalars.lean
diff --git a/Mathbin/Algebra/Algebra/Subalgebra/Basic.lean b/Mathbin/Algebra/Algebra/Subalgebra/Basic.lean
diff --git a/Mathbin/Algebra/Algebra/Tower.lean b/Mathbin/Algebra/Algebra/Tower.lean
diff --git a/Mathbin/Algebra/Algebra/Unitization.lean b/Mathbin/Algebra/Algebra/Unitization.lean
diff --git a/Mathbin/Algebra/Category/Group/Biproducts.lean b/Mathbin/Algebra/Category/Group/Biproducts.lean
@@ -56,7 +56,7 @@ def binaryProductLimitCone (G H : AddCommGroupCat.{u}) : Limits.LimitCone (pair
           · ext x
             simp
       uniq := fun s m w => by
-        ext <;> [rw [← w ⟨walking_pair.left⟩], rw [← w ⟨walking_pair.right⟩]] <;> rfl }
+        ext <;> [rw [← w ⟨walking_pair.left⟩];rw [← w ⟨walking_pair.right⟩]] <;> rfl }
 #align AddCommGroup.binary_product_limit_cone AddCommGroupCat.binaryProductLimitCone
 
 @[simp]

diff --git a/Mathbin/Algebra/Category/Module/Basic.lean b/Mathbin/Algebra/Category/Module/Basic.lean
diff --git a/Mathbin/Algebra/Category/Module/Biproducts.lean b/Mathbin/Algebra/Category/Module/Biproducts.lean
@@ -60,7 +60,7 @@ def binaryProductLimitCone (M N : ModuleCat.{v} R) : Limits.LimitCone (pair M N)
               Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply, LinearMap.prod_apply,
               Pi.prod]
       uniq := fun s m w => by
-        ext <;> [rw [← w ⟨walking_pair.left⟩], rw [← w ⟨walking_pair.right⟩]] <;> rfl }
+        ext <;> [rw [← w ⟨walking_pair.left⟩];rw [← w ⟨walking_pair.right⟩]] <;> rfl }
 #align Module.binary_product_limit_cone ModuleCat.binaryProductLimitCone
 
 @[simp]

diff --git a/Mathbin/Algebra/CharP/Basic.lean b/Mathbin/Algebra/CharP/Basic.lean
@@ -204,10 +204,10 @@ theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a
   by
   rcases lt_trichotomy a 0 with (h | rfl | h)
   · rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
-    lift -a to ℕ using neg_nonneg.mpr (le_of_lt h)
+    lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b
     rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
   · simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
-  · lift a to ℕ using le_of_lt h
+  · lift a to ℕ using le_of_lt h with b
     rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
 #align char_p.int_cast_eq_zero_iff CharP.int_cast_eq_zero_iff
 

diff --git a/Mathbin/Algebra/DirectSum/Finsupp.lean b/Mathbin/Algebra/DirectSum/Finsupp.lean
diff --git a/Mathbin/Algebra/DirectSum/Internal.lean b/Mathbin/Algebra/DirectSum/Internal.lean
diff --git a/Mathbin/Algebra/DirectSum/Module.lean b/Mathbin/Algebra/DirectSum/Module.lean
diff --git a/Mathbin/Algebra/DualNumber.lean b/Mathbin/Algebra/DualNumber.lean
diff --git a/Mathbin/Algebra/DualQuaternion.lean b/Mathbin/Algebra/DualQuaternion.lean
diff --git a/Mathbin/Algebra/EuclideanDomain/Basic.lean b/Mathbin/Algebra/EuclideanDomain/Basic.lean
@@ -242,7 +242,7 @@ theorem gcd_zero_right (a : R) : gcd a 0 = a :=
 theorem gcd_val (a b : R) : gcd a b = gcd (b % a) a :=
   by
   rw [gcd]
-  split_ifs <;> [simp only [h, mod_zero, gcd_zero_right], rfl]
+  split_ifs <;> [simp only [h, mod_zero, gcd_zero_right];rfl]
 #align euclidean_domain.gcd_val EuclideanDomain.gcd_val
 -/
 

diff --git a/Mathbin/Algebra/FreeAlgebra.lean b/Mathbin/Algebra/FreeAlgebra.lean
diff --git a/Mathbin/Algebra/GcdMonoid/Basic.lean b/Mathbin/Algebra/GcdMonoid/Basic.lean
@@ -1138,7 +1138,7 @@ theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b
       have : Associated (a * b) 0 :=
         (gcd_mul_lcm a b).symm.trans <| by rw [h, MulZeroClass.mul_zero]
       simpa only [associated_zero_iff_eq_zero, mul_eq_zero] )
-    (by rintro (rfl | rfl) <;> [apply lcm_zero_left, apply lcm_zero_right])
+    (by rintro (rfl | rfl) <;> [apply lcm_zero_left;apply lcm_zero_right])
 #align lcm_eq_zero_iff lcm_eq_zero_iff
 
 /- warning: normalize_lcm -> normalize_lcm is a dubious translation:

diff --git a/Mathbin/Algebra/GroupPower/Basic.lean b/Mathbin/Algebra/GroupPower/Basic.lean
@@ -141,8 +141,9 @@ but is expected to have type
 Case conversion may be inaccurate. Consider using '#align pow_add pow_addₓ'. -/
 @[to_additive add_nsmul]
 theorem pow_add (a : M) (m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n := by
-  induction' n with n ih <;> [rw [Nat.add_zero, pow_zero, mul_one],
-    rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', Nat.add_assoc]]
+  induction' n with n ih <;>
+    [rw [Nat.add_zero, pow_zero,
+      mul_one];rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', Nat.add_assoc]]
 #align pow_add pow_add
 #align add_nsmul add_nsmul
 
@@ -166,7 +167,7 @@ Case conversion may be inaccurate. Consider using '#align one_pow one_powₓ'. -
 -- the attributes are intentionally out of order. `smul_zero` proves `nsmul_zero`.
 @[to_additive nsmul_zero, simp]
 theorem one_pow (n : ℕ) : (1 : M) ^ n = 1 := by
-  induction' n with n ih <;> [exact pow_zero _, rw [pow_succ, ih, one_mul]]
+  induction' n with n ih <;> [exact pow_zero _;rw [pow_succ, ih, one_mul]]
 #align one_pow one_pow
 #align nsmul_zero nsmul_zero
 

diff --git a/Mathbin/Algebra/GroupPower/Lemmas.lean b/Mathbin/Algebra/GroupPower/Lemmas.lean
@@ -711,7 +711,7 @@ theorem abs_zsmul (n : ℤ) (a : α) : |n • a| = |n| • |a| :=
   obtain n0 | n0 := le_total 0 n
   · lift n to ℕ using n0
     simp only [abs_nsmul, abs_coe_nat, coe_nat_zsmul]
-  · lift -n to ℕ using neg_nonneg.2 n0
+  · lift -n to ℕ using neg_nonneg.2 n0 with m h
     rw [← abs_neg (n • a), ← neg_zsmul, ← abs_neg n, ← h, coe_nat_zsmul, abs_coe_nat, coe_nat_zsmul]
     exact abs_nsmul m _
 #align abs_zsmul abs_zsmul
@@ -762,8 +762,9 @@ theorem WithBot.coe_nsmul [AddMonoid A] (a : A) (n : ℕ) : ((n • a : A) : Wit
 -/
 
 theorem nsmul_eq_mul' [NonAssocSemiring R] (a : R) (n : ℕ) : n • a = a * n := by
-  induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, MulZeroClass.mul_zero],
-    rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]]
+  induction' n with n ih <;>
+    [rw [zero_nsmul, Nat.cast_zero,
+      MulZeroClass.mul_zero];rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]]
 #align nsmul_eq_mul' nsmul_eq_mul'ₓ
 
 @[simp]
@@ -820,7 +821,7 @@ but is expected to have type
 Case conversion may be inaccurate. Consider using '#align int.coe_nat_pow Int.coe_nat_powₓ'. -/
 @[simp, norm_cast]
 theorem Int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m := by
-  induction' m with m ih <;> [exact Int.ofNat_one, rw [pow_succ', pow_succ', Int.ofNat_mul, ih]]
+  induction' m with m ih <;> [exact Int.ofNat_one;rw [pow_succ', pow_succ', Int.ofNat_mul, ih]]
 #align int.coe_nat_pow Int.coe_nat_pow
 
 /- warning: int.nat_abs_pow -> Int.natAbs_pow is a dubious translation:
@@ -830,7 +831,7 @@ but is expected to have type
   forall (n : Int) (k : Nat), Eq.{1} Nat (Int.natAbs (HPow.hPow.{0, 0, 0} Int Nat Int Int.instHPowIntNat n k)) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) (Int.natAbs n) k)
 Case conversion may be inaccurate. Consider using '#align int.nat_abs_pow Int.natAbs_powₓ'. -/
 theorem Int.natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k := by
-  induction' k with k ih <;> [rfl, rw [pow_succ', Int.natAbs_mul, pow_succ', ih]]
+  induction' k with k ih <;> [rfl;rw [pow_succ', Int.natAbs_mul, pow_succ', ih]]
 #align int.nat_abs_pow Int.natAbs_pow
 
 /- warning: bit0_mul -> bit0_mul is a dubious translation:

diff --git a/Mathbin/Algebra/GroupRingAction/Invariant.lean b/Mathbin/Algebra/GroupRingAction/Invariant.lean
diff --git a/Mathbin/Algebra/GroupWithZero/Basic.lean b/Mathbin/Algebra/GroupWithZero/Basic.lean
@@ -300,7 +300,7 @@ but is expected to have type
 Case conversion may be inaccurate. Consider using '#align mul_eq_mul_right_iff mul_eq_mul_right_iffₓ'. -/
 @[simp]
 theorem mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0 := by
-  by_cases hc : c = 0 <;> [simp [hc], simp [mul_left_inj', hc]]
+  by_cases hc : c = 0 <;> [simp [hc];simp [mul_left_inj', hc]]
 #align mul_eq_mul_right_iff mul_eq_mul_right_iff
 
 /- warning: mul_eq_mul_left_iff -> mul_eq_mul_left_iff is a dubious translation:
@@ -311,7 +311,7 @@ but is expected to have type
 Case conversion may be inaccurate. Consider using '#align mul_eq_mul_left_iff mul_eq_mul_left_iffₓ'. -/
 @[simp]
 theorem mul_eq_mul_left_iff : a * b = a * c ↔ b = c ∨ a = 0 := by
-  by_cases ha : a = 0 <;> [simp [ha], simp [mul_right_inj', ha]]
+  by_cases ha : a = 0 <;> [simp [ha];simp [mul_right_inj', ha]]
 #align mul_eq_mul_left_iff mul_eq_mul_left_iff
 
 /- warning: mul_right_eq_self₀ -> mul_right_eq_self₀ is a dubious translation: