Help to prove ( h : n > 1 ) ( 1 : Fin n ).val = 1

Stream: new members

[Xintao Yu]

It is useless to directly rw [Fin.val_one (n := n - 2)] because Lean does not know if n - 2 + 2 = n ?

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

lemma g₂ : (1 : Fin n).val = 1 := by sorry
      -- rw [Fin.val_one (n := n - 2)]

[Riccardo Brasca]

This is false in the case n=1, and this is the reason why n-2 appears.

[Riccardo Brasca]

Note that in the title of the topic you write n > 1, but not in your code.

[Xintao Yu]

Ah! Thank you for your reply! You are right. 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

[Riccardo Brasca]

You can golf it like this

lemma QAQ (x : Fin n)(g : x > 0)(Spe : n > 1) : (x - 1).val = x.val - 1 := by
  obtain ⟨a, ha⟩ : ∃ a, n = a - 2 + 2 := ⟨n, (Nat.sub_add_cancel Spe).symm⟩
  subst ha
  rw [(Fin.coe_sub_iff_le (n := a - 2 + 2) (b := 1)).2
    (Fin.le_def.2 <| Nat.one_le_of_lt (Fin.lt_def.1 g))]
  simp

[Riccardo Brasca]

The trick is to replace n by a -2 + 2 for some a (of course a = n, but Lean complains if you use n), and then everything is much easier.