Misc (#3793)

* add $j tags, *ALT -> *g

* update changes-set.txt

* update comments

* update comments of *g theorems

changes-set.txt

@@ -14,6 +14,44 @@ The ones WITH "Notes" may have to be processed manually.
 
 PROPOSED:
 Date      Old       New         Notes
+proposed  nfiundg   nfiund
+proposed  bnj1441g  bnj1441
+proposed  cbviinvg  cbviinv
+proposed  cbviunvg  cbviunv
+proposed  cbviing   cbviin
+proposed  cbviung   cbviun
+proposed  nfiing    nfiin
+proposed  nfiung    nfiun
+proposed  nfrexg    nfrex
+proposed  nfrexdg   nfrexd
+proposed  nfaba1g   nfaba1
+proposed  nfabg     nfab
+proposed  hblemg    hblem
+proposed  nfsabg    nfsab
+proposed  hbabg     hbab
+proposed  cbvmptvg  cbvmptv
+proposed  cbvmptg   cbvmpt
+proposed  cbvmptfg  cbvmptf
+proposed  cbvopab1g cbvopab1
+proposed  nfiund    nfiundv
+proposed  bnj1441   bnj1441v
+proposed  cbviinv   cbviinvv
+proposed  cbviunv   cbviunvv
+proposed  cbviin    cbviinv
+proposed  cbviun    cbviunv
+proposed  nfiin     nfiinv
+proposed  nfiun     nfiunv
+proposed  nfrex     nfrexv
+proposed  nfrexd    nfrexdv
+proposed  nfaba1    nfaba1v
+proposed  nfab      nfabv
+proposed  hblem     hblemv
+proposed  nfsab     nfsabv
+proposed  hbab      hbabv
+proposed  cbvmptv   cbvmptvv
+proposed  cbvmpt    cbvmptv
+proposed  cbvmptf   cbvmptfv
+proposed  cbvopab1  cbvopab1v
 proposed  syl       imtri       (analogous to *bitr*, sstri, etc.)
                                 there is less agreement on renaming syl
                                 than others here
@@ -94,7 +132,11 @@ Date      Old       New         Notes
 20-Jan-24 nfab      nfabg
 20-Jan-24 hblem     hblemg
 20-Jan-24 nfsab     nfsabg
-20-Jan-24 hbab      hbabg 
+20-Jan-24 hbab      hbabg
+17-Jan-24 cbvmptv   cbvmptvg
+17-Jan-24 cbvmpt    cbvmptg
+17-Jan-24 cbvmptf   cbvmptfg
+17-Jan-24 cbvopab1  cbvopab1g
 17-Jan-24 mteqand   [same]      moved from SN's mathbox to main set.mm
 15-Jan-24 sseqtr4d  sseqtrrd
 14-Jan-24 sseqtr4i  sseqtrri

discouraged

@@ -2998,9 +2998,6 @@
 "cbncms" is used by "ubthlem2".
 "cbvexsv" is used by "onfrALTlem1".
 "cbvexsv" is used by "onfrALTlem1VD".
-"cbvmptALT" is used by "cbvmptvALT".
-"cbvmptfALT" is used by "cbvmptALT".
-"cbvopab1ALT" is used by "cbvmptfALT".
 "cdj3lem1" is used by "cdj3i".
 "cdj3lem1" is used by "cdj3lem2b".
 "cdj3lem2" is used by "cdj3i".
@@ -14063,10 +14060,6 @@ New usage of "cbvalvOLD" is discouraged (0 uses).
 New usage of "cbveuALT" is discouraged (0 uses).
 New usage of "cbvexsv" is discouraged (2 uses).
 New usage of "cbvexvOLD" is discouraged (0 uses).
-New usage of "cbvmptALT" is discouraged (1 uses).
-New usage of "cbvmptfALT" is discouraged (1 uses).
-New usage of "cbvmptvALT" is discouraged (0 uses).
-New usage of "cbvopab1ALT" is discouraged (1 uses).
 New usage of "cbvrabvOLD" is discouraged (0 uses).
 New usage of "cbvrexdva2OLD" is discouraged (0 uses).
 New usage of "ccat2s1fvwALT" is discouraged (0 uses).
@@ -18219,10 +18212,6 @@ Proof modification of "cbvalvOLD" is discouraged (53 steps).
 Proof modification of "cbveuALT" is discouraged (48 steps).
 Proof modification of "cbvexsv" is discouraged (29 steps).
 Proof modification of "cbvexvOLD" is discouraged (38 steps).
-Proof modification of "cbvmptALT" is discouraged (15 steps).
-Proof modification of "cbvmptfALT" is discouraged (166 steps).
-Proof modification of "cbvmptvALT" is discouraged (13 steps).
-Proof modification of "cbvopab1ALT" is discouraged (187 steps).
 Proof modification of "cbvrabvOLD" is discouraged (19 steps).
 Proof modification of "cbvrexdva2OLD" is discouraged (128 steps).
 Proof modification of "ccat2s1fvwALT" is discouraged (149 steps).