bump to nightly-2023-03-15-18

mathlib commit leanprover-community/mathlib@1a313d8

Mathbin/Algebra/Group/Basic.lean

@@ -424,6 +424,12 @@ theorem inv_inj {a b : G} : a⁻¹ = b⁻¹ ↔ a = b :=
 #align inv_inj inv_inj
 #align neg_inj neg_inj
 
+/- warning: inv_eq_iff_eq_inv -> inv_eq_iff_eq_inv is a dubious translation:
+lean 3 declaration is
+  forall {G : Type.{u1}} [_inst_1 : InvolutiveInv.{u1} G] {a : G} {b : G}, Iff (Eq.{succ u1} G (Inv.inv.{u1} G (InvolutiveInv.toHasInv.{u1} G _inst_1) a) b) (Eq.{succ u1} G a (Inv.inv.{u1} G (InvolutiveInv.toHasInv.{u1} G _inst_1) b))
+but is expected to have type
+  forall {G : Type.{u1}} [_inst_1 : InvolutiveInv.{u1} G] {a : G} {b : G}, Iff (Eq.{succ u1} G (Inv.inv.{u1} G (InvolutiveInv.toInv.{u1} G _inst_1) a) b) (Eq.{succ u1} G a (Inv.inv.{u1} G (InvolutiveInv.toInv.{u1} G _inst_1) b))
+Case conversion may be inaccurate. Consider using '#align inv_eq_iff_eq_inv inv_eq_iff_eq_invₓ'. -/
 @[to_additive]
 theorem inv_eq_iff_eq_inv : a⁻¹ = b ↔ a = b⁻¹ :=
   ⟨fun h => h ▸ (inv_inv a).symm, fun h => h.symm ▸ inv_inv b⟩
@@ -1112,7 +1118,7 @@ theorem div_eq_inv_self : a / b = b⁻¹ ↔ a = 1 := by rw [div_eq_mul_inv, mul
 lean 3 declaration is
   forall {G : Type.{u1}} [_inst_1 : Group.{u1} G] (a : G), Function.Surjective.{succ u1, succ u1} G 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_1))))) a)
 but is expected to have type
-  forall {G : Type.{u1}} [_inst_1 : Group.{u1} G] (a : G), Function.Surjective.{succ u1, succ u1} G G ((fun (x._@.Mathlib.Algebra.Group.Basic._hyg.3540 : G) (x._@.Mathlib.Algebra.Group.Basic._hyg.3542 : 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_1))))) x._@.Mathlib.Algebra.Group.Basic._hyg.3540 x._@.Mathlib.Algebra.Group.Basic._hyg.3542) a)
+  forall {G : Type.{u1}} [_inst_1 : Group.{u1} G] (a : G), Function.Surjective.{succ u1, succ u1} G G ((fun (x._@.Mathlib.Algebra.Group.Basic._hyg.3497 : G) (x._@.Mathlib.Algebra.Group.Basic._hyg.3499 : 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_1))))) x._@.Mathlib.Algebra.Group.Basic._hyg.3497 x._@.Mathlib.Algebra.Group.Basic._hyg.3499) a)
 Case conversion may be inaccurate. Consider using '#align mul_left_surjective mul_left_surjectiveₓ'. -/
 @[to_additive]
 theorem mul_left_surjective (a : G) : Function.Surjective ((· * ·) a) := fun x =>

Mathbin/Algebra/Periodic.lean

