mathlib

e21b4bcb - chore(data/equiv/transfer_instance): reuse existing proofs (#6868)

chore(data/equiv/transfer_instance): reuse existing proofs (#6868) This makes all the proofs in this file identical. It's unfortunate that the `letI`s have to be written out in each case,