int_eq_of_natAbs_eq_zero

formal source

 770        exact not_le_of_gt this
 771      exact (this hznn).elim
 772
 773private lemma int_eq_of_natAbs_eq_zero {z : ℤ} (hz : Int.natAbs z = 0) : z = 0 := by
 774  exact (Int.natAbs_eq_zero.mp hz)
 775
 776private lemma exists_unique_of_sum_univ_eq_one {d : Nat} (f : Fin d → Nat)
 777    (hs : (∑ i : Fin d, f i) = 1) :
 778    ∃ k : Fin d, f k = 1 ∧ ∀ i : Fin d, i ≠ k → f i = 0 := by
 779  classical
 780  have hs_ne0 : (∑ i : Fin d, f i) ≠ 0 := by
 781    simpa [hs] using Nat.one_ne_zero
 782  obtain ⟨k, _hkMem, hkne0⟩ := Finset.exists_ne_zero_of_sum_ne_zero (s := (Finset.univ : Finset (Fin d)))
 783    (f := fun i => f i) hs_ne0
 784  have hdecomp : f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 1 := by
 785    -- `f k + sum (erase k) = sum univ`
 786    have := (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fun i => f i) (a := k) (by simp))
 787    simpa [hs] using this
 788  have hk_cases := Nat.add_eq_one_iff.mp hdecomp
 789  have hk1 : f k = 1 ∧ Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
 790    cases hk_cases with
 791    | inl h0 =>
 792        -- f k = 0 contradicts hkne0
 793        exfalso
 794        exact hkne0 h0.1
 795    | inr h1 =>
 796        exact h1
 797  refine ⟨k, hk1.1, ?_⟩
 798  intro i hik
 799  have hi' : i ∈ (Finset.univ.erase k : Finset (Fin d)) := by
 800    simp [Finset.mem_erase, hik]
 801  -- sum=0 on erase ⇒ every term on erase is 0
 802  have hall0 :
 803      ∀ j : Fin d, j ∈ (Finset.univ.erase k : Finset (Fin d)) → f j = 0 := by