chore(deps): track CSLib main and Lean v4.36.0-rc2

Complexity/Algorithms/WordRAM/Karger/FastCut.lean

@@ -658,7 +658,7 @@ theorem two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α
       have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval
       have ha_hit : a ∈ hit₁ := not_not.mp ha_not_miss
       rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply]
-      refine ENNReal.tsum_eq_zero.mpr fun b => ?_
+      refine tsum_eq_zero_iff.mpr fun b => ?_
       by_cases hb_eval : b ∈ (m₂ a).eval.support
       · have hb : b ∈ (m₂ a).support := (ProbComp.support_eval (m₂ a)) ▸ hb_eval
         have hmem : f a b ∈ hit := hprop₁ a ha ha_hit b hb

Complexity/Algorithms/WordRAM/Karger/Graph.lean

@@ -1107,7 +1107,7 @@ theorem toOuterMeasure_bind_ge_mul_ennreal {α β : Type*} (p : PMF α) (kernel
     s₁ * s₂ ≤ p.toOuterMeasure pre * s₂ := mul_le_mul_of_nonneg_right hp zero_le
     _ ≤ (p.bind kernel).toOuterMeasure event := by
       rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right]
-      refine ENNReal.tsum_le_tsum fun a => ?_
+      refine tsum_le_tsum fun a => ?_
       by_cases ha : a ∈ pre
       · simp only [Set.indicator_of_mem ha]
         by_cases hs : a ∈ p.support
@@ -1131,7 +1131,7 @@ theorem toOuterMeasure_bind_le_mul_ennreal {α β : Type*} (p : PMF α) (kernel
     (p.bind kernel).toOuterMeasure failure
       ≤ p.toOuterMeasure stillFailing * q₂ := by
         rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right]
-        refine ENNReal.tsum_le_tsum fun a => ?_
+        refine tsum_le_tsum fun a => ?_
         by_cases hs : a ∈ p.support
         · by_cases ha : a ∈ stillFailing
           · simp only [Set.indicator_of_mem ha]
@@ -1146,7 +1146,7 @@ valid on arbitrary types without measurability hypotheses. -/
 theorem toOuterMeasure_add_compl_ennreal {α : Type*} (p : PMF α) (s : Set α) :
     p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1 := by
   classical
-  rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add]
+  rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add]
   have hpt : (fun x => s.indicator p x + sᶜ.indicator p x) = p := by
     ext x
     by_cases hx : x ∈ s <;> simp [hx]

Complexity/Algorithms/WordRAM/KargerMinCut.lean

@@ -1181,7 +1181,7 @@ theorem ampLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : 
         obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁
         rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply,
           PMF.toOuterMeasure_apply]
-        convert ENNReal.tsum_eq_zero.mpr _
+        refine tsum_eq_zero_iff.mpr ?_
         intro z₂
         by_cases hz₂_eval : z₂ ∈ m_r.eval.support
         · have hz₂ : z₂ ∈ m_r.support := (ProbComp.support_eval m_r) ▸ hz₂_eval

Complexity/Algorithms/WordRAM/KargerStein.lean

@@ -168,7 +168,7 @@ private theorem toOuterMeasure_mono_support {α : Type} (m : ProbComp α) {S T :
     m.eval.toOuterMeasure S ≤ m.eval.toOuterMeasure T := by
   classical
   rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply]
-  refine ENNReal.tsum_le_tsum fun a => ?_
+  refine tsum_le_tsum fun a => ?_
   by_cases ha : a ∈ S
   · simp only [Set.indicator_of_mem ha]
     by_cases hs : a ∈ m.support
@@ -2684,7 +2684,7 @@ theorem fastCutNode_spec {n w : ℕ} {W₀ : Fin n → Fin n → ℕ}
               have hcompl0 : (ms2_fn z₂.1).eval.toOuterMeasure
                   {zs | zs.1.regs retVal = minCut W₀}ᶜ = 0 := by
                 rw [PMF.toOuterMeasure_apply]
-                refine ENNReal.tsum_eq_zero.mpr fun zs => ?_
+                refine tsum_eq_zero_iff.mpr fun zs => ?_
                 by_cases hzs_ev : zs ∈ (ms2_fn z₂.1).eval.support
                 · have hzs : zs ∈ (ms2_fn z₂.1).support :=
                     (ProbComp.support_eval (ms2_fn z₂.1)) ▸ hzs_ev