@@ -900,7 +900,7 @@ theorem Antiperiodic.sub_const [AddCommGroup α] [Neg β] (h : Antiperiodic f c)
 lean 3 declaration is
   forall {α : Type.{u1}} {β : Type.{u2}} {γ : Type.{u3}} {f : α -> β} {c : α} [_inst_1 : Add.{u1} α] [_inst_2 : Monoid.{u3} γ] [_inst_3 : AddGroup.{u2} β] [_inst_4 : DistribMulAction.{u3, u2} γ β _inst_2 (SubNegMonoid.toAddMonoid.{u2} β (AddGroup.toSubNegMonoid.{u2} β _inst_3))], (Function.Antiperiodic.{u1, u2} α β _inst_1 (SubNegMonoid.toHasNeg.{u2} β (AddGroup.toSubNegMonoid.{u2} β _inst_3)) f c) -> (forall (a : γ), Function.Antiperiodic.{u1, u2} α β _inst_1 (SubNegMonoid.toHasNeg.{u2} β (AddGroup.toSubNegMonoid.{u2} β _inst_3)) (SMul.smul.{u3, max u1 u2} γ (α -> β) (Function.hasSMul.{u1, u3, u2} α γ β (SMulZeroClass.toHasSmul.{u3, u2} γ β (AddZeroClass.toHasZero.{u2} β (AddMonoid.toAddZeroClass.{u2} β (SubNegMonoid.toAddMonoid.{u2} β (AddGroup.toSubNegMonoid.{u2} β _inst_3)))) (DistribSMul.toSmulZeroClass.{u3, u2} γ β (AddMonoid.toAddZeroClass.{u2} β (SubNegMonoid.toAddMonoid.{u2} β (AddGroup.toSubNegMonoid.{u2} β _inst_3))) (DistribMulAction.toDistribSMul.{u3, u2} γ β _inst_2 (SubNegMonoid.toAddMonoid.{u2} β (AddGroup.toSubNegMonoid.{u2} β _inst_3)) _inst_4)))) a f) c)
 but is expected to have type
-  forall {α : Type.{u3}} {β : Type.{u1}} {γ : Type.{u2}} {f : α -> β} {c : α} [_inst_1 : Add.{u3} α] [_inst_2 : Monoid.{u2} γ] [_inst_3 : AddGroup.{u1} β] [_inst_4 : DistribMulAction.{u2, u1} γ β _inst_2 (SubNegMonoid.toAddMonoid.{u1} β (AddGroup.toSubNegMonoid.{u1} β _inst_3))], (Function.Antiperiodic.{u3, u1} α β _inst_1 (NegZeroClass.toNeg.{u1} β (SubNegZeroMonoid.toNegZeroClass.{u1} β (SubtractionMonoid.toSubNegZeroMonoid.{u1} β (AddGroup.toSubtractionMonoid.{u1} β _inst_3)))) f c) -> (forall (a : γ), Function.Antiperiodic.{u3, u1} α β _inst_1 (NegZeroClass.toNeg.{u1} β (SubNegZeroMonoid.toNegZeroClass.{u1} β (SubtractionMonoid.toSubNegZeroMonoid.{u1} β (AddGroup.toSubtractionMonoid.{u1} β _inst_3)))) (HSMul.hSMul.{u2, max u3 u1, max u3 u1} γ (α -> β) (α -> β) (instHSMul.{u2, max u3 u1} γ (α -> β) (Pi.instSMul.{u3, u1, u2} α γ (fun (a._@.Mathlib.Algebra.Periodic._hyg.4890 : α) => β) (fun (i : α) => SMulZeroClass.toSMul.{u2, u1} γ β (NegZeroClass.toZero.{u1} β (SubNegZeroMonoid.toNegZeroClass.{u1} β (SubtractionMonoid.toSubNegZeroMonoid.{u1} β (AddGroup.toSubtractionMonoid.{u1} β _inst_3)))) (DistribSMul.toSMulZeroClass.{u2, u1} γ β (AddMonoid.toAddZeroClass.{u1} β (SubNegMonoid.toAddMonoid.{u1} β (AddGroup.toSubNegMonoid.{u1} β _inst_3))) (DistribMulAction.toDistribSMul.{u2, u1} γ β _inst_2 (SubNegMonoid.toAddMonoid.{u1} β (AddGroup.toSubNegMonoid.{u1} β _inst_3)) _inst_4))))) a f) c)
+  forall {α : Type.{u3}} {β : Type.{u1}} {γ : Type.{u2}} {f : α -> β} {c : α} [_inst_1 : Add.{u3} α] [_inst_2 : Monoid.{u2} γ] [_inst_3 : AddGroup.{u1} β] [_inst_4 : DistribMulAction.{u2, u1} γ β _inst_2 (SubNegMonoid.toAddMonoid.{u1} β (AddGroup.toSubNegMonoid.{u1} β _inst_3))], (Function.Antiperiodic.{u3, u1} α β _inst_1 (NegZeroClass.toNeg.{u1} β (SubNegZeroMonoid.toNegZeroClass.{u1} β (SubtractionMonoid.toSubNegZeroMonoid.{u1} β (AddGroup.toSubtractionMonoid.{u1} β _inst_3)))) f c) -> (forall (a : γ), Function.Antiperiodic.{u3, u1} α β _inst_1 (NegZeroClass.toNeg.{u1} β (SubNegZeroMonoid.toNegZeroClass.{u1} β (SubtractionMonoid.toSubNegZeroMonoid.{u1} β (AddGroup.toSubtractionMonoid.{u1} β _inst_3)))) (HSMul.hSMul.{u2, max u3 u1, max u3 u1} γ (α -> β) (α -> β) (instHSMul.{u2, max u3 u1} γ (α -> β) (Pi.instSMul.{u3, u1, u2} α γ (fun (a._@.Mathlib.Algebra.Periodic._hyg.4884 : α) => β) (fun (i : α) => SMulZeroClass.toSMul.{u2, u1} γ β (NegZeroClass.toZero.{u1} β (SubNegZeroMonoid.toNegZeroClass.{u1} β (SubtractionMonoid.toSubNegZeroMonoid.{u1} β (AddGroup.toSubtractionMonoid.{u1} β _inst_3)))) (DistribSMul.toSMulZeroClass.{u2, u1} γ β (AddMonoid.toAddZeroClass.{u1} β (SubNegMonoid.toAddMonoid.{u1} β (AddGroup.toSubNegMonoid.{u1} β _inst_3))) (DistribMulAction.toDistribSMul.{u2, u1} γ β _inst_2 (SubNegMonoid.toAddMonoid.{u1} β (AddGroup.toSubNegMonoid.{u1} β _inst_3)) _inst_4))))) a f) c)
 Case conversion may be inaccurate. Consider using '#align function.antiperiodic.smul Function.Antiperiodic.smulₓ'. -/
 protected theorem Antiperiodic.smul [Add α] [Monoid γ] [AddGroup β] [DistribMulAction γ β]
     (h : Antiperiodic f c) (a : γ) : Antiperiodic (a • f) c := by simp_all

