From 955455ab353ae1e2b06fe57454506ca6148b4c75 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Sun, 14 Jun 2020 14:28:16 +1000
Subject: [PATCH 1/2] naming advice around `inj` and `ext`.

---
 templates/contribute/naming.md | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md
index 6d1b3eceba..9052fd067f 100644
--- a/templates/contribute/naming.md
+++ b/templates/contribute/naming.md
@@ -259,6 +259,40 @@ check le_of_mul_le_mul_left
 check le_of_mul_le_mul_right
 ```
 
+## Naming of structural lemmas ##
+
+We are trying to standardize certain naming patterns for structural lemmas.
+At present these are not uniform across mathlib.
+
+### Extensionality ###
+
+A lemma of the form `(∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂` should be named `.ext`,
+and labelled with the `@[ext]` attribute.
+Often this type of lemma can be generated automatically by putting the
+`@[ext]` attribute on a structure.
+
+A lemma of the form `s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂` should be named `.ext_iff`.
+
+### Injectivity ###
+
+Injectivity lemmas should usually be written as bidirectional implications,
+e.g. as `f x = f y ↔ x = y`. Such lemmas should be named `f_inj`
+(although if they are in an appropriate namespace `.inj` is good too).
+Bidirectional injectivity lemmas are often good candidates for `@[simp]`.
+There are still many unidirectional implications named `inj` in mathlib,
+and it is reasonable to update and replace these as you come across them.
+
+Note however that constructors for inductive types have
+automatically generated unidirectional implications, named `.inj`,
+and there is no intention to change this.
+When such an automatically generated lemma already exists,
+and a bidirectional lemma is needed, it may be named `.inj_iff`.
+
+Injectivity lemmas written in terms of an `injective f` conclusion
+should instead use the full word `injective`, typically as `f_injective`.
+The form `injective_f` still appears often in mathlib.
+
+
 ------
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

From 61112b7a3f94fd1dc9b74ec64d6fa95b8bd11064 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Sun, 14 Jun 2020 21:53:07 +1000
Subject: [PATCH 2/2] Apply suggestions from code review

---
 templates/contribute/naming.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/templates/contribute/naming.md b/templates/contribute/naming.md
index 9052fd067f..b2e2f0684e 100644
--- a/templates/contribute/naming.md
+++ b/templates/contribute/naming.md
@@ -266,12 +266,16 @@ At present these are not uniform across mathlib.
 
 ### Extensionality ###
 
-A lemma of the form `(∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂` should be named `.ext`,
+A lemma of the form `(∀ x, f x = g x) → f = g` should be named `.ext`,
 and labelled with the `@[ext]` attribute.
 Often this type of lemma can be generated automatically by putting the
 `@[ext]` attribute on a structure.
+(However an automatically generated lemma will always be written in terms
+of the structure projections, and often there is a better statement,
+e.g. using coercions, that should be written by hand then marked with `@[ext]`.)
 
-A lemma of the form `s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂` should be named `.ext_iff`.
+
+A lemma of the form `f = g ↔ ∀ x, f x = g x` should be named `.ext_iff`.
 
 ### Injectivity ###