Transparency (defeq) abuse

Stream: mathlib4

[Matthew Ballard]

Here are the top offenders as measured by having more than 10 erw's (including in comments because I am lazy):

./Geometry/Manifold/VectorBundle/FiberwiseLinear.lean: 60 occurrences of erw found.
./Geometry/RingedSpace/PresheafedSpace/Gluing.lean: 44 occurrences of erw found.
./Algebra/BigOperators/Basic.lean: 41 occurrences of erw found.
./Geometry/RingedSpace/OpenImmersion.lean: 35 occurrences of erw found.
./RepresentationTheory/GroupCohomology/Resolution.lean: 30 occurrences of erw found.
./Algebra/Group/InjSurj.lean: 30 occurrences of erw found.
./AlgebraicGeometry/StructureSheaf.lean: 26 occurrences of erw found.
./CategoryTheory/Equivalence.lean: 23 occurrences of erw found.
./CategoryTheory/Limits/Shapes/Pullbacks.lean: 22 occurrences of erw found.
./AlgebraicGeometry/GammaSpecAdjunction.lean: 20 occurrences of erw found.
./Topology/Sheaves/Stalks.lean: 19 occurrences of erw found.
./AlgebraicGeometry/Pullbacks.lean: 18 occurrences of erw found.
./Algebra/Category/ModuleCat/ChangeOfRings.lean: 18 occurrences of erw found.
./Topology/Gluing.lean: 17 occurrences of erw found.
./CategoryTheory/Monoidal/Internal/Module.lean: 17 occurrences of erw found.
./Algebra/Category/ModuleCat/Monoidal/Basic.lean: 17 occurrences of erw found.
./AlgebraicGeometry/OpenImmersion.lean: 16 occurrences of erw found.
./Algebra/Order/BigOperators/Group/Finset.lean: 16 occurrences of erw found.
./CategoryTheory/Sites/ConcreteSheafification.lean: 15 occurrences of erw found.
./CategoryTheory/Monoidal/Bimod.lean: 15 occurrences of erw found.
./Geometry/Manifold/VectorBundle/Basic.lean: 15 occurrences of erw found.
./Algebra/MonoidAlgebra/Basic.lean: 15 occurrences of erw found.
./CategoryTheory/Limits/Presheaf.lean: 14 occurrences of erw found.
./GroupTheory/HNNExtension.lean: 14 occurrences of erw found.
./Algebra/BigOperators/Finprod.lean: 14 occurrences of erw found.
./RepresentationTheory/Rep.lean: 13 occurrences of erw found.
./AlgebraicTopology/ExtraDegeneracy.lean: 13 occurrences of erw found.
./Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean: 13 occurrences of erw found.
./CategoryTheory/Limits/KanExtension.lean: 12 occurrences of erw found.
./CategoryTheory/Adjunction/Opposites.lean: 12 occurrences of erw found.
./Algebra/Module/LocalizedModule.lean: 12 occurrences of erw found.
./Algebra/Homology/ModuleCat.lean: 12 occurrences of erw found.
./Topology/Category/Profinite/Basic.lean: 11 occurrences of erw found.
./AlgebraicGeometry/Restrict.lean: 11 occurrences of erw found.
./AlgebraicGeometry/Gluing.lean: 11 occurrences of erw found.
./AlgebraicGeometry/Spec.lean: 11 occurrences of erw found.
./AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean: 11 occurrences of erw found.
./CategoryTheory/Limits/HasLimits.lean: 11 occurrences of erw found.
./Algebra/Category/AlgebraCat/Basic.lean: 11 occurrences of erw found.
./Topology/Category/TopCat/Limits/Pullbacks.lean: 10 occurrences of erw found.
./Topology/Sheaves/Skyscraper.lean: 10 occurrences of erw found.
./Analysis/Normed/Group/SemiNormedGroupCat/Kernels.lean: 10 occurrences of erw found.
./FieldTheory/Adjoin.lean: 10 occurrences of erw found.
./AlgebraicGeometry/EllipticCurve/Affine.lean: 10 occurrences of erw found.
./RepresentationTheory/GroupCohomology/Basic.lean: 10 occurrences of erw found.
./Data/Num/Lemmas.lean: 10 occurrences of erw found.