@@ -3679,7 +3679,7 @@ theorem fastCutAmpLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem
         have hbv₁ : z₁.1.regs bestVal = minCut W := not_not.mp hhit
         obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁
         rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply]
-        refine ENNReal.tsum_eq_zero.mpr fun z₂ => ?_
+        refine tsum_eq_zero_iff.mpr fun z₂ => ?_
         by_cases hz₂_eval : z₂ ∈ m_r.eval.support
         · have hz₂ : z₂ ∈ m_r.support := (ProbComp.support_eval m_r) ▸ hz₂_eval
           have hbv₂ : z₂.1.regs bestVal = minCut W :=

Complexity/Computability/Circuit/Arithmetic/Determinant.lean

@@ -272,7 +272,9 @@ generic determinants has `n * n` variables, degree at most `n` and arithmetic ci
 `3 * n ^ 4 + 4` gates. -/
 theorem detFamily_mem_VP : detFamily K ∈ VP K := by
   choose c hc hsize using exists_circuit_det (K := K)
-  refine ⟨⟨by fun_prop, PolynomiallyBounded.id.mono_of_le fun n =>
+  refine ⟨⟨?_, PolynomiallyBounded.id.mono_of_le fun n =>
     totalDegree_det_genericMatrix_le n⟩, c, PolynomiallyBounded.mono_of_le (by fun_prop) hsize, hc⟩
+  change PolynomiallyBounded (fun n : ℕ => n * n)
+  fun_prop
 
 end Cslib.Circuits.Arithmetic

Complexity/Computability/Circuit/Bird.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Init
+public import Mathlib.LinearAlgebra.Matrix.Array
 public import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
 public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Complexity/Computability/Circuit/Quantum/Basic.lean

@@ -172,7 +172,7 @@ theorem place_apply (A : Fin k ↪ Fin n) (U : unitaryGroup (Fin k → Bool) ℂ
     (place A U : Matrix _ _ ℂ) y x =
       if ∀ j, (¬∃ i, A i = j) → y j = x j then (U : Matrix _ _ ℂ) (y ∘ A) (x ∘ A) else 0 := by
   simp only [place, MonoidHom.coe_mk, OneHom.coe_mk, submatrix_apply, kroneckerMap_apply,
-    splitEquiv_apply_fst, splitEquiv_apply_snd, one_apply, funext_iff, Subtype.forall]
+    splitEquiv_apply_fst, splitEquiv_apply_snd, Matrix.one_apply, funext_iff, Subtype.forall]
   split_ifs <;> simp
 
 namespace PlacedGate
@@ -281,7 +281,7 @@ theorem hadamardMatrix_mem_unitaryGroup : hadamardMatrix ∈ unitaryGroup Bool 
   rw [mem_unitaryGroup_iff]
   ext b c
   cases b <;> cases c <;>
-    simp [hadamardMatrix, mul_apply, star_eq_conjTranspose, Complex.conj_ofReal, h2, h1]
+    simp [hadamardMatrix, Matrix.mul_apply, star_eq_conjTranspose, Complex.conj_ofReal, h2, h1]
 
 theorem star_hadamardMatrix : star hadamardMatrix = hadamardMatrix := by
   ext b c

Complexity/Computability/Circuit/Rational/Wronskian.lean

@@ -148,7 +148,7 @@ lemma wronskian_order_of_distinct_orders {K : Type*} [Field K] [CharZero K]
       Matrix.det_mul_row (fun j => (f j).trailingCoeff)
         (Matrix.of fun i j : Fin h => ((f j).natTrailingDegree.descFactorial i.val : K))]
     exact mul_ne_zero (Finset.prod_ne_zero_iff.mpr fun j _ =>
-      trailingCoeff_nonzero_iff_nonzero.mpr (hf j)) (det_descFactorial_ne_zero _ hd)
+      trailingCoeff_ne_zero.mpr (hf j)) (det_descFactorial_ne_zero _ hd)
   have hB0 : B.det ≠ 0 := fun hz => by simp [hz] at hBc
   have hA0 : A.det ≠ 0 := hdet ▸ mul_ne_zero (pow_ne_zero _ X_ne_zero) hB0
   have hscale : A.det = X ^ (∑ i : Fin h, i.val) * wronskianFamily f := by

Complexity/Computability/Complexity/Classes/IP.lean

@@ -148,7 +148,7 @@ theorem acceptProb_eq_acceptProbWith (verifier : WordOracleComp Operation Bool)
 /-- The acceptance probability sums the masses of the accepting outcomes over final states. -/
 theorem acceptProb_eq_tsum (verifier : WordOracleComp Operation Bool) (P : Prover Operation) :
     acceptProb verifier P = ∑' s, P.run verifier P.init (true, s) := by
