chore: bump Lean and Mathlib to v4.34.0-rc1

LeanPool/ABCExceptions/Section2.lean

@@ -953,7 +953,7 @@ private theorem radical_le_X_pow_mul_prod : (radical n : ℕ) ≤ (X : ℝ)^ε *
 theorem x_K_le_X_pow : x KIndex ≤ (X : ℝ) ^ ε := by
   have h1n := h1n
   have hnX := hnX
-  rw [x, if_pos ?side]
+  rw [x, ite_eq_left ?side]
   case side =>
     simp
   have := hKd
@@ -1494,7 +1494,7 @@ noncomputable def const (ε : ℝ) : ℝ :=
 theorem const_spec {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) :
     let d := ⌊10 * ε⁻¹ ^ 4⌋₊
     ∀ x : ℕ, 2 ≤ x → (Nat.log 2 x + 1) ^ (3 * d) ≤ const ε * (x : ℝ)^(ε/4) := by
-  rw [const, dif_pos hε_pos, dif_pos hε]
+  rw [const, dite_eq_left hε_pos, dite_eq_left hε]
   extract_lets d _ _ _ hd
   apply Classical.choose_spec (tmp hε_pos d hd)
 
@@ -1510,8 +1510,8 @@ theorem const_nonneg {ε : ℝ} : 0 ≤ const ε := by
       apply nonneg_of_mul_nonneg_left this
       apply Real.rpow_pos_of_pos
       norm_num
-    · rw [const, dif_pos hε_pos, dif_neg hε]
-  · rw [const, dif_neg hε_pos]
+    · rw [const, dite_eq_left hε_pos, dite_eq_right hε]
+  · rw [const, dite_eq_right hε_pos]
 
 end Asymptotics
 

LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/BuildStrategies.lean

