refactor(algebra): use Fintype sum zero criterion

TNLean/Algebra/MatrixAux.lean

@@ -78,7 +78,7 @@
 variable {ι n : Type*} [Fintype ι] [Fintype n]
 
 /-- If `∑ᵢ Bᵢ * Bᵢ† = 0`, then every `Bᵢ` is zero. -/
 theorem eq_zero_of_sum_mul_conjTranspose_eq_zero
     (B : ι → Matrix n n ℂ)
     (h : ∑ i : ι, B i * (B i)ᴴ = 0) :
     ∀ i, B i = 0 := by
@@ -92,8 +92,8 @@
     rw [← Complex.re_sum, ← Matrix.trace_sum, h]
     simp
   have htrace_re : ((B i * (B i)ᴴ).trace).re = 0 :=
-    Finset.sum_eq_zero_iff_of_nonneg (fun j _ => htrace_nonneg j)
-      |>.mp htrace_sum i (Finset.mem_univ i)
+    congrFun (Fintype.sum_eq_zero_iff_of_nonneg (fun j => htrace_nonneg j) |>.mp
+      htrace_sum) i
   have htrace_zero : (B i * (B i)ᴴ).trace = 0 :=
     Complex.ext htrace_re
       (Complex.le_def.mp (Matrix.posSemidef_self_mul_conjTranspose (B i)).trace_nonneg).2.symm

TNLean/Algebra/PerronFrobenius/RankOne.lean

@@ -86,8 +86,8 @@ private lemma exists_eq_one_of_sum_eq_one_sum_sq_eq_one_nonneg
       _ = 0 := by rw [h_sum, h_sq]; norm_num
   have hterm_zero : ∀ i, lam i * (1 - lam i) = 0 := by
     intro i
-    exact (Finset.sum_eq_zero_iff_of_nonneg
-      (fun j _ => hterm_nonneg j)).mp hsum_term i (Finset.mem_univ i)
+    exact congrFun (Fintype.sum_eq_zero_iff_of_nonneg
+      (fun j => hterm_nonneg j) |>.mp hsum_term) i
   have hex : ∃ i, lam i = 1 := by
     by_contra hno
     have hall_zero : ∀ i, lam i = 0 := by

TNLean/Channel/FixedPoint/Cesaro.lean

@@ -106,8 +106,9 @@ private theorem psd_orthogonal_difference_eq_zero
     have hre_sum : ∑ j, (star (e j) ⬝ᵥ Y.mulVec (e j)).re = 0 := by
       have h1 := map_sum Complex.reAddGroupHom (fun j => star (e j) ⬝ᵥ Y.mulVec (e j)) Finset.univ
       rw [← hY_tr_sum, hY_tr] at h1; exact h1.symm
-    have hre_zero := (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => hre_nonneg j)).mp hre_sum
-    intro j; exact Complex.ext (hre_zero j (Finset.mem_univ _)) (him j)
+    have hre_zero := congrFun
+      (Fintype.sum_eq_zero_iff_of_nonneg (fun j => hre_nonneg j) |>.mp hre_sum)
+    intro j; exact Complex.ext (hre_zero j) (him j)
   -- Y.mulVec(e_j) = 0 via dotProduct_mulVec_zero_iff for (A+Y) or (B+Y)
   have hY_mulVec_zero : ∀ j, Y.mulVec (e j) = 0 := by
     intro j; rcases he_ker j with hA_ker | hB_ker

TNLean/Channel/Irreducible/Growth/OneStep.lean

@@ -53,7 +53,7 @@
 of `A` therefore satisfies `(1-Q) K_i Q = 0` for all `i`, which gives
 `Q * E(Q X Q) * Q = E(Q X Q)` for all `X`. By irreducibility `Q ∈ {0, 1}`.
 Since `A ≠ 0` forces `Q ≠ 0`, we get `Q = 1`, i.e., `A` is PosDef. -/
 theorem posDef_of_ker_subset_irreducible_cp
     (E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ)
     (hCP : IsCPMap E) (hIrr : IsIrreducibleMap E)
     (A : Matrix (Fin D) (Fin D) ℂ)
