natAdd_eq_addNat

formal source

 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
 174    have h :
 175        ((n - (i.val + 2)) + 1) + (i.val + 1) = (n - (i.val + 1)) + (i.val + 1) := by
 176      calc
 177        ((n - (i.val + 2)) + 1) + (i.val + 1)
 178            = (n - (i.val + 2)) + (1 + (i.val + 1)) := by
 179                simp [Nat.add_assoc]
 180        _ = (n - (i.val + 2)) + (i.val + 2) := by
 181                simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
 182        _ = n := Nat.sub_add_cancel hle2
 183        _ = (n - (i.val + 1)) + (i.val + 1) := (Nat.sub_add_cancel hle1).symm
 184    exact Nat.add_right_cancel h
 185  have hrev_succ : (Fin.rev (i + 1)).val = n - (i.val + 2) := by
 186    simp [Fin.val_rev, hival, Nat.add_assoc]
 187  have hnpos : 0 < n := Nat.pos_of_ne_zero (NeZero.ne n)
 188  have hpos1 : 0 < i.val + 1 := Nat.succ_pos _
 189  have hlt : n - (i.val + 1) < n := Nat.sub_lt hnpos hpos1