Mathbin/Analysis/Complex/RootsOfUnity.lean

@@ -140,7 +140,7 @@ theorem IsPrimitiveRoot.arg {n : ℕ} {ζ : ℂ} (h : IsPrimitiveRoot ζ n) (hn
   by
   rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
   obtain ⟨i, h, hin, rfl⟩ := h
-  rw [mul_comm, ← mul_assoc, Complex.exp_mul_i]
+  rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
   refine' ⟨if i * 2 ≤ n then i else i - n, _, _, _⟩
   on_goal 2 =>
     replace hin := nat.is_coprime_iff_coprime.mpr hin

Mathbin/Analysis/SpecialFunctions/Complex/Arg.lean

@@ -86,7 +86,7 @@ theorem abs_eq_one_iff (z : ℂ) : abs z = 1 ↔ ∃ θ : ℝ, exp (θ * I) = z
       _ = z := abs_mul_exp_arg_mul_I z
 
   · rintro ⟨θ, rfl⟩
-    exact Complex.abs_exp_of_real_mul_i θ
+    exact Complex.abs_exp_ofReal_mul_I θ
 #align complex.abs_eq_one_iff Complex.abs_eq_one_iff
 
 @[simp]

Mathbin/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -126,7 +126,7 @@ theorem Real.Angle.expMapCircle_coe (x : ℝ) : Real.Angle.expMapCircle x = expM
 theorem Real.Angle.coe_expMapCircle (θ : Real.Angle) : (θ.expMapCircle : ℂ) = θ.cos + θ.sin * I :=
   by
   induction θ using Real.Angle.induction_on
-  simp [Complex.exp_mul_i]
+  simp [Complex.exp_mul_I]
 #align real.angle.coe_exp_map_circle Real.Angle.coe_expMapCircle
 
 @[simp]

Mathbin/Analysis/SpecialFunctions/Gamma.lean

@@ -1792,7 +1792,7 @@ theorem gammaSeq_tendsto_gamma (s : ℝ) : Tendsto (gammaSeq s) atTop (𝓝 <| g
 /-- Euler's reflection formula for the real Gamma function. -/
 theorem gamma_mul_gamma_one_sub (s : ℝ) : gamma s * gamma (1 - s) = π / sin (π * s) :=
   by
-  simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.of_real_sin, Complex.ofReal_mul, ←
+  simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.ofReal_sin, Complex.ofReal_mul, ←
     Complex.gamma_of_real, Complex.ofReal_sub, Complex.ofReal_one]
   exact Complex.gamma_mul_gamma_one_sub s
 #align real.Gamma_mul_Gamma_one_sub Real.gamma_mul_gamma_one_sub

Mathbin/Analysis/SpecialFunctions/PolarCoord.lean

@@ -67,8 +67,8 @@ def polarCoord : LocalHomeomorph (ℝ × ℝ) (ℝ × ℝ)
       congr 1
       ring
     · convert Complex.arg_mul_cos_add_sin_mul_i hr ⟨hθ.1, hθ.2.le⟩
-      simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.of_real_cos,
-        Complex.of_real_sin]
+      simp only [Complex.equivRealProd_symm_apply, Complex.ofReal_mul, Complex.ofReal_cos,
+        Complex.ofReal_sin]
       ring
   left_inv' := by
     rintro ⟨x, y⟩ hxy
