cast_add_one

formal source

  64
  65/-! ## Injectivity (no repeats) -/
  66
  67private lemma cast_add_one {n m : Nat} [NeZero n] [NeZero m] (h : n = m) (i : Fin n) :
  68    (i + 1).cast h = (i.cast h) + 1 := by
  69  subst h
  70  simp
  71
  72theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
  73  | 0 => by
  74      intro i j _
  75      -- `Fin 1` is a subsingleton (only `0`)
  76      simpa [Fin.eq_zero i, Fin.eq_zero j]
  77  | (d + 1) => by
  78      intro i j hij
  79      -- unfold the `d+1` definition and reduce to injectivity of the appended halves
  80      classical
  81      let T : Nat := 2 ^ d
  82      have hTT : 2 ^ (d + 1) = T + T := by
  83        simpa [T, twoPow_succ_eq_add d]
  84      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
  85      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
  86      have hij' :
  87          Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
  88        simpa [brgcPath, T, hTT, left, right] using hij
  89
  90      have hleft_inj : Function.Injective left := by
  91        intro a b hab
  92        have hab' : brgcPath d a = brgcPath d b := by
  93          funext k
  94          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
  95          simpa [left, snocBit] using this
  96        exact (brgcPath_injective d) hab'
  97