bump to nightly-2024-01-11-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/GroupPower/Lemmas.lean

@@ -589,15 +589,19 @@ theorem WithBot.coe_nsmul [AddMonoid A] (a : A) (n : ℕ) : ((n • a : A) : Wit
 #align with_bot.coe_nsmul WithBot.coe_nsmul
 -/
 
+#print nsmul_eq_mul' /-
 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]]
-#align nsmul_eq_mul' nsmul_eq_mul'ₓ
+#align nsmul_eq_mul' nsmul_eq_mul'
+-/
 
+#print nsmul_eq_mul /-
 @[simp]
 theorem nsmul_eq_mul [NonAssocSemiring R] (n : ℕ) (a : R) : n • a = n * a := by
   rw [nsmul_eq_mul', (n.cast_commute a).Eq]
-#align nsmul_eq_mul nsmul_eq_mulₓ
+#align nsmul_eq_mul nsmul_eq_mul
+-/
 
 #print NonUnitalNonAssocSemiring.nat_smulCommClass /-
 /-- Note that `add_comm_monoid.nat_smul_comm_class` requires stronger assumptions on `R`. -/
@@ -723,13 +727,15 @@ theorem zsmul_int_one (n : ℤ) : n • 1 = n := by simp
 #align zsmul_int_one zsmul_int_one
 -/
 
+#print Int.cast_pow /-
 @[simp, norm_cast]
 theorem Int.cast_pow [Ring R] (n : ℤ) (m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
   by
   induction' m with m ih
   · rw [pow_zero, pow_zero, Int.cast_one]
   · rw [pow_succ, pow_succ, Int.cast_mul, ih]
-#align int.cast_pow Int.cast_powₓ
+#align int.cast_pow Int.cast_pow
+-/
 
 #print neg_one_pow_eq_pow_mod_two /-
 theorem neg_one_pow_eq_pow_mod_two [Ring R] {n : ℕ} : (-1 : R) ^ n = (-1) ^ (n % 2) := by

Mathbin/Algebra/Order/LatticeGroup.lean

@@ -458,7 +458,7 @@ theorem sup_sq_eq_mul_mul_abs_div [CovariantClass α α (· * ·) (· ≤ ·)] (
   rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, ← mul_assoc, mul_comm, mul_assoc,
     ← pow_two, inv_mul_cancel_left]
 #align lattice_ordered_comm_group.sup_sq_eq_mul_mul_abs_div LatticeOrderedCommGroup.sup_sq_eq_mul_mul_abs_div
-#align lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub
+#align lattice_ordered_comm_group.two_sup_eq_add_add_abs_sub LatticeOrderedCommGroup.two_nsmul_sup_eq_add_add_abs_sub
 -/
 
 #print LatticeOrderedCommGroup.inf_sq_eq_mul_div_abs_div /-
@@ -469,7 +469,7 @@ theorem inf_sq_eq_mul_div_abs_div [CovariantClass α α (· * ·) (· ≤ ·)] (
   rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
     inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
 #align lattice_ordered_comm_group.inf_sq_eq_mul_div_abs_div LatticeOrderedCommGroup.inf_sq_eq_mul_div_abs_div
-#align lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub
+#align lattice_ordered_comm_group.two_inf_eq_add_sub_abs_sub LatticeOrderedCommGroup.two_nsmul_inf_eq_add_sub_abs_sub
 -/
 
 #print CommGroup.toDistribLattice /-

Mathbin/Algebra/Order/ToIntervalMod.lean

@@ -913,22 +913,22 @@ theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo :
 #align Ico_eq_locus_Ioc_eq_Union_Ioo Ico_eq_locus_Ioc_eq_iUnion_Ioo
 -/
 
-#print toIocDiv_wcovby_toIcoDiv /-
-theorem toIocDiv_wcovby_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b :=
+#print toIocDiv_wcovBy_toIcoDiv /-
+theorem toIocDiv_wcovBy_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b :=
   by
   suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
-    rwa [wcovby_iff_eq_or_covby, ← Order.succ_eq_iff_covby]
+    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]
   rw [eq_comm, ← not_modeq_iff_to_Ico_div_eq_to_Ioc_div, eq_comm, ←
     modeq_iff_to_Ico_div_eq_to_Ioc_div_add_one]
   exact em' _
-#align to_Ioc_div_wcovby_to_Ico_div toIocDiv_wcovby_toIcoDiv
+#align to_Ioc_div_wcovby_to_Ico_div toIocDiv_wcovBy_toIcoDiv
 -/
 
 #print toIcoMod_le_toIocMod /-
 theorem toIcoMod_le_toIocMod (a b : α) : toIcoMod hp a b ≤ toIocMod hp a b :=
   by
   rw [toIcoMod, toIocMod, sub_le_sub_iff_left]
-  exact zsmul_mono_left hp.le (toIocDiv_wcovby_toIcoDiv _ _ _).le
+  exact zsmul_mono_left hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le
 #align to_Ico_mod_le_to_Ioc_mod toIcoMod_le_toIocMod
 -/
 
@@ -937,7 +937,7 @@ theorem toIocMod_le_toIcoMod_add (a b : α) : toIocMod hp a b ≤ toIcoMod hp a
   by
   rw [toIcoMod, toIocMod, sub_add, sub_le_sub_iff_left, sub_le_iff_le_add, ← add_one_zsmul,
     (zsmul_strictMono_left hp).le_iff_le]
-  apply (toIocDiv_wcovby_toIcoDiv _ _ _).le_succ
+  apply (toIocDiv_wcovBy_toIcoDiv _ _ _).le_succ
 #align to_Ioc_mod_le_to_Ico_mod_add toIocMod_le_toIcoMod_add
 -/
 

Mathbin/Analysis/Calculus/ContDiffDef.lean

@@ -1057,8 +1057,8 @@ theorem iteratedFDerivWithin_one_apply (h : UniqueDiffWithinAt 𝕜 s x) (m : Fi
 #align iterated_fderiv_within_one_apply iteratedFDerivWithin_one_apply
 -/
 
-#print Filter.EventuallyEq.iterated_fderiv_within' /-
-theorem Filter.EventuallyEq.iterated_fderiv_within' (h : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) (n : ℕ) :
+#print Filter.EventuallyEq.iteratedFDerivWithin' /-
+theorem Filter.EventuallyEq.iteratedFDerivWithin' (h : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) (n : ℕ) :
     iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t :=
   by
   induction' n with n ihn
@@ -1067,13 +1067,13 @@ theorem Filter.EventuallyEq.iterated_fderiv_within' (h : f₁ =ᶠ[𝓝[s] x] f)
     apply this.mono
     intro y hy
     simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (· ∘ ·)]
-#align filter.eventually_eq.iterated_fderiv_within' Filter.EventuallyEq.iterated_fderiv_within'
+#align filter.eventually_eq.iterated_fderiv_within' Filter.EventuallyEq.iteratedFDerivWithin'
 -/
 
 #print Filter.EventuallyEq.iteratedFDerivWithin /-
 protected theorem Filter.EventuallyEq.iteratedFDerivWithin (h : f₁ =ᶠ[𝓝[s] x] f) (n : ℕ) :
     iteratedFDerivWithin 𝕜 n f₁ s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s :=
-  h.iterated_fderiv_within' Subset.rfl n
+  h.iteratedFDerivWithin' Subset.rfl n
 #align filter.eventually_eq.iterated_fderiv_within Filter.EventuallyEq.iteratedFDerivWithin
 -/
 
@@ -1083,7 +1083,7 @@ iterated differentials within this set at `x` coincide. -/
 theorem Filter.EventuallyEq.iteratedFDerivWithin_eq (h : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x)
     (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x :=
   have : f₁ =ᶠ[𝓝[insert x s] x] f := by simpa [eventually_eq, hx]
-  (this.iterated_fderiv_within' (subset_insert _ _) n).self_of_nhdsWithin (mem_insert _ _)
+  (this.iteratedFDerivWithin' (subset_insert _ _) n).self_of_nhdsWithin (mem_insert _ _)
 #align filter.eventually_eq.iterated_fderiv_within_eq Filter.EventuallyEq.iteratedFDerivWithin_eq
 -/
 
@@ -1379,8 +1379,8 @@ theorem contDiffOn_succ_iff_fderivWithin {n : ℕ} (hs : UniqueDiffOn 𝕜 s) :
 #align cont_diff_on_succ_iff_fderiv_within contDiffOn_succ_iff_fderivWithin
 -/
 
-#print contDiffOn_succ_iff_has_fderiv_within /-
-theorem contDiffOn_succ_iff_has_fderiv_within {n : ℕ} (hs : UniqueDiffOn 𝕜 s) :
+#print contDiffOn_succ_iff_hasFDerivWithin /-
+theorem contDiffOn_succ_iff_hasFDerivWithin {n : ℕ} (hs : UniqueDiffOn 𝕜 s) :
     ContDiffOn 𝕜 (n + 1 : ℕ) f s ↔
       ∃ f' : E → E →L[𝕜] F, ContDiffOn 𝕜 n f' s ∧ ∀ x, x ∈ s → HasFDerivWithinAt f (f' x) s x :=
   by
@@ -1389,7 +1389,7 @@ theorem contDiffOn_succ_iff_has_fderiv_within {n : ℕ} (hs : UniqueDiffOn 𝕜
   rcases h with ⟨f', h1, h2⟩
   refine' ⟨fun x hx => (h2 x hx).DifferentiableWithinAt, fun x hx => _⟩
   exact (h1 x hx).congr' (fun y hy => (h2 y hy).fderivWithin (hs y hy)) hx
-#align cont_diff_on_succ_iff_has_fderiv_within contDiffOn_succ_iff_has_fderiv_within
+#align cont_diff_on_succ_iff_has_fderiv_within contDiffOn_succ_iff_hasFDerivWithin
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]] -/
@@ -1844,15 +1844,15 @@ theorem contDiff_iff_forall_nat_le : ContDiff 𝕜 n f ↔ ∀ m : ℕ, ↑m ≤
 #align cont_diff_iff_forall_nat_le contDiff_iff_forall_nat_le
 -/
 
-#print contDiff_succ_iff_has_fderiv /-
+#print contDiff_succ_iff_hasFDerivAt /-
 /-- A function is `C^(n+1)` iff it has a `C^n` derivative. -/
-theorem contDiff_succ_iff_has_fderiv {n : ℕ} :
+theorem contDiff_succ_iff_hasFDerivAt {n : ℕ} :
     ContDiff 𝕜 (n + 1 : ℕ) f ↔
       ∃ f' : E → E →L[𝕜] F, ContDiff 𝕜 n f' ∧ ∀ x, HasFDerivAt f (f' x) x :=
   by
   simp only [← contDiffOn_univ, ← hasFDerivWithinAt_univ,
-    contDiffOn_succ_iff_has_fderiv_within uniqueDiffOn_univ, Set.mem_univ, forall_true_left]
-#align cont_diff_succ_iff_has_fderiv contDiff_succ_iff_has_fderiv
+    contDiffOn_succ_iff_hasFDerivWithin uniqueDiffOn_univ, Set.mem_univ, forall_true_left]
+#align cont_diff_succ_iff_has_fderiv contDiff_succ_iff_hasFDerivAt
 -/
 
 /-! ### Iterated derivative -/

Mathbin/Analysis/Calculus/Fderiv/Basic.lean

@@ -1204,20 +1204,20 @@ theorem Filter.EventuallyEq.fderivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx :
 #align filter.eventually_eq.fderiv_within_eq Filter.EventuallyEq.fderivWithin_eq
 -/
 
-#print Filter.EventuallyEq.fderiv_within' /-
-theorem Filter.EventuallyEq.fderiv_within' (hs : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) :
+#print Filter.EventuallyEq.fderivWithin' /-
+theorem Filter.EventuallyEq.fderivWithin' (hs : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) :
     fderivWithin 𝕜 f₁ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 f t :=
   (eventually_nhdsWithin_nhdsWithin.2 hs).mp <|
     eventually_mem_nhdsWithin.mono fun y hys hs =>
       Filter.EventuallyEq.fderivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht)
         (hs.self_of_nhdsWithin hys)
-#align filter.eventually_eq.fderiv_within' Filter.EventuallyEq.fderiv_within'
+#align filter.eventually_eq.fderiv_within' Filter.EventuallyEq.fderivWithin'
 -/
 
 #print Filter.EventuallyEq.fderivWithin /-
 protected theorem Filter.EventuallyEq.fderivWithin (hs : f₁ =ᶠ[𝓝[s] x] f) :
     fderivWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] fderivWithin 𝕜 f s :=
-  hs.fderiv_within' Subset.rfl
+  hs.fderivWithin' Subset.rfl
 #align filter.eventually_eq.fderiv_within Filter.EventuallyEq.fderivWithin
 -/
 

Mathbin/Analysis/Calculus/Taylor.lean

@@ -260,18 +260,18 @@ theorem taylorWithinEval_hasDerivAt_Ioo {f : ℝ → E} {a b t : ℝ} (x : ℝ)
 #align taylor_within_eval_has_deriv_at_Ioo taylorWithinEval_hasDerivAt_Ioo
 -/
 
-#print has_deriv_within_taylorWithinEval_at_Icc /-
+#print hasDerivWithinAt_taylorWithinEval_at_Icc /-
 /-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.
 
 Version for closed intervals -/
-theorem has_deriv_within_taylorWithinEval_at_Icc {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ}
+theorem hasDerivWithinAt_taylorWithinEval_at_Icc {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ}
     (hx : a < b) (ht : t ∈ Icc a b) (hf : ContDiffOn ℝ n f (Icc a b))
     (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)) :
     HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
       (((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a b) t :=
   hasDerivWithinAt_taylorWithinEval (uniqueDiffOn_Icc hx t ht) (uniqueDiffOn_Icc hx)
     self_mem_nhdsWithin ht rfl.Subset hf (hf' t ht)
-#align has_deriv_within_taylor_within_eval_at_Icc has_deriv_within_taylorWithinEval_at_Icc
+#align has_deriv_within_taylor_within_eval_at_Icc hasDerivWithinAt_taylorWithinEval_at_Icc
 -/
 
 /-! ### Taylor's theorem with mean value type remainder estimate -/
@@ -416,7 +416,7 @@ theorem taylor_mean_remainder_bound {f : ℝ → E} {a b C x : ℝ} {n : ℕ} (h
     by
     intro t ht
     have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
-    exact (has_deriv_within_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I
+    exact (hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I
   have := norm_image_sub_le_of_norm_deriv_le_segment' A h' x (right_mem_Icc.2 hx.1)
   simp only [taylorWithinEval_self] at this 
   refine' this.trans_eq _

Mathbin/Analysis/Convex/Cone/Proper.lean

@@ -110,17 +110,17 @@ theorem toConvexCone_eq_coe (K : ProperCone 𝕜 E) : K.toConvexCone = K :=
   rfl
 #align proper_cone.to_convex_cone_eq_coe ProperCone.toConvexCone_eq_coe
 
-#print ProperCone.ext' /-
-theorem ext' : Function.Injective (coe : ProperCone 𝕜 E → ConvexCone 𝕜 E) := fun S T h => by
-  cases S <;> cases T <;> congr
-#align proper_cone.ext' ProperCone.ext'
+#print ProperCone.toPointedCone_injective /-
+theorem toPointedCone_injective : Function.Injective (coe : ProperCone 𝕜 E → ConvexCone 𝕜 E) :=
+  fun S T h => by cases S <;> cases T <;> congr
+#align proper_cone.ext' ProperCone.toPointedCone_injective
 -/
 
 -- TODO: add convex_cone_class that extends set_like and replace the below instance
 instance : SetLike (ProperCone 𝕜 E) E
     where
   coe K := K.carrier
-  coe_injective' _ _ h := ProperCone.ext' (SetLike.coe_injective h)
+  coe_injective' _ _ h := ProperCone.toPointedCone_injective (SetLike.coe_injective h)
 
 #print ProperCone.ext /-
 @[ext]
@@ -230,7 +230,7 @@ theorem mem_map {f : E →L[ℝ] F} {K : ProperCone ℝ E} {y : F} :
 #print ProperCone.map_id /-
 @[simp]
 theorem map_id (K : ProperCone ℝ E) : K.map (ContinuousLinearMap.id ℝ E) = K :=
-  ProperCone.ext' <| by simpa using IsClosed.closure_eq K.is_closed
+  ProperCone.toPointedCone_injective <| by simpa using IsClosed.closure_eq K.is_closed
 #align proper_cone.map_id ProperCone.map_id
 -/
 
@@ -313,7 +313,7 @@ variable {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Complete
 /-- The dual of the dual of a proper cone is itself. -/
 @[simp]
 theorem dual_dual (K : ProperCone ℝ E) : K.dual.dual = K :=
-  ProperCone.ext' <|
+  ProperCone.toPointedCone_injective <|
     (K : ConvexCone ℝ E).innerDualCone_of_innerDualCone_eq_self K.Nonempty K.IsClosed
 #align proper_cone.dual_dual ProperCone.dual_dual
 -/

Mathbin/Analysis/Normed/Field/Basic.lean

@@ -787,19 +787,17 @@ instance (priority := 100) NormedDivisionRing.to_topologicalDivisionRing : Topol
 #align normed_division_ring.to_topological_division_ring NormedDivisionRing.to_topologicalDivisionRing
 -/
 
-#print norm_map_one_of_pow_eq_one /-
 theorem norm_map_one_of_pow_eq_one [Monoid β] (φ : β →* α) {x : β} {k : ℕ+} (h : x ^ (k : ℕ) = 1) :
     ‖φ x‖ = 1 :=
   by
   rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow]
   exacts [norm_nonneg _, zero_le_one, k.pos]
 #align norm_map_one_of_pow_eq_one norm_map_one_of_pow_eq_one
--/
 
-#print norm_one_of_pow_eq_one /-
-theorem norm_one_of_pow_eq_one {x : α} {k : ℕ+} (h : x ^ (k : ℕ) = 1) : ‖x‖ = 1 :=
+#print IsOfFinOrder.norm_eq_one /-
+theorem IsOfFinOrder.norm_eq_one {x : α} {k : ℕ+} (h : x ^ (k : ℕ) = 1) : ‖x‖ = 1 :=
   norm_map_one_of_pow_eq_one (MonoidHom.id α) h
-#align norm_one_of_pow_eq_one norm_one_of_pow_eq_one
+#align norm_one_of_pow_eq_one IsOfFinOrder.norm_eq_one
 -/
 
 end NormedDivisionRing

Mathbin/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -586,7 +586,7 @@ theorem Gamma_eq_integral {s : ℝ} (hs : 0 < s) : Gamma s = ∫ x in Ioi 0, exp
 theorem Gamma_add_one {s : ℝ} (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s :=
   by
   simp_rw [Gamma]
-  rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.ofReal_mul_re]
+  rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.re_ofReal_mul]
   rwa [Complex.ofReal_ne_zero]
 #align real.Gamma_add_one Real.Gamma_add_one
 -/

Mathbin/Analysis/SpecialFunctions/Integrals.lean

@@ -427,14 +427,14 @@ theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [a, b
     ∫ x in a..b, (x : ℂ) ^ (r : ℂ) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
     integral_cpow h'
   apply_fun Complex.re at this ; convert this
-  · simp_rw [interval_integral_eq_integral_uIoc, Complex.real_smul, Complex.ofReal_mul_re]
+  · simp_rw [interval_integral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul]
     · change Complex.re with IsROrC.re
       rw [← integral_re]; rfl
       refine' interval_integrable_iff.mp _
       cases h'
       · exact interval_integrable_cpow' h'; · exact interval_integrable_cpow (Or.inr h'.2)
   · rw [(by push_cast : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
-    simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.ofReal_mul_re, Complex.sub_re]
+    simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.re_ofReal_mul, Complex.sub_re]
     rfl
 #align integral_rpow integral_rpow
 -/

Mathbin/Analysis/SpecialFunctions/Pow/Real.lean

@@ -418,7 +418,7 @@ theorem rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^
 theorem rpow_add_int {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + n) = x ^ y * x ^ n := by
   rw [rpow_def, Complex.ofReal_add, Complex.cpow_add _ _ (complex.of_real_ne_zero.mpr hx),
     Complex.ofReal_int_cast, Complex.cpow_int_cast, ← Complex.ofReal_zpow, mul_comm,
-    Complex.ofReal_mul_re, ← rpow_def, mul_comm]
+    Complex.re_ofReal_mul, ← rpow_def, mul_comm]
 #align real.rpow_add_int Real.rpow_add_int
 -/
 

Mathbin/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean

@@ -373,7 +373,7 @@ theorem Real.tendsto_euler_sin_prod (x : ℝ) :
   by
   convert (complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x)
   · ext1 n
-    rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.ofReal_mul_re]
+    rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.re_ofReal_mul]
     suffices
       ∏ j : ℕ in Finset.range n, (1 - (x : ℂ) ^ 2 / (↑j + 1) ^ 2) =
         ↑(∏ j : ℕ in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))

Mathbin/CategoryTheory/Sites/Adjunction.lean

@@ -65,7 +65,7 @@ noncomputable section
 /-- This is the functor sending a sheaf `X : Sheaf J E` to the sheafification
 of `X ⋙ G`. -/
 abbrev composeAndSheafify (G : E ⥤ D) : Sheaf J E ⥤ Sheaf J D :=
-  sheafToPresheaf J E ⋙ (whiskeringRight _ _ _).obj G ⋙ presheafToSheaf J D
+  sheafToPresheaf J E ⋙ (whiskeringRight _ _ _).obj G ⋙ plusPlusSheaf J D
 #align category_theory.Sheaf.compose_and_sheafify CategoryTheory.Sheaf.composeAndSheafify
 -/
 

Mathbin/CategoryTheory/Sites/LeftExact.lean

@@ -249,14 +249,14 @@ variable (K : Type max v u)
 
 variable [SmallCategory K] [FinCategory K] [HasLimitsOfShape K D]
 
-instance : PreservesLimitsOfShape K (presheafToSheaf J D) :=
+instance : PreservesLimitsOfShape K (plusPlusSheaf J D) :=
   by
   constructor; intro F; constructor; intro S hS
   apply is_limit_of_reflects (Sheaf_to_presheaf J D)
   haveI : reflects_limits_of_shape K (forget D) := reflects_limits_of_shape_of_reflects_isomorphisms
   apply is_limit_of_preserves (J.sheafification D) hS
 
-instance [HasFiniteLimits D] : PreservesFiniteLimits (presheafToSheaf J D) :=
+instance [HasFiniteLimits D] : PreservesFiniteLimits (plusPlusSheaf J D) :=
   by
   apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{max v u}
   intros; skip; infer_instance

Mathbin/CategoryTheory/Sites/Pushforward.lean

@@ -54,7 +54,7 @@ instance {X : C} : IsCofiltered (J.cover X) :=
 same direction as `G`. -/
 @[simps]
 def Functor.sheafPullback (G : C ⥤ D) : Sheaf J A ⥤ Sheaf K A :=
-  sheafToPresheaf J A ⋙ lan G.op ⋙ presheafToSheaf K A
+  sheafToPresheaf J A ⋙ lan G.op ⋙ plusPlusSheaf K A
 #align category_theory.sites.pushforward CategoryTheory.Functor.sheafPullback
 -/
 
@@ -65,15 +65,15 @@ instance (G : C ⥤ D) [RepresentablyFlat G] :
   · infer_instance
   apply (config := { instances := false }) comp_preserves_finite_limits
   · apply CategoryTheory.lanPreservesFiniteLimitsOfFlat
-  · apply CategoryTheory.presheafToSheaf.Limits.preservesFiniteLimits.{u₁, v₁, v₁}
+  · apply CategoryTheory.plusPlusSheaf.Limits.preservesFiniteLimits.{u₁, v₁, v₁}
     infer_instance
 
 #print CategoryTheory.Functor.sheafAdjunctionContinuous /-
 /-- The pushforward functor is left adjoint to the pullback functor. -/
 def Functor.sheafAdjunctionContinuous {G : C ⥤ D} (hG₁ : CompatiblePreserving K G)
     (hG₂ : CoverPreserving J K G) :
     Functor.sheafPullback A J K G ⊣ Functor.sheafPushforwardContinuous A hG₁ hG₂ :=
-  ((Lan.adjunction A G.op).comp (sheafificationAdjunction K A)).restrictFullyFaithful
+  ((Lan.adjunction A G.op).comp (plusPlusAdjunction K A)).restrictFullyFaithful
     (sheafToPresheaf J A) (𝟭 _)
     (NatIso.ofComponents (fun _ => Iso.refl _) fun _ _ _ =>
       (Category.comp_id _).trans (Category.id_comp _).symm)