-  rw [acceptProb, PMF.map_apply, ENNReal.tsum_prod', tsum_bool]
+  rw [acceptProb, PMF.map_apply, tsum_prod', tsum_bool]
   simp
 
 /-- Private coins drawn before any message average the acceptance probabilities of the

Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean

@@ -413,7 +413,7 @@ private theorem card_filter_not_injective_div_le (n : ℕ) :
 private theorem tsum_map_mul {β γ : Type*} (μ : PMF β) (m : β → γ) (f : γ → ENNReal) :
     ∑' c, μ.map m c * f c = ∑' b, μ b * f (m b) := by
   simp only [PMF.map_apply, ENNReal.tsum_mul_right.symm]
-  rw [ENNReal.tsum_comm]
+  rw [tsum_comm]
   refine tsum_congr fun b => ?_
   rw [tsum_eq_single (m b)]
   · simp

Complexity/Computability/Complexity/Classes/IP/Guessing.lean

@@ -77,8 +77,8 @@ noncomputable def Prover.guessProb (P : Prover Unit) (s : P.State) (m : List Boo
 theorem Prover.guessProb_add_le_one (P : Prover Unit) (s : P.State) (m : List Bool) :
     P.guessProb s m false + P.guessProb s m true ≤ 1 := by
   simp only [Prover.guessProb, PMF.map_apply]
-  rw [← ENNReal.tsum_add, ← PMF.tsum_coe ((P.respond ((), m)).run s)]
-  refine ENNReal.tsum_le_tsum fun y => ?_
+  rw [← tsum_add, ← PMF.tsum_coe ((P.respond ((), m)).run s)]
+  refine tsum_le_tsum fun y => ?_
   by_cases h : List.take 1 y.1 = [false]
   · simp [h]
   · by_cases h' : List.take 1 y.1 = [true] <;> simp [h, h']
@@ -120,7 +120,7 @@ theorem acceptProb_guessingRound_le {message : Bool → ProbComp (List Bool)} {
         exact hclose _ fun m => PMF.coe_le_one _ _
     _ = ∑' m, ProbComp.eval (message false) m *
           (P.guessProb P.init m false + P.guessProb P.init m true) + δ := by
-        rw [← add_assoc, ← ENNReal.tsum_add]
+        rw [← add_assoc, ← tsum_add]
         simp only [mul_add]
     _ ≤ 1 + δ := by
         gcongr

Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean

@@ -304,7 +304,7 @@ private theorem sum_acceptFrom_after_le (hF : IsBounded F D L) (P : Prover Unit)
       lia
     rw [Finset.sum_eq_zero fun m _ => ?_, add_zero]
     · split_ifs <;> simp
-    · refine ENNReal.tsum_eq_zero.mpr fun ys => ?_
+    · refine tsum_eq_zero_iff.mpr fun ys => ?_
       rw [after_append]
       unfold outcome at hnil
       rcases hah : after (F r) h with _ | ⟨b⟩ | ⟨q, next⟩
@@ -320,12 +320,12 @@ private theorem sum_acceptFrom_after_le (hF : IsBounded F D L) (P : Prover Unit)
       exact (Finset.sum_congr rfl fun r _ => by split_ifs <;> simp).le
     rw [Finset.sum_comm]
     refine Finset.sum_le_sum fun m _ => ?_
-    rw [← Summable.tsum_finsetSum fun r _ => ENNReal.summable]
+    rw [← Summable.tsum_finsetSum fun r _ => CompleteLattice.summable]
     calc ∑' ys : List Bool × P.State, ∑ r, (P.respond ((), m)).run s ys *
           acceptFrom P ys.2 (after (F r) (h ++ [(m, ys.1)]))
         ≤ ∑' ys : List Bool × P.State, (P.respond ((), m)).run s ys *
           ((BitString.shortWords L).sup fun y => value F L n (h ++ [(m, y)]) : ℕ) := by
-          refine ENNReal.tsum_le_tsum fun ys => ?_
+          refine tsum_le_tsum fun ys => ?_
           rw [← Finset.mul_sum]
           refine mul_le_mul_right ?_ _
           refine (ih (h ++ [(m, ys.1)]) (by
@@ -395,7 +395,7 @@ private theorem sum_acceptFrom_optimalProver_after (hF : IsBounded F D L) (n : 
       lia
     rw [Finset.sum_eq_zero fun m _ => ?_, add_zero]
     · split_ifs <;> simp
-    · refine ENNReal.tsum_eq_zero.mpr fun ys => ?_
+    · refine tsum_eq_zero_iff.mpr fun ys => ?_
       rw [after_append]
       unfold outcome at hnil
       rcases hah : after (F r) h with _ | ⟨b⟩ | ⟨q, next⟩

Complexity/Computability/Complexity/Classes/IP/Repetition.lean

@@ -64,7 +64,7 @@ private theorem acceptProb_bind_ite (P : Prover Operation)
     acceptProb (do let ok ← round; if ok then rest else pure false) P =
       ∑' s, P.run round P.init (true, s) * acceptProb rest { P with init := s } := by
   simp only [acceptProb, Prover.run_bind, PMF.map_bind]
-  rw [PMF.bind_apply, ENNReal.tsum_prod', tsum_bool]
+  rw [PMF.bind_apply, tsum_prod', tsum_bool]
   simp only [Bool.false_eq_true, Bool.true_eq_false, ↓reduceIte, Prover.run_pure, PMF.pure_map,
     PMF.pure_apply, mul_zero, tsum_zero, zero_add]
   rfl
@@ -81,7 +81,7 @@ theorem acceptProb_sequentialRepeat_le {round : WordOracleComp Operation Bool} {
     calc ∑' s, P.run round P.init (true, s) *
           acceptProb (sequentialRepeat k round) { P with init := s }
         ≤ ∑' s, P.run round P.init (true, s) * ε ^ k :=
-          ENNReal.tsum_le_tsum fun s => mul_le_mul' le_rfl (ih _)
+          tsum_le_tsum fun s => mul_le_mul' le_rfl (ih _)
       _ = (∑' s, P.run round P.init (true, s)) * ε ^ k := ENNReal.tsum_mul_right
       _ ≤ ε * ε ^ k := by
           gcongr
@@ -103,7 +103,7 @@ theorem le_acceptProb_sequentialRepeat {round : WordOracleComp Operation Bool} {
           gcongr
           exact (h s).trans_eq (acceptProb_eq_tsum round _)
       _ = ∑' s', P.run round s (true, s') * c ^ k := ENNReal.tsum_mul_right.symm
-      _ ≤ _ := ENNReal.tsum_le_tsum fun s' => mul_le_mul' le_rfl (ih s')
+      _ ≤ _ := tsum_le_tsum fun s' => mul_le_mul' le_rfl (ih s')
 
 /-- A constant number of sequential runs of a strict oracle PPT verifier is strict oracle PPT. -/
 theorem isOraclePPTOn_sequentialRepeat [DecidableEq Operation] [Finite Operation]

Complexity/Computability/Complexity/Classes/LogSpace/Randomized/Amplification.lean

@@ -126,7 +126,7 @@ theorem eval_runClosed_orElse_apply (h₁ : first.toNTM.RunsInTime input t₁)
           exact congrArg _ (PMF.pure_apply_self _)
         · rw [add_zero]
     _ = q + ProbComp.eval (first.runClosed t₁ input) [true] * (1 - q) := by
-        rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, tsum_ite_eq]
+        rw [tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, tsum_ite_eq]
 
 /-- **Rejections multiply under `orElse`.** Counted on coin strings, the probability that
 `first.orElse second` does not accept is the product of the probabilities that `first` and

Complexity/Computability/Complexity/Classes/MIP/OptimalProver.lean

@@ -581,7 +581,7 @@ private theorem tsum_mul_le_bestOfList (μ : PMF α) (g : α → ℝ≥0∞) (de
     ∑' x, μ x * g x ≤ g (bestOfList g default l) := by
   calc ∑' x, μ x * g x
       ≤ ∑' x, μ x * g (bestOfList g default l) := by
-        refine ENNReal.tsum_le_tsum fun x => ?_
+        refine tsum_le_tsum fun x => ?_
         by_cases hx : x ∈ μ.support
         · exact mul_le_mul_right (le_bestOfList g default l (hsupp x hx)) (μ x)
         · rw [PMF.mem_support_iff, not_not] at hx
@@ -618,7 +618,7 @@ theorem exists_deterministic_prover_family [Finite ι] [DecidableEq ι] {γ : Ty
       rw [run_eq_bind_piPresample (hF c) P (fun _ => d) (fun _ => le_rfl)
         (Prover.independent P).init, PMF.bind_apply]
     simp only [hc, ← ENNReal.tsum_mul_left]
-    rw [← Summable.tsum_finsetSum fun _ _ => ENNReal.summable]
+    rw [← Summable.tsum_finsetSum fun _ _ => CompleteLattice.summable]
     refine tsum_congr fun f => ?_
     rw [Finset.mul_sum]
     exact Finset.sum_congr rfl fun c _ => by rw [mul_left_comm]

Complexity/Computability/Complexity/FineGrained/PPSZ/Basic.lean

@@ -276,7 +276,7 @@ theorem ppz_round_apply_le {φ : CNF (Fin n)} {w : ℕ} (hw : 1 ≤ w) {σ : Fin
     (hσ : φ.eval σ = true) :
     PPZ.round φ (fun x => some (σ x)) ≤ round φ w (fun x => some (σ x)) := by
   rw [PPZ.round, round, PPZ.roundWith, PPZ.roundWith, PMF.bind_apply, PMF.bind_apply]
-  refine ENNReal.tsum_le_tsum fun π => mul_le_mul_right ?_ _
+  refine tsum_le_tsum fun π => mul_le_mul_right ?_ _
   rw [← PPZ.restrict_prefixSet_self σ π]
   rw [PPZ.runWith_apply_restrict (O := PPZ.forced φ) (fun _ hτ _ _ h => PPZ.forced_eq hσ hτ h) π
     le_rfl, PPZ.runWith_apply_restrict (O := implied φ w) (fun _ hτ _ _ h => implied_eq hσ hτ h) π

Complexity/Computability/Complexity/FineGrained/PPZ.lean

@@ -458,7 +458,7 @@ theorem runWith_apply_restrict {O : (Fin n → Option Bool) → Fin n → Option
       by_cases hsupp : τ ∈ (runWith O π i).support
       · rw [PMF.map_apply]
         convert mul_zero _
-        refine ENNReal.tsum_eq_zero.mpr fun b => ite_eq_right fun e => hτ ?_
+        refine tsum_eq_zero_iff.mpr fun b => ite_eq_right fun e => hτ ?_
         funext y
         by_cases hy : y = x
         · subst hy

Complexity/Computability/Interactive/Plain.lean

@@ -202,9 +202,9 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s)
           st'
     calc ∑' c, ProbComp.eval smp.1 c * _ ≤
           ∑' c, ProbComp.eval smp.1 c * (A.indicator 1 c + PerChallenge.sum s ε.2) :=
-          ENNReal.tsum_le_tsum fun c => by gcongr; exact hinner c
+          tsum_le_tsum fun c => by gcongr; exact hinner c
       _ = (ProbComp.eval smp.1).toOuterMeasure A + PerChallenge.sum s ε.2 := by
-          simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul,
+          simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul,
             PMF.toOuterMeasure_apply]
           congr 1
           refine tsum_congr fun c => ?_

Complexity/Computability/Kolmogorov/AverageCase.lean

@@ -277,7 +277,7 @@ private theorem pmf_map_true_le_one_sub_of_imp_false {α : Type*} (q : PMF α) (
     ((q.map P) true).toReal ≤ 1 - ((q.map Q) true).toReal := by
   have hle : (q.map P) true ≤ (q.map Q) false := by
     rw [PMF.map_apply, PMF.map_apply]
-    refine ENNReal.tsum_le_tsum fun v => ?_
+    refine tsum_le_tsum fun v => ?_
     by_cases hp : P v = true
     · have hq : Q v = false := hdisj v hp
       simp [hp, hq]
@@ -292,7 +292,7 @@ private theorem pmf_map_true_le_of_imp_true {α : Type*} (q : PMF α) (P Q : α
     ((q.map P) true).toReal ≤ ((q.map Q) true).toReal := by
   apply ENNReal.toReal_mono (PMF.apply_ne_top _ _)
   rw [PMF.map_apply, PMF.map_apply]
-  refine ENNReal.tsum_le_tsum fun v => ?_
+  refine tsum_le_tsum fun v => ?_
   by_cases hp : P v = true
   · have hq : Q v = true := himp v hp
     simp [hp, hq]

Complexity/Computability/PCP/TwoProverGame.lean

@@ -117,7 +117,7 @@ theorem winProb_shared_le_value [Nonempty A] [Nonempty B] {R : Type*} (ρ : PMF
     exact ENNReal.ofReal_le_ofReal (G.winProb_le_value (fun x => ha x r) (fun y => hb y r))
   calc ∑' r, ρ r * (G.questions.map fun q => (q, ha q.1 r, hb q.2 r)).toOuterMeasure
         {z | G.accepts z.1.1 z.1.2 z.2.1 z.2.2}
-      ≤ ∑' r, ρ r * ENNReal.ofReal G.value := ENNReal.tsum_le_tsum fun r => by gcongr; exact hr r
+      ≤ ∑' r, ρ r * ENNReal.ofReal G.value := tsum_le_tsum fun r => by gcongr; exact hr r
     _ = ENNReal.ofReal G.value := by rw [ENNReal.tsum_mul_right, ρ.tsum_coe, one_mul]
 
 end Finite

Complexity/Computability/WordRAM/Randomized/Expected.lean

@@ -117,7 +117,7 @@ theorem evalRand_haltedSet_mono (w : ℕ) (p : Program B r) (s : State r) :
     rw [evalRand, runRand_add w p T 1, ProbComp.eval_bind]
     simp only [evalRand, runRand_succ, runRand_zero, bind_pure]
   rw [hstep, PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply]
-  refine ENNReal.tsum_le_tsum fun cfg => ?_
+  refine tsum_le_tsum fun cfg => ?_
   by_cases hcfg : cfg ∈ RandCfg.haltedSet r
   · have hmem := hcfg
     obtain ⟨v, d, rfl⟩ := hcfg
@@ -139,7 +139,7 @@ theorem RandHaltsWithin.almostSurelyHalts {w T : ℕ} {p : Program B r} {s : Sta
     exact hnot (h cfg hmem)
   have hsum : (evalRand w p T s).toOuterMeasure (RandCfg.haltedSet r) +
       (evalRand w p T s).toOuterMeasure (RandCfg.haltedSet r)ᶜ = 1 := by
-    rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add]
+    rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add]
     convert (evalRand w p T s).tsum_coe using 1
     congr 1
     funext cfg
@@ -172,7 +172,7 @@ theorem expectedStepsFrom_faulted (w : ℕ) (p : Program B r) :
 
 private theorem tsum_nat_eq_zero_add (g : ℕ → ℝ≥0∞) :
     ∑' t : ℕ, g t = g 0 + ∑' t : ℕ, g (t + 1) := by
-  rw [ENNReal.tsum_eq_add_tsum_ite (f := g) 0]
+  rw [tsum_eq_add_tsum_ite (f := g) 0]
   congr 1
   have hsh := Function.Injective.tsum_eq Nat.succ_injective
     (f := fun t => if t = 0 then 0 else g t) fun t ht => by
@@ -199,7 +199,7 @@ theorem expectedStepsFrom_running (w : ℕ) (p : Program B r) (s : State r) :
     intro t
     rw [runRand_succ, ProbComp.eval_bind, PMF.toOuterMeasure_bind_apply]
   simp only [hsucc]
-  rw [ENNReal.tsum_comm]
+  rw [tsum_comm]
   simp only [ProbComp.expect, expectedStepsFrom, ENNReal.tsum_mul_left]
 
 /-- Under `RandFaultFree`, every horizon partitions probability `1` between `.running` and
@@ -208,7 +208,7 @@ theorem RandFaultFree.running_add_halted_eq_one {w : ℕ} {p : Program B r} {s :
     (hf : RandFaultFree w p s) (t : ℕ) :
     (evalRand w p t s).toOuterMeasure {cfg | ∃ u, cfg = .running u} +
       (evalRand w p t s).toOuterMeasure (RandCfg.haltedSet r) = 1 := by
-  rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add]
+  rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add]
   convert (evalRand w p t s).tsum_coe using 1
   congr 1
   funext cfg
@@ -242,7 +242,7 @@ theorem AlmostSurelyHalts.of_expectedTime_ne_top {w : ℕ} {p : Program B r} {s
   have hinf : (⊤ : ℝ≥0∞) ≤ expectedTime w p s := by
     calc
       (⊤ : ℝ≥0∞) = ∑' _ : ℕ, (1 - supH) := (ENNReal.tsum_const_eq_top_of_ne_zero hpos.ne').symm
-      _ ≤ expectedTime w p s := ENNReal.tsum_le_tsum hle_run
+      _ ≤ expectedTime w p s := tsum_le_tsum hle_run
   exact htop (top_unique hinf)
 
 /-- Under `RandHaltsWithin w p s T`, the active-configuration tail sum vanishes from `T` onward and