Fix Mathlib deprecation warnings

.github/workflows/blueprint.yml

@@ -104,6 +104,7 @@ jobs:
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           build: true
+          build-args: "--wfail"
           lint: true
           mk_all-check: true
 

LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean

@@ -74,7 +74,7 @@ lemma sub_of_not_isSFiniteKernel_right [∀ η : Kernel α β, Decidable (IsSFin
 lemma sub_of_isSFiniteKernel [IsSFiniteKernel κ] [IsSFiniteKernel η]
     [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
     κ - η = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η := by
-  rw [sub_def, dif_pos]
+  rw [sub_def, dite_eq_left]
   exact ⟨inferInstance, inferInstance⟩
 
 -- todo name

LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean

@@ -105,15 +105,15 @@ lemma arm_mul [Nonempty (Fin K)]
     grind
   rw [this]
   filter_upwards [arm_ae_eq_etcNextArm h (K * m - 1)] with ω hn_eq
-  rw [hn_eq, nextArm, dif_neg (by simp), dif_pos rfl]
+  rw [hn_eq, nextArm, dite_eq_right (by simp), dite_eq_left rfl]
   exact this ▸ rfl
 
 /-- For `n ≥ K * m`, the arm pulled at time `n + 1` is the same as the arm pulled at time `n`. -/
 lemma arm_add_one_of_ge (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P)
     {n : ℕ} (hm : m ≠ 0) (hn : K * m ≤ n) :
     A (n + 1) =ᵐ[P] fun ω ↦ A n ω := by
   filter_upwards [arm_ae_eq_etcNextArm h n] with ω hn_eq
-  rw [hn_eq, nextArm, dif_neg (by grind), dif_neg]
+  rw [hn_eq, nextArm, dite_eq_right (by grind), dite_eq_right]
   · rfl
   · have : 0 < K * m := Nat.mul_pos hK hm.bot_lt
     grind

LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

@@ -132,7 +132,7 @@ lemma forall_arm_eq_mod_of_lt (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationa
   | zero => exact arm_zero h
   | succ n _ =>
     filter_upwards [arm_ae_eq_ucbNextArm h n] with h h_eq
-    rw [h_eq, nextArm, if_pos]
+    rw [h_eq, nextArm, ite_eq_left]
     · rfl
     · grind
 

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -495,7 +495,7 @@ lemma measurable_hist_truePast [Countable 𝓐] (alg : Algorithm 𝓐 R)
     by_cases hb : b = a
     · subst hb
       simp only [truePast, ↓reduceIte]
-      rw [min_eq_left, if_pos (by grind)]
+      rw [min_eq_left, ite_eq_left (by grind)]
       grind
     · simp [truePast, hb]
   rw [h_eq]

LeanMachineLearning/SequentialLearning/FiniteActions.lean

@@ -324,7 +324,7 @@ lemma stepsUntil_eq_leastGE (a : 𝓐) (hm : m ≠ 0) :
     exact exists_pullCount_eq_of_le hs hm
   by_cases h_exists : ∃ s, m ≤ pullCount A a (s + 1) ω
   swap; · simp_rw [h_iff]; simp [h_exists]
-  rw [if_pos h_exists, dif_pos]
+  rw [ite_eq_left h_exists, dite_eq_left]
   swap; · rwa [h_iff]
   simp only [ENat.some_eq_natCast, Nat.cast_inj]
   rw [Nat.find_eq_iff]
@@ -476,7 +476,7 @@ lemma stepsUntil_eq_iff {ω : Ω} (n : ℕ) :
     refine ⟨pullCount_add_one_eq_of_stepsUntil_eq_coe h, fun k hk ↦ ?_⟩
     exact pullCount_lt_of_le_stepsUntil a ω h_exists (by rw [h]; exact mod_cast hk)
   · classical
-    rw [stepsUntil_eq_dite a m ω, dif_pos ⟨n, h.1⟩]
+    rw [stepsUntil_eq_dite a m ω, dite_eq_left ⟨n, h.1⟩]
     simp only [Nat.cast_inj]
     rw [Nat.find_eq_iff]
     exact ⟨h.1, fun k hk ↦ (h.2 k hk).ne⟩
@@ -810,7 +810,7 @@ lemma sumRewards_eq_of_pullCount_eq {R' : ℕ → Ω → ℝ} {s t : ℕ}
       intro ha
       have h1 := ha ▸ pullCount_action_eq_pullCount_add_one (A := A) t ω
       lia
-    rw [sumRewards_add_one, if_neg hne, add_zero, ih h_eq_t]
+    rw [sumRewards_add_one, ite_eq_right hne, add_zero, ih h_eq_t]
 
 lemma sumRewards_eq_pullCount_mul_empMean {R' : ℕ → Ω → ℝ} {ω : Ω}
     (h_pull : pullCount A a t ω ≠ 0) :
@@ -825,9 +825,9 @@ lemma sum_rewardByCount_eq_sumRewards {R' : ℕ → Ω → ℝ} (a : 𝓐) (t :
     · rw [← hta] at ht ⊢
       rw [pullCount_action_eq_pullCount_add_one, sum_Icc_succ_top (Nat.le_add_left 1 _), ht]
       unfold sumRewards
-      rw [sum_range_succ, if_pos rfl, rewardByCount_pullCount_add_one_eq_reward]
+      rw [sum_range_succ, ite_eq_left rfl, rewardByCount_pullCount_add_one_eq_reward]
     · unfold sumRewards
-      rwa [pullCount_eq_pullCount_of_action_ne hta, sum_range_succ, if_neg hta, add_zero]
+      rwa [pullCount_eq_pullCount_of_action_ne hta, sum_range_succ, ite_eq_right hta, add_zero]
 
 lemma sumRewards_add_one_eq_sumRewards' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
     sumRewards A R' a (n + 1) ω = sumRewards' n (fun i ↦ (A i ω, R' i ω)) a := by