@@ -50,10 +50,10 @@ lemma eq_planA (hQ : ∀ (x : planA.subtree) (hp : IsPosition x.val p),
   (tryAndElse planA planB).residual x = tryAndElse (planA.residual x) (planB.residual x) := by
   ext1 y hp; dsimp [tryAndElse, PreStrategy.residual]
   split_ifs with h h' h'
-  · exact (if_pos h').symm
+  · exact (ite_eq_left h').symm
   · obtain ⟨a, h⟩ := h; cases h' ⟨⟨a.1, by simpa using a.2⟩, h⟩
   · obtain ⟨a, h'⟩ := h'; cases h ⟨⟨a.1, by simpa using a.2⟩, h'⟩
-  · exact (if_neg h').symm
+  · exact (ite_eq_right h').symm
 end «tryAndElse»
 
 section «void»
@@ -350,7 +350,7 @@ lemma followUntilWon_body : body S.followUntilWon.subtree ≤ body S.subtree ∪
     have hc : ¬ G.WonPosition (S.followUntilWon.subtreeIncl (body.take n ⟨x, hx⟩)).val
         (p.residual (S.followUntilWon.subtreeIncl (body.take n ⟨x, hx⟩)).val) :=
       fun hw ↦ h' ⟨n, hw⟩
-    rwa [if_neg hc] at hmem
+    rwa [ite_eq_right hc] at hmem
 @[simp] lemma followUntilWon_isWinning : S.followUntilWon.IsWinning ↔ S.IsWinning :=
   ⟨sub_winning S.le_followUntilWon, fun h ↦ subset_trans S.followUntilWon_body (by simpa)⟩
 end «followUntilWon»

LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/GaleStewart.lean

@@ -72,8 +72,7 @@ lemma defensive_winning_isClosed (hC : IsClosed G.payoff) (hP : IsPruned G.tree)
     (by synthIsPosition) ha
   apply AllWinning.existsWinning _ (hP.sub _); apply wonPosition_iff_disjoint.mpr
   rw [← Set.subset_empty_iff]; intro a' ⟨h1, h2⟩; apply hfa a'
-  · conv at h1 => simp [ExtensionsAt.val']
-    apply principalOpen_mono _ h1
+  · apply principalOpen_mono _ h1
     nth_rw 1 [(principalOpen_iff_restrict _ _).mp h]
     change Stream'.take x.length a <+:
       Stream'.take (2 * (x.length / 2)) a ++ [a.get (2 * (x.length / 2))]

LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/Games.lean

@@ -57,7 +57,7 @@ namespace Game
         simp [residual, hy, hx, hxy]
     · by_cases hx : x.length % 2 = 0
       · have hxy : (x.length + y.length) % 2 = 1 := by omega
-        simp only [residual, List.length_append, hxy, hy, hx, if_false, if_true, one_ne_zero]
+        simp only [residual, List.length_append, hxy, hy, hx, ite_false, ite_true, one_ne_zero]
         ext a
         simp only [Set.preimage_compl, Set.image_val_compl, subAt_append, subAt_body,
           Stream'.append_append_stream, subAt_body_image, subAtInf_append, Set.mem_sdiff,
@@ -66,7 +66,7 @@ namespace Game
       · have hx1 : x.length % 2 = 1 := Nat.mod_two_ne_zero.mp hx
         have hy1 : y.length % 2 = 1 := Nat.mod_two_ne_zero.mp hy
         have hxy : (x.length + y.length) % 2 = 0 := by omega
-        simp only [residual, List.length_append, hxy, hy, hx, if_false, if_true]
+        simp only [residual, List.length_append, hxy, hy, hx, ite_false, ite_true]
         ext a
         simp only [Set.preimage_compl, compl_compl, subAt_body_image, subAtInf_append,
           Stream'.append_append_stream, Set.mem_preimage, Set.mem_image, Subtype.exists,
@@ -101,15 +101,15 @@ def payoff (p : Player) (G : Game A) : Set (body G.tree) := match p with
     · simp_all
       rfl
     · unfold Player.payoff Player.residual
-      rw [if_pos h, Game.residual_payoff_even G x h]
+      rw [ite_eq_left h, Game.residual_payoff_even G x h]
       ext y
       rfl
   · have hodd : x.length % 2 = 1 := Nat.mod_two_ne_zero.mp h
     cases p
     · simp_all
       rfl
     · unfold Player.payoff Player.residual
-      rw [if_neg h, Game.residual_payoff_odd G x hodd]
+      rw [ite_eq_right h, Game.residual_payoff_odd G x hodd]
       exact compl_compl (body.append x ⁻¹' G.payoff)
 end Player
 @[congr] lemma subtype_val_player_payoff {G' p'} (h : G = G') (hp : p = p') :

LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/CoveringClosedGame.lean

@@ -415,7 +415,7 @@ lemma gameTree_isPruned : IsPruned <| gameTree hyp := by
       exact ⟨⟨⊤, PreStrategy.top_isQuasi (hPr.sub _)⟩, PreStrategy.top_subtree.symm⟩
     · refine (gameTree_concat x ⟨a, subAt (getTree' hyp x) [a]⟩).mpr ⟨hx, ?_⟩
       unfold ValidExt
-      rw [if_neg hlen', dif_neg hlen]
+      rw [ite_eq_right hlen', dite_eq_right hlen]
       exact ⟨ha, rfl⟩
 
 variable (hyp) in

LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/Lift.lean

@@ -275,7 +275,7 @@ lemma concat_mem_tree {y a} (hp : IsPosition y Player.zero)
             ¬ H.game.WinningPosition
               (H.toLift.liftShort.val[2 * k + 1].1 :: (y ++ [b.val]))}
       else Set.univ)
-    rw [if_pos ⟨⟨a, hx⟩, by
+    rw [ite_eq_left ⟨⟨a, hx⟩, by
       change ¬ H.game.WinningPosition
         (H.toLift.liftShort.val[2 * k + 1].1 :: (y ++ [a]))
       exact hw⟩]
@@ -480,7 +480,7 @@ def a : ExtensionsAt h.x' := h.strat h.x' (by have := H.hlvl; synthIsPosition)
 def extension : ExtensionsAt H.x where
   val := (h.a hp).val
   property := by
-    have h' := (h.a hp).prop; conv at h' => simp [game]; conv => simp [game]
+    have h' := (h.a hp).prop; conv at h' => simp [game]
     simp_rw [← List.drop_drop (j := 2 * k + 1), ← List.append_assoc _ _ [_],
       List.take_append_drop] at h'; exact h'
 end Winnable
@@ -497,18 +497,18 @@ def extension (H : PreLift hyp) (hp : IsPosition H.x.val Player.one)
 lemma extension_won {H : PreLift hyp} (h : H.Won) hp R :
     H.extension hp R = h.lift'.extensionMap hp R := by
   unfold extension
-  exact dif_pos h
+  exact dite_eq_left h
 lemma extension_winnable {H : PreLift hyp} (hnWon : ¬ H.Won) (h : H.Winnable) hp R :
     H.extension hp R = h.extension hp := by
   unfold extension
-  exact (dif_neg hnWon).trans (dif_pos h)
+  exact (dite_eq_right hnWon).trans (dite_eq_left h)
 lemma extension_losable {H : PreLift hyp} (h : H.Losable) hp R :
   H.extension hp R = h.lift'.extensionMap hp R := by
   have hnWon : ¬ H.Won := fun hW ↦ h.1 (WLift.mk _ hW).winnable
   have hnWinnable : ¬ H.Winnable := fun hW ↦ h.1 hW
   classical
   unfold extension
-  exact (dif_neg hnWon).trans ((dif_neg hnWinnable).trans (dif_pos h))
+  exact (dite_eq_right hnWon).trans ((dite_eq_right hnWinnable).trans (dite_eq_left h))
 end PreLift
 
 end «Section1»

LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean

@@ -44,11 +44,11 @@ lemma mem_defensiveQuasi (x : G.tree) (h : ¬ WinningPrefix G p.swap x.val) hpr
   intro n hn hx hp _
   conv => simp [defensiveQuasi, extQuasi, tryAndElse, defensivePre, preserveProp, ExtensionsAt.val']
   split_ifs with hne
-  · refine Set.mem_of_subset_of_mem (if_pos hne).ge ?_
+  · refine Set.mem_of_subset_of_mem (ite_eq_left hne).ge ?_
     intro hW; apply h; use n + 1
     rwa [show Player.residual (List.take (n + 1) x.val) p.swap = Player.zero by synthIsPosition,
       ← List.take_concat_get' _ _ hn]
-  · exact Set.mem_of_subset_of_mem (if_neg hne).ge (Set.mem_univ _)
+  · exact Set.mem_of_subset_of_mem (ite_eq_right hne).ge (Set.mem_univ _)
 lemma winningPrefix_of_residual {x y : List A}
   (hW : WinningPrefix (G.residual x) p y) :
   WinningPrefix G (p.residual x) (x ++ y) := by
@@ -274,12 +274,10 @@ lemma winAsap_subtree {x} (h : WinningPrefix G p x) :
       rw [subtree_compatible_iff _ ⟨_, mem_of_append h'⟩
         (by as_aux_lemma => synthIsPosition)] at h'
       conv at h' => simp [winAsap, h.shrink.extend y]
-      conv => simp [winAsap, h.shrink.extend y]
       obtain ⟨_, h'⟩ := h'
       replace h' := congrArg Subtype.val (Set.eq_of_mem_singleton h')
       apply ExtensionsAt.ext (x := (PreStrategy.subtreeIncl _ ⟨_, _⟩)) --why necessary?
       rw [h']
-      conv => simp
       apply h.extend_strat_apply; apply h.hEq_drop_take
     · conv => simp [← List.append_assoc]
       rw [subtree_compatible_iff _ ⟨_, ih⟩ (by as_aux_lemma => synthIsPosition)]

LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/Lift.lean

@@ -197,8 +197,8 @@ lemma extension_conLong hp R : (hW.toWLift'.extensionLift hp R).ConLong := by
   have hget := congrArg (fun xs : List A => xs[2 * k + 1]?) ht
   change (List.take (2 * k + 2) (hW.toWLift'.extensionMap hp R).val')[2 * k + 1]? =
       (List.take (2 * k + 2) H.x.val)[2 * k + 1]? at hget
-  rw [List.getElem?_take, if_pos (by omega)] at hget
-  rw [List.getElem?_take, if_pos (by omega)] at hget
+  rw [List.getElem?_take, ite_eq_left (by omega)] at hget
+  rw [List.getElem?_take, ite_eq_left (by omega)] at hget
   have hleft : 2 * k + 1 < (hW.toWLift'.extensionMap hp R).val'.length := by
     have hlen := ExtensionsAt.val'_length (hW.toWLift'.extensionMap hp R)
     rw [hlen]
@@ -490,7 +490,6 @@ lemma take (hn : 1 ≤ h.2.num + n) :
   (H.take (2 * k + 1 + h.2.num + n) (by as_aux_lemma => omega)).Losable := by
   use H.conLong_take (h := by omega) h.1
   replace h := h.2
-  conv at h => simp [List.drop_take]
   conv => simp [List.drop_take]
   apply WinningPrefix.of_take (n := h.num)
   simpa (disch := omega) [List.take_take] using h.shrink
@@ -553,18 +552,18 @@ noncomputable def extension : ExtensionsAt H.x := by
 lemma extension_lost (h : H.Lost) :
   H.extension hp R = h.toLLift'.extensionMap hp R := by
   unfold extension
-  exact dif_pos h
+  exact dite_eq_left h
 lemma extension_losable (hnLost : ¬ H.Lost) (h : H.Losable) :
     H.extension hp R = h.extension hp := by
   unfold extension
-  exact (dif_neg hnLost).trans (dif_pos h)
+  exact (dite_eq_right hnLost).trans (dite_eq_left h)
 lemma extension_winnable (h : H.Winnable) :
   H.extension hp R = h.toWLift'.extensionMap hp R := by
   have hnLost : ¬ H.Lost := fun hL ↦ h (hL.1.mk.losable h.conLong).2
   have hnLosable : ¬ H.Losable := fun hL ↦ h hL.2
   classical
   unfold extension
-  exact (dif_neg hnLost).trans ((dif_neg hnLosable).trans (dif_pos h))
+  exact (dite_eq_right hnLost).trans ((dite_eq_right hnLosable).trans (dite_eq_left h))
 end Lift
 
 end «Section1»

LeanPool/AharoniKorman/Counterexample.lean

@@ -586,7 +586,7 @@ lemma image_chainBetween_isChain {a b c d n : ℕ} :
 open Finset in
 lemma card_chainBetween {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) :
     #(chainBetween a b c d) = c + d + 1 - (a + b) := by
-  rw [chainBetween, if_pos ⟨hac, hbd⟩, card_union_of_disjoint, Finset.card_Icc_prod]
+  rw [chainBetween, ite_eq_left ⟨hac, hbd⟩, card_union_of_disjoint, Finset.card_Icc_prod]
   · simp only [Icc_self, card_singleton, Nat.card_Icc]
     rw [← Finset.Ico_map_sectR, card_map, Nat.card_Ico]
     omega
@@ -892,14 +892,14 @@ noncomputable def x0y0 (n : ℕ) (C : Set Hollom) : ℕ × ℕ := by
 
 lemma x0y0_mem (h : (C ∩ level (n + 1)).Nonempty) :
     embed (n + 1) (x0y0 n C) ∈ C := by
-  rw [x0y0, dif_pos h]
+  rw [x0y0, dite_eq_left h]
   exact WellFounded.min_mem _ {x | embed (n + 1) x ∈ C} _
 
 lemma x0y0_min (z : ℕ × ℕ) (hC : IsChain (· ≤ ·) C) (h : embed (n + 1) z ∈ C) :
     embed (n + 1) (x0y0 n C) ≤ embed (n + 1) z := by
   have : (C ∩ level (n + 1)).Nonempty := ⟨_, h, by simp [level_eq_range]⟩
   refine isChain_le_of_not_lt hC h (x0y0_mem this) ?_
-  rw [x0y0, dif_pos this, OrderEmbedding.lt_iff_lt]
+  rw [x0y0, dite_eq_left this, OrderEmbedding.lt_iff_lt]
   exact wellFounded_lt.not_lt_min {x | embed (n + 1) x ∈ C} h
 
 /--
@@ -948,7 +948,7 @@ We will later show the same assuming `C ∩ level (n + 1)` is infinite.
 -/
 lemma square_subset_S_case_1 (h : (C ∩ level n).Finite) (h' : (C ∩ level (n + 1)).Finite) :
     ∀ᶠ a in atTop, embed n '' Set.Ici (a, a) ⊆ S n C \ (C ∩ level n) := by
-  rw [S, if_pos h']
+  rw [S, ite_eq_left h']
   -- Take a maximal pair `(b, c)` so that any `(d, e, n)` in `C` satisfies
   -- `(d, e, n) ≤ (b, c, n)`.
   obtain ⟨b, c, hab⟩ : ∃ b c, ∀ d e, h(d, e, n + 1) ∈ C → (d, e) ≤ (b, c) := by
@@ -983,7 +983,7 @@ We earlier showed the same assuming `C ∩ level (n + 1)` is finite.
 -/
 lemma square_subset_S_case_2 (h : (C ∩ level n).Finite) (h' : (C ∩ level (n + 1)).Infinite) :
     ∀ᶠ a in atTop, embed n '' Set.Ici (a, a) ⊆ S n C \ (C ∩ level n) := by
-  rw [S, if_neg h']
+  rw [S, ite_eq_right h']
   filter_upwards [eventually_ge_atTop (x0 n C + 1), eventually_ge_atTop (y0 n C + 1),
     square_subset_R h] with a hax hay haR
   simp [Set.subset_def, embed_apply] at *
@@ -1034,7 +1034,7 @@ theorem not_S_hits_next (f : SpinalMap C) (hC : IsChain (· ≤ ·) C)
   cases (C ∩ level (n + 1)).finite_or_infinite
   -- In the case that `C ∩ level (n + 1)` is finite, this is immediate from the definition of `S`.
   case inl h =>
-    rw [S, if_pos h, Set.mem_ofPred_eq] at hx
+    rw [S, ite_eq_left h, Set.mem_ofPred_eq] at hx
     intro hy
     refine f.incomp_apply ?_ (hx.2 _ hy).symm
     have := R_subset_level hx.1
@@ -1045,7 +1045,7 @@ theorem not_S_hits_next (f : SpinalMap C) (hC : IsChain (· ≤ ·) C)
   case inr h =>
     -- Write `(x, y, n)` for our given point, and set `(a, b, n + 1) := f(x, y, n)`
     induction S_subset_level hx using induction_on_level with | h x y =>
-    simp only [S, if_neg h, Set.mem_ofPred_eq, ofHollom_toHollom] at hx
+    simp only [S, ite_eq_right h, Set.mem_ofPred_eq, ofHollom_toHollom] at hx
     intro hp
     set fp := f h(x, y, n) with hfp
     clear_value fp
@@ -1169,7 +1169,8 @@ theorem not_S_mapsTo_previous (hC : IsChain (· ≤ ·) C)
     set c := f x with hc
     have hc' : c ∈ C ∩ level (n - 1) := h _ (F_subs hx)
     clear_value c
-    rw [coe_image, chainBetween, Ico_self, if_pos (by omega), empty_union, ← Icc_map_sectL] at hx
+    rw [coe_image, chainBetween, Ico_self, ite_eq_left (by omega), empty_union,
+      ← Icc_map_sectL] at hx
     simp only [embed_apply, coe_map, Function.Embedding.sectL_apply, coe_Icc,
       Set.mem_image, Set.mem_Icc, exists_exists_and_eq_and] at hx
     obtain ⟨b, ⟨hab, hba⟩, rfl⟩ := hx

LeanPool/AndersonConjecture/AdicNoetherian.lean

@@ -673,7 +673,7 @@ private def adicCompletion_ideal_fg_proof : PLift (
       have hcLim_spec : ∀ g, g ∈ genS → ∀ n,
           pc n g ≡ cLim g [SMOD (Mi ^ n • ⊤ : Submodule R (AdicCompletion Mi R))] := by
         intro g hg n
-        simpa only [cLim, dif_pos hg] using (hpc_lim g hg).choose_spec n
+        simpa only [cLim, dite_eq_left hg] using (hpc_lim g hg).choose_spec n
       -- Step 7: L = y₀ + ∑ cLim(g) * g by Hausdorff, hence L ∈ I₀
       suffices hL_eq : L = y₀ + sumG cLim from
         hL_eq ▸ I₀.add_mem hy₀ (hsum_in_I₀ cLim)
@@ -721,12 +721,12 @@ private def adicCompletion_ideal_fg_proof : PLift (
         rcases hg with hg | hg
         · rw [Finset.mem_image] at hg
           obtain ⟨a, ha, rfl⟩ := hg
-          rw [dif_pos ha, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
+          rw [dite_eq_left ha, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
           rw [hlJ_eq a ha]
           exact Ideal.subset_span ha
         · rw [Finset.mem_image] at hg
           obtain ⟨r, hr, rfl⟩ := hg
-          rw [dif_pos hr, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
+          rw [dite_eq_left hr, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
           have hr_pow : r ∈ Mi ^ n0 := hFN_le n0 (hS_F ▸ Ideal.subset_span hr)
           have : (evalₐ Mi n0) (lF r hr) =
             Ideal.Quotient.factorPow Mi (Nat.le_succ n0) (evalₐ Mi (n0 + 1) (lF r hr)) :=

LeanPool/AndersonConjecture/CompleteDomain/CompleteDomain.lean

@@ -340,7 +340,7 @@ lemma coeff_negSubst (g : MvPowerSeries (Fin 2) ℂ) (m : Fin 2 →₀ ℕ) :
     rw [hsum]
     ring
   · intro d hd
-    simp only [if_neg (Ne.symm hd), mul_zero]
+    simp only [ite_eq_right (Ne.symm hd), mul_zero]
 
 open MvPowerSeries in
 lemma ψHom_coeff_odd_parity (f : MvPowerSeries (Fin 3) ℂ)

LeanPool/AndersonConjecture/CompleteDomain/Domain.lean

@@ -235,7 +235,7 @@ lemma ψHom_coeff_sum
       mkFin3 (m₀ + 2 * k) (m₁ - k) (m₂ - k) 2) := by
     simp only [mkFin3_zero, mkFin3_one, mkFin3_two, he_def, mkFin2_inj]
     constructor <;> omega
-  rw [if_pos hcond]
+  rw [ite_eq_left hcond]
   rfl
 
 /-- Key lemma: ψbar is injective. This is equivalent to ker ψHom = conjI.
@@ -290,7 +290,7 @@ lemma ψBar_injective : Function.Injective ψBar := by
   -- Case on m 0 ≥ 2
   by_cases hm0 : 2 ≤ m 0
   · -- m 0 ≥ 2: telescoping
-    rw [if_pos (hd₀_iff.mpr hm0)]
+    rw [ite_eq_left (hd₀_iff.mpr hm0)]
     have sub0 : (m - d₀) 0 = m 0 - 2 := by simp [Finsupp.tsub_apply, d₀]
     have sub1 : (m - d₀) 1 = m 1 := by simp [Finsupp.tsub_apply, d₀]
     have sub2 : (m - d₀) 2 = m 2 := by simp [Finsupp.tsub_apply, d₀]
@@ -301,7 +301,7 @@ lemma ψBar_injective : Function.Injective ψBar := by
       simp only [divQ, sub0, sub1, sub2, show m 0 - 2 + 2 = m 0 from by omega]
     rw [hdivQ0]
     by_cases hm12 : 1 ≤ m 1 ∧ 1 ≤ m 2
-    · rw [if_pos (hd₁₂_iff.mpr hm12)]
+    · rw [ite_eq_left (hd₁₂_iff.mpr hm12)]
       have s0' : (m - d₁₂) 0 = m 0 := by simp [Finsupp.tsub_apply, d₁₂, Finsupp.add_apply]
       have s1' : (m - d₁₂) 1 = m 1 - 1 := by simp [Finsupp.tsub_apply, d₁₂, Finsupp.add_apply]
       have s2' : (m - d₁₂) 2 = m 2 - 1 := by simp [Finsupp.tsub_apply, d₁₂, Finsupp.add_apply]
@@ -329,7 +329,7 @@ lemma ψBar_injective : Function.Injective ψBar := by
       rw [Finset.sum_congr rfl hterms]
       ring
     · push Not at hm12
-      rw [if_neg (fun h => by
+      rw [ite_eq_right (fun h => by
                     simp_all)]
       simp only [sub_zero]
       have hmin0 : min (m 1) (m 2) = 0 := by
@@ -342,14 +342,14 @@ lemma ψBar_injective : Function.Injective ψBar := by
       rw [← mkFin3_ext]
   · -- m 0 < 2 (m 0 ≤ 1)
     have hm0' : m 0 ≤ 1 := by omega
-    rw [if_neg (fun h => by
+    rw [ite_eq_right (fun h => by
                   simp_all)]
     simp only [zero_sub]
     have hψ_sum : ∑ k ∈ Finset.range (min (m 1) (m 2) + 1),
         f (mkFin3 (m 0 + 2 * k) (m 1 - k) (m 2 - k)) = 0 := by
       rw [ψHom_coeff_sum f (m 0) (m 1) (m 2) hm0', hψ0, map_zero]
     by_cases hm12 : 1 ≤ m 1 ∧ 1 ≤ m 2
-    · rw [if_pos (hd₁₂_iff.mpr hm12)]
+    · rw [ite_eq_left (hd₁₂_iff.mpr hm12)]
       change f m = -(divQ f (m - d₁₂))
       simp only [divQ]
       have s0 : (m - d₁₂) 0 = m 0 := by simp [Finsupp.tsub_apply, d₁₂, Finsupp.add_apply]
@@ -370,7 +370,7 @@ lemma ψBar_injective : Function.Injective ψBar := by
       rw [mkFin3_inj]
       refine ⟨by ring, ?_, ?_⟩ <;> omega
     · push Not at hm12
-      rw [if_neg (fun h => by
+      rw [ite_eq_right (fun h => by
                     simp_all)]
       simp only [neg_zero]
       have : min (m 1) (m 2) = 0 := by