refactor(Analysis): golf Mathlib/Analysis/Convex/Birkhoff (#39893)

- refactors `Convex/Birkhoff` by removing the `Linarith` import and shortening the support-shrinking argument in `doublyStochastic_sum_perm_aux`

Extracted from #37968

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/Analysis/Convex/Birkhoff.lean

@@ -11,7 +11,6 @@ public import Mathlib.Analysis.Convex.Jensen
 public import Mathlib.Analysis.Normed.Module.Convex
 public import Mathlib.Combinatorics.Hall.Basic
 public import Mathlib.Analysis.Convex.DoublyStochasticMatrix
-public import Mathlib.Tactic.Linarith
 
 /-!
 # Birkhoff's theorem
@@ -126,15 +125,11 @@ private lemma doublyStochastic_sum_perm_aux (M : Matrix n n R)
     gcongr
     rw [ssubset_iff_of_subset (monotone_filter_right _ _)]
     · simp_rw [mem_filter_univ, not_not, Prod.exists]
-      refine ⟨i, σ i, hMi'.ne', ?_⟩
-      simp [N, Equiv.toPEquiv_apply]
+      exact ⟨i, σ i, hMi'.ne', by simp [N, Equiv.toPEquiv_apply]⟩
     · rintro ⟨i', j'⟩ _ hN' hM'
-      dsimp at hN' hM'
-      simp only [sub_apply, hM', smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply,
-        Option.mem_def, Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, zero_sub,
-        neg_eq_zero, ite_eq_right_iff, Classical.not_imp, N] at hN'
-      obtain ⟨rfl, _⟩ := hN'
-      linarith [hi' i' (by simp)]
+      have hσ' : σ i' ≠ j' := by
+        simpa [Equiv.toPEquiv_apply] using hσ i' j' hM'
+      exact hN' <| by simp [N, hM', hσ', Equiv.toPEquiv_apply]
   obtain ⟨w, hw, hw'⟩ := ih _ hd' _ s' hs' this rfl
   refine ⟨w + fun σ' => if σ' = σ then M i (σ i) else 0, ?_⟩
   simp only [Pi.add_apply, add_smul, sum_add_distrib, hw', ite_smul, zero_smul,