Bump toolchain to v4.35.0

Analysis/Appendix_A_1.lean

@@ -188,10 +188,10 @@ example {X Y Z:Prop} (hXY: X ↔ Y) (hXZ: X ↔ Z) : [X,Y,Z].TFAE := by
   tfae_have 1 ↔ 3 := by exact hXZ  -- This line is optional
   tfae_finish
 
-/-- Note for the {name (full := List.TFAE.out)}`out` method that one indexes starting from 0, in
-contrast to the {tactic}`tfae_have` tactic. -/
+/-- Note that the {name (full := List.TFAE.out)}`out` method indexes starting from 1, just like
+the {tactic}`tfae_have` tactic. -/
 example {X Y Z:Prop} (h: [X,Y,Z].TFAE) : X ↔ Y := by
-  exact h.out 0 1
+  exact h.out 1 2
 
 /-- Exercise A.1.1.  Fill in the first {syntax term}`sorry` with something reasonable. -/
 example {X Y:Prop} : ¬ ((X ∨ Y) ∧ ¬ (X ∧ Y)) ↔ sorry := by sorry

Analysis/Appendix_A_2.lean

@@ -34,7 +34,7 @@ example : (3:ℤ) = 2 → (3:ℤ)^2 = 4 := example_A_2_1 3
 
 example : (-2:ℤ) = 2 → (-2:ℤ)^2 = 4 := example_A_2_1 (-2)
 
-#check _root_.not_imp
+#check Classical.not_imp
 
 example : ¬ ((2+2=4) → (4+4)=2) := by
   rw [Classical.not_imp]
@@ -66,7 +66,7 @@ example : ((2+2:ℤ)=5) → (4=(10-4:ℤ)) := by
   intro h
   have : (4 + 4:ℤ) = 10 := by
     replace h := congr(2*$h)
-    convert h using 1
+    convert h using 1 <;> norm_num
   rwa [←eq_sub_iff_add_eq] at this
 
 /-- Theorem A.2.4 -/

Analysis/Appendix_A_6.lean

@@ -1,6 +1,7 @@
 import Mathlib.Tactic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import Mathlib.Analysis.Calculus.Deriv.MeanValue
 
 /-!
 # Analysis I, Appendix A.6: Some examples of proofs and quantifiers

Analysis/Appendix_B_1.lean

@@ -56,7 +56,7 @@ abbrev Digit.mk {n:ℕ} (h: n < 10) : Digit := ⟨n, h⟩
 theorem Digit.toNat_mk {n:ℕ} (h: n < 10) : (Digit.mk h:ℕ) = n := rfl
 
 @[simp]