@@ -77,9 +77,9 @@ def polarCoord : LocalHomeomorph (ℝ × ℝ) (ℝ × ℝ)
         Complex.ofReal_re, Complex.mul_re, Complex.I_re, MulZeroClass.mul_zero, Complex.ofReal_im,
         Complex.I_im, sub_self, add_zero, Complex.add_im, Complex.mul_im, mul_one, zero_add]
     have Z := Complex.abs_mul_cos_add_sin_mul_i (x + y * Complex.I)
-    simp only [← Complex.of_real_cos, ← Complex.of_real_sin, mul_add, ← Complex.ofReal_mul, ←
+    simp only [← Complex.ofReal_cos, ← Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ←
       mul_assoc] at Z
-    simpa [A, -Complex.of_real_cos, -Complex.of_real_sin] using Complex.ext_iff.1 Z
+    simpa [A, -Complex.ofReal_cos, -Complex.ofReal_sin] using Complex.ext_iff.1 Z
   open_target := isOpen_Ioi.Prod isOpen_Ioo
   open_source :=
     (isOpen_lt continuous_const continuous_fst).union

Mathbin/Analysis/SpecialFunctions/Pow.lean

@@ -362,7 +362,7 @@ theorem rpow_def_of_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
     x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) := by
   simp only [rpow_def, Complex.cpow_def] <;> split_ifs <;>
     simp_all [(Complex.of_real_log hx).symm, -Complex.ofReal_mul, -IsROrC.of_real_mul,
-      (Complex.ofReal_mul _ _).symm, Complex.exp_of_real_re]
+      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re]
 #align real.rpow_def_of_nonneg Real.rpow_def_of_nonneg
 
 theorem rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : x ^ y = exp (log x * y) := by
@@ -392,8 +392,8 @@ theorem rpow_def_of_neg {x : ℝ} (hx : x < 0) (y : ℝ) : x ^ y = exp (log x *
     simp only [Complex.log, abs_of_neg hx, Complex.arg_of_real_of_neg hx, Complex.abs_ofReal,
       Complex.ofReal_mul]
     ring
-  · rw [this, Complex.exp_add_mul_i, ← Complex.of_real_exp, ← Complex.of_real_cos, ←
-      Complex.of_real_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
+  · rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
+      Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
       Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im,
       Real.log_neg_eq_log]
     ring

Mathbin/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

@@ -32,7 +32,7 @@ theorem tan_add {x y : ℝ}
         (∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y = (2 * l + 1) * π / 2) :
     tan (x + y) = (tan x + tan y) / (1 - tan x * tan y) := by
   simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div,
-    Complex.ofReal_mul, Complex.of_real_tan] using
+    Complex.ofReal_mul, Complex.ofReal_tan] using
     @Complex.tan_add (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)
 #align real.tan_add Real.tan_add
 
