oneBitDiff_snocBit_flip

formal source

 140        have : j = k := hkuniq j hj'
 141        simpa [this]
 142
 143private theorem oneBitDiff_snocBit_flip {d : Nat} (p : Pattern d) :
 144    OneBitDiff (snocBit p false) (snocBit p true) := by
 145  classical
 146  refine ⟨Fin.last d, ?_, ?_⟩
 147  · simp
 148  · intro j hj
 149    induction j using Fin.lastCases with
 150    | last => rfl
 151    | cast j =>
 152        have : False := by
 153          -- on old coordinates the patterns are equal
 154          simpa [snocBit] using hj
 155        exact this.elim
 156
 157/-! ### Relating `natAdd` vs `addNat` when the sizes match -/
 158
 159private lemma natAdd_eq_addNat {T : Nat} (k : Fin T) :
 160    (Fin.natAdd T k : Fin (T + T)) = k.addNat T := by
 161  apply Fin.ext
 162  -- both sides represent the same natural number `T + k`
 163  simp [Fin.natAdd, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
 164
 165private lemma rev_add_one_eq {n : Nat} [NeZero n] {i : Fin n} (hi : i.val + 1 < n) :
 166    Fin.rev (i + 1) + 1 = Fin.rev i := by
 167  classical
 168  apply Fin.ext
 169  have hival : (i + 1).val = i.val + 1 :=
 170    Fin.val_add_one_of_lt' (n := n) (i := i) hi
 171  have hle1 : i.val + 1 ≤ n := Nat.le_of_lt hi
 172  have hle2 : i.val + 2 ≤ n := Nat.succ_le_of_lt hi
 173  have hnat : (n - (i.val + 2)) + 1 = n - (i.val + 1) := by