Porting Notes

[pitmonticone]

"Type"	Issue	PR	No. Results	No. Files
simp / @[simp] can prove this	leanprover-community#10618	leanprover-community#10619	596	211
dsimp can prove this	leanprover-community#10685	leanprover-community#10686	7	7
simp cannot prove this	leanprover-community#10959	leanprover-community#10960	19	9
dsimp cannot prove this	leanprover-community#10675	leanprover-community#10676	28	13
need dsimp only	leanprover-community#10971	leanprover-community#10972	15	2
was rw	leanprover-community#10691	leanprover-community#10692	13	8
was simp	leanprover-community#10745	leanprover-community#10746	46	32
was dsimp	leanprover-community#10934	leanprover-community#10935	8	2
was tidy	leanprover-community#10936	leanprover-community#10937	10	5
was decide!	leanprover-community#11043	leanprover-community#11044	17	6
was infer_instance	leanprover-community#11187	leanprover-community#11188	6	3
added proof	leanprover-community#10888	leanprover-community#10889	8	4
added instance	leanprover-community#10754	leanprover-community#10755	77	37
added theorem / lemma	leanprover-community#10756	leanprover-community#10757 / leanprover-community#11432	233	115
added definition	leanprover-community#11445	leanprover-community#11446	12	9
added dsimp	leanprover-community#11227	leanprover-community#11228	11	4
added dsimp only	leanprover-community#10750	leanprover-community#10751	14	1
added to ease automation	leanprover-community#10688	leanprover-community#10689	23	16
added to speed up elaboration	leanprover-community#10694	leanprover-community#10695	6	2
added to clean up types	leanprover-community#10750	leanprover-community#10751	14	1
removed @[nolint has_nonempty_instance]	leanprover-community#10927	leanprover-community#10929	43	27
removed @[simp]	leanprover-community#11119	leanprover-community#11121	21	7
removed @[pp_nodot]	leanprover-community#11180	leanprover-community#11181	19	4
removed @[ext]	leanprover-community#11182	leanprover-community#11183	5	3
instance was not necessary (category theory)	leanprover-community#10670	leanprover-community#10671	12	6
broken dot notation	leanprover-community#11036	leanprover-community#11038	36	5
broken proof was	leanprover-community#11039	leanprover-community#11040	13	3
broken ext	leanprover-community#11041	leanprover-community#11042	8	2
cannot automatically derive	leanprover-community#11081	leanprover-community#11082	6	2
slow(er)	leanprover-community#11083	leanprover-community#11084	38	19
TODO	leanprover-community#11215	leanprover-community#11216	182	112
change rw to erw	leanprover-community#11224	leanprover-community#11225	9	5
change (coe : ℤ → α) to (Int.cast : ℤ → α)	leanprover-community#11249	leanprover-community#11250	10	1
deprecated	leanprover-community#11229	leanprover-community#11230	4	2
rfl required	leanprover-community#11441	leanprover-community#11442	6	1
apply → induction	leanprover-community#11443	leanprover-community#11444	9	1