mathlib3

86839bc5 - style (group_theory/iwasawa.lean): shorten proofs and remove unused stuff

style (group_theory/iwasawa.lean): shorten proofs and remove unused stuff Use shortened proofs as suggested by @tb65536 Use set.image_preimage and remove unused basic lemmas Use nontrivial and remove useless intermediate results