Prove equality of sums over Fin n

Stream: new members

[uhr]

Im working with sums over Fin n for some n : Nat, and I am stuck with two sums, that should be equal (and look exactly equal in lean4 infoview), but I do not know how to prove that.

I am stuck with the goal ⊢ ↑xz = ↑xz - ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) + ∑ x : Fin nn, k (Fin.castLE _ ↑↑x).
It would be sufficient to prove that  ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) = ∑ x : Fin nn, k (Fin.castLE _ ↑↑x).

Minimal working example:

import Mathlib
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.Basic
open BigOperators
open Nat

lemma lemma1 {n m: Nat} {k : Fin n → Nat}  {xz : Fin (∑ i : Fin n, k i)}  :
 ∃ j : (Fin (n)) , ∃ m : Fin ( k  j), xz =( ∑ i1 : Fin j.val, k ( Fin.castLE (Fin.is_lt j) i1)) + m := by
induction n with
| zero =>
  /-
  some code
  -/
  sorry

| succ nn ih =>
  let  q := ∑ ii : Fin nn, k ( Fin.castLE (Fin.is_lt nn) ii) ;
  match le_or_lt q ( xz.val)  with
  |Or.inl q_leq_x =>

    use Fin.mk nn (Nat.lt_succ_self nn)


    have x_minus_q_le_knn : xz - q < k (Fin.mk nn (Nat.lt_succ_self nn)):=
      by sorry

    use Fin.mk (xz-q) x_minus_q_le_knn

    ring_nf
    rw[add_comm]

    -- ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) and ∑ x : Fin nn, k (Fin.castLE _ ↑↑x) are equal. How to prove that?
    -- this rewritte fails
    rw[sub_add_cancel]
    sorry

  | Or.inr x_le_q =>
    /-
  some code
  -/
    sorry

[Daniel Weber]

The problem is that a - b + b = a isn't correct in general for Nat, because subtraction is truncating (note that docs#sub_add_cancel requires AddGroup A, but Nat isn't an additive group). You can use docs#Nat.sub_add_cancel.