@@ -44,12 +44,12 @@ theorem tan_add' {x y : ℝ}
 
 theorem tan_two_mul {x : ℝ} : tan (2 * x) = 2 * tan x / (1 - tan x ^ 2) := by
   simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_div, Complex.ofReal_pow,
-    Complex.ofReal_mul, Complex.of_real_tan, Complex.ofReal_bit0, Complex.ofReal_one] using
+    Complex.ofReal_mul, Complex.ofReal_tan, Complex.ofReal_bit0, Complex.ofReal_one] using
     Complex.tan_two_mul
 #align real.tan_two_mul Real.tan_two_mul
 
 theorem tan_ne_zero_iff {θ : ℝ} : tan θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ k * π / 2 := by
-  rw [← Complex.ofReal_ne_zero, Complex.of_real_tan, Complex.tan_ne_zero_iff] <;> norm_cast
+  rw [← Complex.ofReal_ne_zero, Complex.ofReal_tan, Complex.tan_ne_zero_iff] <;> norm_cast
 #align real.tan_ne_zero_iff Real.tan_ne_zero_iff
 
 theorem tan_eq_zero_iff {θ : ℝ} : tan θ = 0 ↔ ∃ k : ℤ, θ = k * π / 2 := by

Mathbin/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean

@@ -38,7 +38,7 @@ theorem tendsto_abs_tan_of_cos_eq_zero {x : ℝ} (hx : cos x = 0) :
     Tendsto (fun x => abs (tan x)) (𝓝[≠] x) atTop :=
   by
   have hx : Complex.cos x = 0 := by exact_mod_cast hx
-  simp only [← Complex.abs_ofReal, Complex.of_real_tan]
+  simp only [← Complex.abs_ofReal, Complex.ofReal_tan]
   refine' (Complex.tendsto_abs_tan_of_cos_eq_zero hx).comp _
   refine' tendsto.inf complex.continuous_of_real.continuous_at _
   exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1

Mathbin/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean

@@ -114,8 +114,8 @@ theorem integral_sin_mul_sin_mul_cos_pow_eq (hn : 2 ≤ n) (hz : z ≠ 0) :
     have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
     convert ((Complex.hasDerivAt_sin x).mul c).comp_of_real using 1
     · ext1 y
-      simp only [Complex.of_real_sin, Complex.of_real_cos]
-    · simp only [Complex.of_real_cos, Complex.of_real_sin]
+      simp only [Complex.ofReal_sin, Complex.ofReal_cos]
+    · simp only [Complex.ofReal_cos, Complex.ofReal_sin]
       rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
       congr 1
       · rw [← pow_succ, Nat.sub_add_cancel (by linarith : 1 ≤ n)]
@@ -148,7 +148,7 @@ theorem integral_sin_mul_sin_mul_cos_pow_eq (hn : 2 ≤ n) (hz : z ≠ 0) :
     refine' integral_congr fun x hx => _
     dsimp only
     -- get rid of real trig functions and divions by 2 * z:
-    rw [Complex.of_real_cos, Complex.of_real_sin, Complex.sin_sq, ← mul_div_right_comm, ←
+    rw [Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq, ← mul_div_right_comm, ←
       mul_div_right_comm, ← sub_div, mul_div, ← neg_div]
     congr 1
     have : Complex.cos ↑x ^ n = Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2 := by
@@ -383,7 +383,7 @@ theorem Real.tendsto_euler_sin_prod (x : ℝ) :
     rw [Complex.ofReal_prod]
     refine' Finset.prod_congr (by rfl) fun n hn => _
     norm_cast
-  · rw [← Complex.ofReal_mul, ← Complex.of_real_sin, Complex.ofReal_re]
+  · rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]
 #align real.tendsto_euler_sin_prod Real.tendsto_euler_sin_prod
 
 end EulerSine