-theorem Digit.inj (d d':Digit) : d = d' ↔ (d:ℕ) = d' := by grind
+theorem Digit.inj (d d':Digit) : d = d' ↔ (d:ℕ) = d' := Fin.ext_iff
 
 theorem Digit.mk_eq_iff (d:Digit) {n:ℕ} (h: n < 10) : d = mk h ↔ (d:ℕ) = n := by
   convert Digit.inj d (mk h)
@@ -72,7 +72,7 @@ theorem Digit.mk_eq_iff (d:Digit) {n:ℕ} (h: n < 10) : d = mk h ↔ (d:ℕ) = n
 #check (9:Digit)
 
 theorem Digit.eq (n: Digit) : n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9 := by
-  fin_cases n <;> simp +decide
+  decide +revert
 
 /-- Definition B.1.2 -/
 structure PosintDecimal where
@@ -134,7 +134,7 @@ theorem PosintDecimal.ten_eq_ten : (mk' 1 [0] (by decide):ℕ) = 10 := by
   decide
 
 theorem PosintDecimal.digit_eq {d:Digit} (h: d ≠ 0) : (mk' d [] h:ℕ) = d := by
-  simp [toNat, mk']
+  decide +revert
 
 theorem PosintDecimal.pos (p:PosintDecimal) : 0 < (p:ℕ) := by
   simp [toNat]
@@ -188,6 +188,7 @@ theorem PosintDecimal.eq_append {p:PosintDecimal} (h: 2 ≤ p.digits.length) : 
   rw [←p.digits.cons_head_tail p.nonempty]
   congr 1
   convert (List.dropLast_append_getLast _).symm using 2; grind
+  rw [List.getLast_tail]
   simp [←List.length_pos_iff]; omega
 
 /-- Theorem B.1.4 (Uniqueness and existence of decimal representations) -/
@@ -198,8 +199,8 @@ theorem PosintDecimal.exists_unique (n:ℕ) : n > 0 → ∃! p:PosintDecimal, (p
   -- note: the variable `m` in the text is referred to as `m+1` here.
   clear n; intro m hind _
   obtain hm | hm := lt_or_ge m 9
-  . apply ExistsUnique.intro (mk' (.mk (show m+1 < 10 by omega)) [] (by simp [Digit.mk]))
-    . simp [mk', Digit.mk, toNat, Digit.toNat]
+  . apply ExistsUnique.intro (mk' (.mk (show m+1 < 10 by omega)) [] (Fin.ne_of_val_ne m.succ_ne_zero))
+    . simp [mk', Digit.mk, toNat, Digit.toNat]; rfl
     intro d hd
     obtain hdl | hdl := lt_or_ge d.digits.length 2
     . replace hdl : d.digits.length = 1 := by linarith [d.length_pos]
@@ -210,18 +211,18 @@ theorem PosintDecimal.exists_unique (n:ℕ) : n > 0 → ∃! p:PosintDecimal, (p
       . simp [hdl, mk']
       intro i hi₁ hi₂
       replace hi₁ : i = 0 := by omega
-      simp [hi₁, mk', Digit.mk, hd]
+      simp [hi₁, mk', Digit.mk, hd]; rfl
     have : d.toNat ≥ 10 := calc
       _ ≥ (d.head:ℕ) * 10^(d.digits.length-1) := by
         set a : Fin d.digits.length := ⟨ d.digits.length - 1, by omega ⟩
+        simp only [ge_iff_le, toNat]
         convert Finset.single_le_sum _ (Finset.mem_univ a)
         . simp [a, head, List.head_eq_getElem]
         . infer_instance
         intros; positivity
       _ ≥ 1 * 10^(2-1) := by
         gcongr
-        . have := d.head_ne_zero'; omega
-        norm_num
+        have := d.head_ne_zero'; omega
       _ = 10 := by norm_num
     linarith
   have := (m+1).mod_add_div 10

Analysis/Appendix_B_2.lean

@@ -67,6 +67,7 @@ theorem NNRealDecimal.surj (x:NNReal) : ∃ d:NNRealDecimal, x = d := by
   have := (d.toNNReal_conv.tendsto_sum_tsum_nat).const_add (s 0:NNReal)
   convert_to Filter.atTop.Tendsto (fun n ↦ s n * (10:NNReal)^(-n:ℝ)) (nhds (d:NNReal)) at this
   . ext n; rw [hsum n]
+  . rfl
   apply tendsto_nhds_unique _ this
   apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ x - (10:NNReal)^(-n:ℝ)) (h := fun _ ↦ x)
   . convert Filter.Tendsto.const_sub (c := 0) x _

Analysis/MeasureTheory/Notation.lean

@@ -1,4 +1,5 @@
 import Mathlib.Tactic
+import Mathlib.Analysis.InnerProductSpace.PiL2
 
 /-!
 # Introduction to Measure Theory, Chapter 0: Notation
@@ -79,7 +80,7 @@ def EuclideanSpace'.prod_equiv (d₁ d₂:ℕ) : EuclideanSpace' (d₁ + d₂) 
       simp only [this]
   right_inv x := by
     ext ⟨i, hi⟩
-    · simp [dif_pos hi]
+    · simp [dite_eq_left hi]
     · simp [show ¬(i + d₁ < d₁) by omega]
 
 def EuclideanSpace'.prod {d₁ d₂:ℕ} (E₁: Set (EuclideanSpace' d₁)) (E₂: Set (EuclideanSpace' d₂)) : Set (EuclideanSpace' (d₁+d₂)) := (EuclideanSpace'.prod_equiv d₁ d₂).symm '' (E₁ ×ˢ E₂)
@@ -124,20 +125,19 @@ theorem ENNReal.upward_continuous {x y:ℕ → ENNReal} (hx: Monotone x) (hy: Mo
       have := hx hn.1
       order
     have : atTop.Tendsto (fun n ↦ x n * y ny) (nhds ⊤) := by
-      convert Tendsto.comp (g := fun z ↦ z * y ny) _ hx_lim
-      convert (ENNReal.continuous_mul_const hyn').tendsto ⊤
-      rw [top_mul]; order
+      have h := ((ENNReal.continuous_mul_const hyn').tendsto ⊤).comp hx_lim
+      rw [ENNReal.top_mul hny.ne'] at h
+      exact h
     apply tendsto_nhds_top_mono this
     simp [EventuallyLE, eventually_atTop]
     use ny; intro n hn
     gcongr; exact hy hn
   obtain rfl | hy₀' := eq_top_or_lt_top y₀
   . rw [mul_top (by order)]
     have : atTop.Tendsto (fun n ↦ x nx * y n) (nhds ⊤) := by
-      convert Tendsto.comp (g := fun z ↦ (x nx) * z) _ hy_lim
-      convert (ENNReal.continuous_const_mul _).tendsto ⊤
-      . rw [mul_top]; order
-      specialize hx_lt nx; order
+      have h := ((ENNReal.continuous_const_mul ((hx_lt nx).trans_lt hx₀').ne).tendsto ⊤).comp hy_lim
+      rw [ENNReal.mul_top hnx.ne'] at h
+      exact h
     apply tendsto_nhds_top_mono this
     simp [EventuallyLE, eventually_atTop]
     use nx; intro n hn
@@ -166,7 +166,7 @@ example : ∃ (x y:ℕ → ENNReal) (_hx: Antitone x) (_hy: Antitone y)
   · have hxR : Tendsto (fun n : ℕ => (1 : ℝ) / (n : ℝ)) atTop (nhds 0) :=
       tendsto_one_div_atTop_nhds_zero_nat
     have hxR' : Tendsto (fun n : ℕ => ENNReal.ofReal (1 / (n : ℝ))) atTop (nhds 0) := by
-      simpa [Function.comp, ENNReal.ofReal_zero]
+      simpa [Function.comp_def, ENNReal.ofReal_zero]
       using (ENNReal.continuous_ofReal.tendsto 0).comp hxR
     have heq : ∀ᶠ n in atTop, x n = ENNReal.ofReal (1 / (n : ℝ)) := by
       refine (eventually_ge_atTop 1).mono ?_
@@ -189,8 +189,7 @@ example : ∃ (x y:ℕ → ENNReal) (_hx: Antitone x) (_hy: Antitone y)
 example {A:Type} {x : A → ENNReal} (hx: ∑' α, x α < ⊤) :
   ∃ E: Set A, Countable E ∧ ∀ α ∉ E, x α = 0 := by
   refine ⟨{a | x a ≠ 0}, ?_, ?_⟩
-  · simpa [Set.mem_setOf_eq] using
-      (Summable.countable_support_ennreal (ne_of_lt hx))
+  · exact Summable.countable_support_ennreal (ne_of_lt hx)
   · aesop
 
 /-- Theorem 0.0.2 (Tonelli's theorem for series)  -/
@@ -219,7 +218,7 @@ theorem ENNReal.tsum_of_tsum (x: ℕ → ℕ → ENNReal) : ∑' p:ℕ × ℕ, x
       _ ≤ _ := by apply ENNReal.tsum_le_tsum; intros; apply ENNReal.sum_le_tsum
   apply le_of_tendsto' (tendsto_nat_tsum _); intro N
   apply le_of_tendsto' (f := fun M ↦ ∑ n ∈ .range N, ∑ m ∈ .range M, x n m) (x := atTop)
-  . apply tendsto_finset_sum; intros; apply tendsto_nat_tsum
+  . apply tendsto_finsetSum; intros; apply tendsto_nat_tsum
   intro M; calc
     _ = ∑ p ∈ .range N ×ˢ .range M, x p.1 p.2 := by symm; apply Finset.sum_product
     _ ≤ _ := ENNReal.sum_le_tsum _

Analysis/MeasureTheory/Section_1_1_1.lean

@@ -38,7 +38,7 @@ instance BoundedInterval.instEmpty : EmptyCollection BoundedInterval where
 /-- The empty {name}`BoundedInterval` coerces to the empty set. -/
 @[simp]
 theorem BoundedInterval.coe_empty : ((∅ : BoundedInterval):Set ℝ) = ∅ := by
-  simp [toSet]
+  show toSet (Ioo 0 0) = ∅; simp [toSet]
 
 open Classical in
 /-- This is to make {name}`Finset`s of {name}`BoundedInterval`s work properly -/
@@ -278,12 +278,12 @@ lemma toSet_injective_of_nonempty {I J : BoundedInterval}
 end BoundedInterval
 
 /-- A witness for lowerBound of upperBounds -/
-def witness_lowerBound_upperBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X)
+lemma witness_lowerBound_upperBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X)
     : y ∈ lowerBounds (upperBounds X) := by
   intro u hu; simp [upperBounds] at hu; exact hu hy
 
 /-- A witness for upperBound of lowerBounds -/
-def witness_upperBound_lowerBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X)
+lemma witness_upperBound_lowerBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X)
     : y ∈ upperBounds (lowerBounds X) := by
   intro u hu; simp [lowerBounds] at hu; exact hu hy
 
@@ -788,11 +788,11 @@ theorem BoundedInterval.sdiff (I J: BoundedInterval) :
   refine ⟨K₁, K₂, ?_⟩
   rw [← hK₁, ← hK₂]
   ext x
-  simp only [Set.mem_diff, Set.mem_union, Set.mem_inter_iff, mem_iff', mk'_a, mk'_b,
+  simp only [Set.mem_sdiff, Set.mem_union, Set.mem_inter_iff, mem_iff', mk'_a, mk'_b,
     mk'_lclosed, mk'_uclosed]
   cases hIl : I.lclosed <;> cases hIu : I.uclosed <;> cases hJl : J.lclosed <;> cases hJu : J.uclosed <;>
     simp only [Bool.not_true, Bool.not_false, Bool.false_eq_true, reduceIte] <;>
-    push_neg <;>
+    push Not <;>
     constructor <;>
     intro h <;>
     grind
@@ -815,13 +815,13 @@ theorem Box.sdiff {d:ℕ} (B C: Box d) : IsElementary (B.toSet \ C.toSet) := by
     cases k <;> simp
   refine ⟨Finset.univ.image (fun p : Fin d × Bool ↦ piece p.1 p.2), ?_⟩
   ext x
-  simp only [Set.mem_diff, Box.mem_toSet, Set.mem_iUnion, Finset.mem_image, Finset.mem_univ,
+  simp only [Set.mem_sdiff, Box.mem_toSet, Set.mem_iUnion, Finset.mem_image, Finset.mem_univ,
     true_and, exists_prop]
   constructor
   · rintro ⟨hxB, hxC⟩
     obtain ⟨i, hi⟩ : ∃ i, x i ∉ (C.side i : Set ℝ) := by
       by_contra hc
-      push_neg at hc
+      push Not at hc
       exact hxC (fun i ↦ hc i)
     have : x i ∈ ((K₁ i : Set ℝ)) ∪ ((K₂ i : Set ℝ)) := by
       rw [← hK i]; exact ⟨hxB i, hi⟩
@@ -858,13 +858,13 @@ theorem IsElementary.sdiff {d:ℕ} {E F: Set (EuclideanSpace' d)}
   | insert C T' hC ih =>
     have hrw : E \ (⋃ B ∈ insert C T', (B:Set (EuclideanSpace' d)))
         = (E \ ⋃ B ∈ T', (B:Set (EuclideanSpace' d))) \ C.toSet := by
-      rw [Finset.set_biUnion_insert, Set.diff_diff, Set.union_comm]
+      rw [Finset.set_biUnion_insert, Set.sdiff_sdiff, Set.union_comm]
     rw [hrw]
     obtain ⟨S, hS⟩ := ih
     rw [hS]
     have hdiff : (⋃ B ∈ S, (B:Set (EuclideanSpace' d))) \ C.toSet
         = ⋃ B ∈ S, ((B:Set (EuclideanSpace' d)) \ C.toSet) := by
-      ext y; simp only [Set.mem_diff, Set.mem_iUnion, exists_prop]; tauto
+      ext y; simp only [Set.mem_sdiff, Set.mem_iUnion, exists_prop]; tauto
     rw [hdiff]
     have : (⋃ B ∈ S, ((B:Set (EuclideanSpace' d)) \ C.toSet))
         = ⋃ X ∈ S.image (fun B : Box d ↦ (B:Set (EuclideanSpace' d)) \ C.toSet), X := by
@@ -899,11 +899,11 @@ theorem BoundedInterval.translate (I: BoundedInterval) (c:ℝ) :
   · intro hy
     refine ⟨y - c, ?_, by ring⟩
     revert hy
-    cases I.lclosed <;> cases I.uclosed <;> simp only [if_true, if_false,
+    cases I.lclosed <;> cases I.uclosed <;> simp only [ite_true, ite_false,
       Bool.false_eq_true] <;> grind
   · rintro ⟨z, hz, rfl⟩
     revert hz
-    cases I.lclosed <;> cases I.uclosed <;> simp only [if_true, if_false,
+    cases I.lclosed <;> cases I.uclosed <;> simp only [ite_true, ite_false,
       Bool.false_eq_true] <;> grind
 
 /-- Translating a box gives a box. -/
@@ -1059,7 +1059,7 @@ theorem Box.partition {d:ℕ} (S: Finset (Box d)) : ∃ T: Finset (Box d), (T :
   intro B hB
   choose U hU using hJ
   use {B' | ∀ i, ∃ hi : B'.val.side i ∈ J i, ⟨ _, hi ⟩ ∈ U i hB}
-  ext x; simp only [Box.mem_toSet, Set.mem_iUnion, Set.mem_setOf_eq, Subtype.exists]
+  ext x; simp only [Box.mem_toSet, Set.mem_iUnion, Set.mem_ofPred_eq, Subtype.exists]
   constructor
   . intro h
     have h' : ∀ i, x i ∈ ⋃ K ∈ U i hB, (K:BoundedInterval).toSet := by
@@ -1150,7 +1150,7 @@ theorem Box.vol_eq {d:ℕ} (B: Box d):
   (nhds |B|ᵥ) := by
   simp [Box.volume]
   have : ∀ i ∈ Finset.univ, Filter.atTop.Tendsto (fun N:ℕ ↦ (N:ℝ)⁻¹ * Nat.card ↥((B.side i).toSet ∩ Set.range ((fun n:ℤ ↦ (N:ℝ)⁻¹*n)))) (nhds |B.side i|ₗ) := fun i _ ↦ (B.side i).length_eq
-  convert tendsto_finset_prod Finset.univ this with N
+  convert tendsto_finsetProd Finset.univ this with N
   simp [Finset.prod_mul_distrib]; left
   norm_cast; simp_rw [←Nat.card_coe_set_eq, ←Nat.card_pi]
   apply Nat.card_congr (B.sample_congr N)
@@ -1161,7 +1161,7 @@ theorem Box.sum_vol_eq {d:ℕ} {T: Finset (Box d)}
  (hT: (T : Set (Box d)).PairwiseDisjoint Box.toSet) :
   Filter.atTop.Tendsto (fun N:ℕ ↦ (N:ℝ)^(-d:ℝ) * Nat.card ↥((⋃ B ∈ T, B.toSet) ∩ (Set.range (fun (n:Fin d → ℤ) ↦ .toLp 2 (fun i ↦ (N:ℝ)⁻¹*(n i))))))
   (nhds (∑ B ∈ T, |B|ᵥ)) := by
-  apply (tendsto_finset_sum T (fun B _ ↦ B.vol_eq)).congr'
+  apply (tendsto_finsetSum T (fun B _ ↦ B.vol_eq)).congr'
   rw [Filter.EventuallyEq, Filter.eventually_atTop]; use 1; intro N hN
   symm; convert Finset.mul_sum _ _ _
   convert Nat.cast_sum _ _
@@ -1395,7 +1395,7 @@ lemma IsElementary.sum_insert_split {d:ℕ} {a: Set (EuclideanSpace' d)} {S': Fi
     -- Base case: S' = ∅
     -- LHS: ∑ E:(insert a ∅), ... = sum over {a}
     -- RHS: measure of a + ∑ E:∅, ... = measure of a + 0
-    simp [Finset.sum_empty]
+    simp [Finset.sum_empty]; exact Fintype.sum_unique _
   | @insert b S'' hb_notin ih =>
     -- Inductive case: S' = insert b S''
     -- Goal: ∑ E:(insert a (insert b S'')), ... = measure(a) + ∑ E:(insert b S''), ...
@@ -1867,15 +1867,15 @@ lemma Box.prod_side {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) (i : Fin (
 lemma EuclideanSpace'.prod_equiv_symm_apply_left {d₁ d₂:ℕ}
     (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) {i : ℕ} (hi : i < d₁) :
     (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) ⟨i, Nat.lt_add_right d₂ hi⟩ = y ⟨i, hi⟩ := by
-  simp [EuclideanSpace'.prod_equiv, dif_pos hi]
+  simp [EuclideanSpace'.prod_equiv, dite_eq_left hi]
 
 /-- Coordinate of a product vector in the second block. -/
 lemma EuclideanSpace'.prod_equiv_symm_apply_right {d₁ d₂:ℕ}
     (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) {j : ℕ} (hj : j < d₂) :
     (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) ⟨d₁ + j, Nat.add_lt_add_left hj d₁⟩ =
       z ⟨j, hj⟩ := by
   have hnot : ¬ d₁ + j < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _)
-  simp [EuclideanSpace'.prod_equiv, dif_neg hnot, Nat.add_sub_cancel_left]
+  simp [EuclideanSpace'.prod_equiv, dite_eq_right hnot, Nat.add_sub_cancel_left]
 
 /-- First factor of {name}`prod_equiv`. -/
 lemma EuclideanSpace'.prod_equiv_apply_fst {d₁ d₂:ℕ}
@@ -1900,22 +1900,22 @@ lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) :
     rcases i with ⟨i, hi⟩
     simp only [Box.prod]
     split_ifs with h
-    · simp [EuclideanSpace'.prod_equiv, dif_pos h]
+    · simp [EuclideanSpace'.prod_equiv, dite_eq_left h]
       exact hy ⟨i, h⟩
-    · simp [EuclideanSpace'.prod_equiv, dif_neg h]
+    · simp [EuclideanSpace'.prod_equiv, dite_eq_right h]
       exact hz ⟨i - d₁, Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) hi⟩
   · intro hx
     refine ⟨⟨(EuclideanSpace'.prod_equiv d₁ d₂ x).1, (EuclideanSpace'.prod_equiv d₁ d₂ x).2⟩, ?_,
       (EuclideanSpace'.prod_equiv d₁ d₂).left_inv x⟩
     constructor
     · intro i
       have hx' := hx ⟨(i : ℕ), Nat.lt_add_right d₂ i.isLt⟩
-      simp [Box.prod, EuclideanSpace'.prod_equiv, dif_pos i.isLt] at hx' ⊢
+      simp [Box.prod, EuclideanSpace'.prod_equiv, dite_eq_left i.isLt] at hx' ⊢
       exact hx'
     · intro j
       have hnot : ¬ (j : ℕ) + d₁ < d₁ := Nat.not_lt.mpr (Nat.le_add_left d₁ _)
       have hx' := hx ⟨(j : ℕ) + d₁, by omega⟩
-      simp [Box.prod, EuclideanSpace'.prod_equiv, dif_neg hnot] at hx' ⊢
+      simp [Box.prod, EuclideanSpace'.prod_equiv, dite_eq_right hnot] at hx' ⊢
       convert hx' <;> (apply Fin.ext; exact Nat.add_sub_cancel (j : ℕ) d₁)
 
 /-- Recovering the factors from a product box. -/
@@ -1926,12 +1926,12 @@ lemma Box.prod_injective {d₁ d₂:ℕ} :
   refine Prod.ext ?_ ?_
   · ext i
     have := congrFun hside ⟨i, Nat.lt_add_right d₂ i.isLt⟩
-    rw [Box.prod_side, Box.prod_side, dif_pos i.isLt, dif_pos i.isLt] at this
+    rw [Box.prod_side, Box.prod_side, dite_eq_left i.isLt, dite_eq_left i.isLt] at this
     exact this
   · ext j
     have hnot : ¬ (j : ℕ) + d₁ < d₁ := Nat.not_lt.mpr (Nat.le_add_left d₁ _)
     have := congrFun hside ⟨(j : ℕ) + d₁, by omega⟩
-    rw [Box.prod_side, Box.prod_side, dif_neg hnot, dif_neg hnot] at this
+    rw [Box.prod_side, Box.prod_side, dite_eq_right hnot, dite_eq_right hnot] at this
     have hj (C : Box d₂) : C.side ⟨(j : ℕ) + d₁ - d₁,
         Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp hnot)
           (by omega)⟩ = C.side j :=