https://github.com/fpvandoorn/carleson/blob/1d0d61deb511bf80f43f0c8f71da274b0c8659f8/Carleson/HolderVanDerCorput.lean#L97
https://github.com/fpvandoorn/carleson/blob/1d0d61deb511bf80f43f0c8f71da274b0c8659f8/Carleson/HolderVanDerCorput.lean#L105
https://github.com/fpvandoorn/carleson/blob/1d0d61deb511bf80f43f0c8f71da274b0c8659f8/Carleson/HolderVanDerCorput.lean#L112
https://github.com/fpvandoorn/carleson/blob/1d0d61deb511bf80f43f0c8f71da274b0c8659f8/Carleson/HolderVanDerCorput.lean#L171
https://github.com/fpvandoorn/carleson/blob/451f4568375c1be265a0beb82adb601f9a3ee74d/Carleson/HardyLittlewood.lean#L384
https://github.com/hargoniX/fil-rb/blob/495b941eb72c0200039f8750f41d067de617e3a3/Filrb/Internal/Model.lean#L189
https://github.com/hargoniX/fil-rb/blob/495b941eb72c0200039f8750f41d067de617e3a3/Filrb/Internal/Model.lean#L195
https://github.com/hargoniX/fil-rb/blob/495b941eb72c0200039f8750f41d067de617e3a3/Filrb/Internal/Model.lean#L198
https://github.com/hargoniX/fil-rb/blob/495b941eb72c0200039f8750f41d067de617e3a3/Filrb/Internal/Model.lean#L236
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L18
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L20
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L22
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L90
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L96
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/Homotopy.lean#L20
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/Homotopy.lean#L69
https://github.com/joelriou/topcat-model-category/blob/05b734528674155c6c54f2c49d2867762f5f4765/TopCatModelCategory/SSet/Subcomplex.lean#L499
https://github.com/leanprover-community/mathlib4/blob/cd410875f97a5e8ffd93b683739483202ad99651/Mathlib/Geometry/Manifold/HasNiceBoundary.lean#L154
https://github.com/leanprover-community/mathlib4/blob/7c2926281641c28dc9181cac4f3738d4bb2a4e0f/Mathlib/Algebra/Azumaya/Basic.lean#L321
https://github.com/leanprover-community/mathlib4/blob/7c2926281641c28dc9181cac4f3738d4bb2a4e0f/Mathlib/Algebra/Azumaya/Basic.lean#L327
https://github.com/leanprover-community/mathlib4/blob/237526a5ca997d8087fc2e48476189b9ba2b59c2/Mathlib/LinearAlgebra/ExteriorPower/HodgeStar.lean#L71
https://github.com/leanprover-community/mathlib4/blob/237526a5ca997d8087fc2e48476189b9ba2b59c2/Mathlib/LinearAlgebra/ExteriorPower/WedgeProduct.lean#L38
https://github.com/leanprover-community/mathlib4/blob/237526a5ca997d8087fc2e48476189b9ba2b59c2/Mathlib/LinearAlgebra/ExteriorPower/WedgeProduct.lean#L44
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L315
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L316
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L340
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L343
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L345
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L346
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L347
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L368
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L399
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L400
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L424
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L427
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L429
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L430
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLessThanOne.lean#L431
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean#L252
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean#L270
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/Sandbox.lean#L233
https://github.com/leanprover-community/mathlib4/blob/c853daa166b9dd80ed9735c71db69a20561a613f/Mathlib/Sandbox.lean#L257
https://github.com/m4lvin/lean4-pdl/blob/fb9f64ec5fc547d303efb4a9316eefe0118f7831/Pdl/Distance.lean#L566
https://github.com/siddhartha-gadgil/LeanAide/blob/cd35740f0fd5b4e20f7f99ba8db190e88d5a6a2a/CodeGen/from_statement_12669426150657371507.lean#L116
https://github.com/siddhartha-gadgil/LeanAide/blob/cd35740f0fd5b4e20f7f99ba8db190e88d5a6a2a/CodeGen/from_statement_12669426150657371507.lean#L161
https://github.com/siddhartha-gadgil/LeanAide/blob/c5b492594bec960b38c8aaab513dd9d6fe9ce50e/CodeGen/from_statement_13190426273245751.lean#L111
https://github.com/urkud/DeRhamCohomology/blob/36294892d98704ed045ed43c086b39ee8cd43247/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean#L77
https://github.com/urkud/DeRhamCohomology/blob/36294892d98704ed045ed43c086b39ee8cd43247/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean#L86
https://github.com/urkud/DeRhamCohomology/blob/36294892d98704ed045ed43c086b39ee8cd43247/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean#L90
https://github.com/urkud/DeRhamCohomology/blob/36294892d98704ed045ed43c086b39ee8cd43247/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean#L98
https://github.com/urkud/DeRhamCohomology/blob/36294892d98704ed045ed43c086b39ee8cd43247/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean#L101