brgcPath_injective

formal source

  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
  98      have hright_inj : Function.Injective right := by
  99        intro a b hab
 100        have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
 101          funext k
 102          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab