Update lean and mathlib

This update was quite annoying because `Int64` is now a native type
(though that's a good thing!). I've left a lot of cruft in here as a
result (shims converting between the native and obsolete ways of doing
things with Int64).

Interval/Approx.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.OrderIso

Interval/Box/Basic.lean

@@ -125,10 +125,11 @@ instance : ApproxStar Box ℂ where
 /-- `Box.neg` respects `approx` -/
 instance : ApproxNeg Box ℂ where
   approx_neg z := by
-    simp only [Box.instApprox, ← image_neg, image_image2, image2_subset_iff, mem_image2,
-      exists_and_left]
-    intro r rz i iz
-    refine ⟨-r, ?_, -i, ?_, rfl⟩
+    intro x m
+    simp only [instApprox, mem_neg, mem_image2] at m ⊢
+    rcases m with ⟨r,rz,i,iz,e⟩
+    rw [← neg_eq_iff_eq_neg] at e
+    refine ⟨-r, ?_, -i, ?_, by rw [← e]; rfl⟩
     repeat { apply approx_neg; simpa only [mem_neg, neg_neg] }
 
 /-- `Box.add` respects `approx` -/

Interval/EulerMaclaurin/EulerMaclaurin.lean

@@ -410,7 +410,9 @@ lemma presaw_smul_iteratedDeriv_by_parts [CompleteSpace E] (fc : ContDiffOn ℝ
       presaw (s+1) c a • iteratedDerivWithin s f t a -
       ∫ x in a..(a + 1), presaw (s+1) c x • iteratedDerivWithin (s+1) f t x := by
   have i0 := intervalIntegrable_presaw_smul (s := s) (c := c) fc.of_succ (by linarith) u abt
-  have i1 := intervalIntegrable_presaw_smul (s := s + 1) (c := c) fc (by linarith) u abt
+  have i1 : IntervalIntegrable (fun x ↦ presaw (s + 1) c x •
+      iteratedDerivWithin (s + 1) f t x) volume (↑a) (a + 1) :=
+    intervalIntegrable_presaw_smul (s := s + 1) (c := c) fc (by linarith) u abt
   rw [eq_sub_iff_add_eq, ← intervalIntegral.integral_add i0 i1]
   set g := fun x ↦ presaw (s + 1) c x • iteratedDerivWithin s f t x
   set g' := fun x ↦ presaw s c x • iteratedDerivWithin s f t x +

Interval/EulerMaclaurin/LHopital.lean

@@ -29,7 +29,7 @@ theorem lhopital_field {f g : 𝕜 → 𝕜} {a f' g' : 𝕜} (df : HasDerivAt f
   intro e ep
   simp only [hasDerivAt_iff_isLittleO, f0, sub_zero, smul_eq_mul, Asymptotics.isLittleO_iff,
     g0] at df dg
-  have g'p : 0 < ‖g'‖ := norm_pos_iff'.mpr g'0
+  have g'p : 0 < ‖g'‖ := norm_pos_iff.mpr g'0
   generalize hb : 2 * (1 + ‖f' / g'‖) / ‖g'‖ = b
   generalize hc : min (e / 2 / b) (2⁻¹ * ‖g'‖) = c
   have b0 : 0 < b := by
@@ -49,7 +49,7 @@ theorem lhopital_field {f g : 𝕜 → 𝕜} {a f' g' : 𝕜} (df : HasDerivAt f
   intro x fx gx xa
   generalize hy : x - a = y at fx gx
   have y0 : y ≠ 0 := by simpa only [← hy, sub_ne_zero]
-  have yp : 0 < ‖y‖ := norm_pos_iff'.mpr y0
+  have yp : 0 < ‖y‖ := norm_pos_iff.mpr y0
   have lo : ‖g x‖ ≥ 2⁻¹ * ‖g'‖ * ‖y‖ := by
     calc ‖g x‖
       _ = ‖y * g' + (g x - y * g')‖ := by ring_nf

Interval/EulerMaclaurin/PartialDerivCommute.lean

@@ -51,24 +51,24 @@ lemma deriv_deriv_comm {f : ℝ × ℝ → E} {z : ℝ × ℝ} (sf : ContDiff 
   simpa using fderiv_fderiv_comm sf (dx := 1) (dy := 1) (z := z)
 
 lemma _root_.ContDiff.iteratedDeriv_right {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {m : ℕ∞} {n : ℕ∞} {i : ℕ}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {m : WithTop ℕ∞} {n : ℕ∞} {i : ℕ}
     (hf : ContDiff 𝕜 n f) (hmn : m + i ≤ n) : ContDiff 𝕜 m (iteratedDeriv i f) := by
   have e : iteratedDeriv i f = fun x ↦ iteratedDeriv i f x := rfl
   simp only [e, iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.apply_apply]
   exact contDiff_const.clm_apply (hf.iteratedFDeriv_right hmn)
 
 lemma _root_.ContDiff.deriv {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-    {f : E → 𝕜 → F} {g : E → 𝕜} {m : ℕ∞} (fc : ContDiff 𝕜 ⊤ (uncurry f)) (gc : ContDiff 𝕜 ⊤ g) :
-    ContDiff 𝕜 m fun z ↦ deriv (fun y ↦ f z y) (g z) := by
+    {f : E → 𝕜 → F} {g : E → 𝕜} {m : WithTop ℕ∞} (fc : ContDiff 𝕜 ⊤ (uncurry f))
+    (gc : ContDiff 𝕜 ⊤ g) : ContDiff 𝕜 m fun z ↦ deriv (fun y ↦ f z y) (g z) := by
   simp_rw [← fderiv_deriv]
   simp_rw [← ContinuousLinearMap.apply_apply (v := (1 : 𝕜))]
   exact contDiff_const.clm_apply (ContDiff.fderiv fc (gc.of_le le_top) le_top)
 
 lemma _root_.ContDiff.iteratedDeriv {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
     {f : E → 𝕜 → F} {g : E → 𝕜}
-    {m : ℕ∞} {n : ℕ} (fc : ContDiff 𝕜 ⊤ (uncurry f)) (gc : ContDiff 𝕜 ⊤ g) :
+    {m : WithTop ℕ∞} {n : ℕ} (fc : ContDiff 𝕜 ⊤ (uncurry f)) (gc : ContDiff 𝕜 ⊤ g) :
     ContDiff 𝕜 m fun z ↦ iteratedDeriv n (fun y ↦ f z y) (g z) := by
   revert fc f
   induction' n with n ic