rev_add_one_eq

proof body

Tactic-mode proof.

 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
 190  have hrev_add_lt : (Fin.rev (i + 1)).val + 1 < n := by
 191    calc
 192      (Fin.rev (i + 1)).val + 1
 193          = n - (i.val + 1) := by
 194              calc
 195                (Fin.rev (i + 1)).val + 1 = (n - (i.val + 2)) + 1 := by
 196                  simpa [hrev_succ]
 197                _ = n - (i.val + 1) := hnat
 198      _ < n := hlt
 199  have hL : (Fin.rev (i + 1) + 1).val = (Fin.rev (i + 1)).val + 1 :=
 200    Fin.val_add_one_of_lt' (n := n) (i := Fin.rev (i + 1)) hrev_add_lt
 201  have hR : (Fin.rev i).val = n - (i.val + 1) := by
 202    simp [Fin.val_rev]
 203  calc
 204    (Fin.rev (i + 1) + 1).val = (Fin.rev (i + 1)).val + 1 := hL
 205    _ = (n - (i.val + 2)) + 1 := by simpa [hrev_succ]
 206    _ = n - (i.val + 1) := hnat
 207    _ = (Fin.rev i).val := by simpa [hR]
 208