How to prove (x - 1).val = x.val - 1

Stream: new members

[Xintao Yu]

import Mathlib.Analysis.BoxIntegral.Partition.Basic
import Mathlib.Data.Finset.Sups
import Mathlib.MeasureTheory.Measure.FiniteMeasure
import Mathlib.Data.Fin.SuccPred

variable {n : ℕ} [NeZero n] -- n no of slices

#check Fin.coe_sub_one
--Fin.coe_sub_one {n : ℕ} (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else ↑a - 1
lemma QAQ (x : Fin n)(g : x > 0)(Spe : n > 1) : (x - 1).val = x.val - 1 := sorry

[Xintao Yu]

I searched for existing theorems in the Mathlib library, and Fin.coe_sub_one is the closest one, but I still don't know how to convert Fin n+1 to Fin n, both rewrite and refine seem to be unusable

[Richard Copley]

First show that there exists some m such that m + 1 = n.

[Xintao Yu]

Richard Copley said:

First show that there exists some m such that m + 1 = n.

Thank you for your reply, actually I've tried this thought before, but maybe because I did not use the \exist to prove?
I'll try it tomorrow, and hope to get more guidance from you!

[Xintao Yu]

I tried to prove QAQ in a more basic way but was still confused with some details

import Mathlib.Analysis.BoxIntegral.Partition.Basic
import Mathlib.Data.Finset.Sups
import Mathlib.MeasureTheory.Measure.FiniteMeasure
import Mathlib.Data.Fin.SuccPred

variable {n : ℕ} [NeZero n] -- n no of slices


--Fin.coe_sub_one {n : ℕ} (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else ↑a - 1
lemma QAQ (x : Fin n)(g : x > 0)(Spe : n > 1) : (x - 1).val = x.val - 1 := by
  rw [sub_eq_add_neg]
  rw [Fin.val_add_eq_ite]
  have g₁ : (-1 : Fin n).val = n - 1 := by
    rw [Fin.coe_neg]
    have g₂ : (1 : Fin n).val = 1 := sorry
    rw [g₂]
    rw [Nat.mod_eq_of_lt]
    cases n
    · exact Nat.lt_trans Nat.le.refl Spe
    · exact Nat.le.refl
  rw [g₁]
  rw [if_pos]
  · sorry
  · have : x.val ≠ 0 := sorry
    apply Nat.le_add_pred_of_pos n this

[Xintao Yu]

Here is the result :

lemma QAQ (x : Fin n)(g : x > 0)(Spe : n > 1) : (x - 1).val = x.val - 1 := by
  rw [sub_eq_add_neg]
  rw [Fin.val_add_eq_ite]
  have g₁ : (-1 : Fin n).val = n - 1 := by
    rw [Fin.coe_neg]
    have g₂ : (1 : Fin n).val = 1 := by
      simp
      exact Nat.mod_eq_of_lt Spe
    rw [g₂]
    rw [Nat.mod_eq_of_lt]
    cases n
    · exact Nat.lt_trans Nat.le.refl Spe
    · exact Nat.le.refl
  rw [g₁]
  rw [if_pos]
  · rw [add_comm]
    apply Nat.sub_eq_of_eq_add
    calc
      n - 1 + x.val = n + x.val - 1 := by rw [← Nat.sub_add_comm (show 1 ≤ n by exact Nat.le_of_lt Spe)]
      _ = x.val + n - 1 := by rw [add_comm]
      _ = x.val - 1 + n := Nat.sub_add_comm g
  · have : x.val ≠ 0 := by
      exact Nat.pos_iff_ne_zero.mp g
    apply Nat.le_add_pred_of_pos n this

[Damiano Testa]

Here is a shorter alternative, if you prefer:

lemma QAQ (x : Fin n)(g : x > 0)(Spe : n > 1) : (x - 1).val = x.val - 1 := by
  rw [Fin.coe_sub, Fin.val_one', Nat.mod_eq_of_lt Spe, ← Nat.add_sub_assoc Spe.le, add_comm,
    Nat.mod_eq_sub_mod, Nat.add_sub_assoc (by exact g), Nat.add_sub_cancel_left]
  · exact Nat.mod_eq_of_lt (by omega)
  · exact Nat.le_sub_of_add_le <| Nat.add_le_add Nat.le.refl g