@@ -88,8 +88,8 @@
             star ((K j')ᴴ *ᵥ v) ⬝ᵥ (A *ᵥ ((K j')ᴴ *ᵥ v))).re = 0 := by
           rw [← hsum]; simp [hqf_EA]
         rwa [Complex.re_sum] at this
-      have hre := (Finset.sum_eq_zero_iff_of_nonneg
-        (fun j' _ => hA_psd.re_dotProduct_nonneg _)).mp h_sum_re j (Finset.mem_univ _)
+      have hre := congrFun (Fintype.sum_eq_zero_iff_of_nonneg
+        (fun j' => hA_psd.re_dotProduct_nonneg _) |>.mp h_sum_re) j
       exact Complex.ext hre (hA_psd.isHermitian.im_star_dotProduct_mulVec_self _)
     exact (hA_psd.dotProduct_mulVec_zero_iff _).mp (h_each i)
   -- Step 2: Construct support projection Q = U * diag(sgn(λ)) * U†

TNLean/Channel/Semigroup/LiouvillianKernel.lean

@@ -384,8 +384,8 @@ private theorem each_commutator_eq_zero_of_sum_eq_zero
     have h_tr_re :
         ((A * F.L j - F.L j * A)ᴴ * (A * F.L j - F.L j * A)).trace.re = 0 :=
       le_antisymm
-        (by linarith [Finset.sum_eq_zero_iff_of_nonneg (fun k _ => h_each_nonneg k)
-            |>.mp h_tr_sum_re j (Finset.mem_univ j)])
+        (le_of_eq <| congrFun (Fintype.sum_eq_zero_iff_of_nonneg
+          (fun k => h_each_nonneg k) |>.mp h_tr_sum_re) j)
         (h_each_nonneg j)
     have h_tr_zero :
         ((A * F.L j - F.L j * A)ᴴ * (A * F.L j - F.L j * A)).trace = 0 :=

TNLean/MPS/Irreducible/FixedPointProjection.lean

@@ -266,8 +266,8 @@ private lemma ker_invariant_under_adjoint
       rw [← map_sum, ← hsum, hqf]
       exact Complex.zero_re
     have hre :=
-        (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => hρ_psd.re_dotProduct_nonneg _)).mp
-          h_sum_zero i (Finset.mem_univ _)
+        congrFun (Fintype.sum_eq_zero_iff_of_nonneg
+          (fun j => hρ_psd.re_dotProduct_nonneg _) |>.mp h_sum_zero) i
     exact Complex.ext hre (hρ_psd.isHermitian.im_star_dotProduct_mulVec_self _)
   intro i
   exact (hρ_psd.dotProduct_mulVec_zero_iff _).mp (h_each_zero i)

TNLean/QPF/PosDef.lean

@@ -79,8 +79,9 @@ private lemma ker_invariant_under_adjoint
     have h_sum_zero :
         ∑ j, RCLike.re (star ((A j)ᴴ *ᵥ x) ⬝ᵥ (ρ *ᵥ ((A j)ᴴ *ᵥ x))) = 0 := by
       rw [← map_sum, ← hsum, hqf]; simp
-    have hre := (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => hρ_psd.re_dotProduct_nonneg _)).mp
-      h_sum_zero i (Finset.mem_univ _)
+    have hre := congrFun
+      (Fintype.sum_eq_zero_iff_of_nonneg (fun j => hρ_psd.re_dotProduct_nonneg _) |>.mp
+        h_sum_zero) i
     exact Complex.ext hre (hρ_psd.isHermitian.im_star_dotProduct_mulVec_self _)
   intro i
   exact (hρ_psd.dotProduct_mulVec_zero_iff _).mp (h_each_zero i)