chore: downstream-lean4 adaptations for nightly-2026-08-06

Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean

@@ -187,21 +187,21 @@ lemma moveInputPos_leftBoundary {n : ℕ} :
 lemma moveInputPos_rightBoundary {n : ℕ} :
     moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by
   unfold moveInputPos
-  rw [dif_neg (by simp; omega)]
+  rw [dite_eq_right (by simp; omega)]
 
 /-- A left move away from the left input boundary decrements the native input position. -/
 lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) :
     moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by
   have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz))
   unfold moveInputPos
   apply Fin.ext
-  rw [dif_pos] <;> simp <;> omega
+  rw [dite_eq_left] <;> simp <;> omega
 
 /-- A right move away from the right input boundary increments the native input position. -/
 lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) :
     moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by
   unfold moveInputPos
-  rw [dif_pos]
+  rw [dite_eq_left]
   · apply Fin.ext
     simp
   · simp

Cslib/Foundations/Data/HasFresh.lean

@@ -62,7 +62,7 @@ def HasFresh.ofSucc {α : Type u} [Inhabited α] [SemilatticeSup α] (f : α →
     HasFresh α where
   fresh s := if hs : s.Nonempty then f (s.sup' hs id) else default
   fresh_notMem s h := if hs : s.Nonempty
-    then not_le_of_gt (hf (s.sup' hs id)) <| by rw [dif_pos hs] at h; exact s.le_sup' id h
+    then not_le_of_gt (hf (s.sup' hs id)) <| by rw [dite_eq_left hs] at h; exact s.le_sup' id h
     else hs ⟨_, h⟩
 
 /-- `ℕ` has a computable fresh function. -/

Cslib/MachineLearning/PACLearning/VersionSpace.lean

@@ -165,7 +165,7 @@ theorem empiricalError_eq_div [DecidableEq β]
     empiricalError h S = (empiricalMiscount h S : ℝ≥0∞) / m := by
   have hm_ne : m ≠ 0 := hm.ne'
   unfold empiricalError empiricalMeasure error empiricalMiscount
-  rw [dif_neg hm_ne, Measure.smul_apply, Measure.finsetSum_apply]
+  rw [dite_eq_right hm_ne, Measure.smul_apply, Measure.finsetSum_apply]
   simp only [Measure.dirac_apply, Set.indicator, Set.mem_ofPred_eq, Pi.one_apply, smul_eq_mul]
   rw [Finset.sum_boole, ← ENNReal.div_eq_inv_mul]