Naming convention for iff and one direction of iff

Stream: mathlib4

[Li Xuanji]

Suppose I want to export the following two lemmas:

import Mathlib

structure Sequence where
  seq : (ℕ → ℚ)

def equiv (a b: Sequence) : Prop := sorry

def isCauchy (a: Sequence) : Prop := sorry

lemma cauchy_of_equiv {a b: Sequence}
  (hab: equiv a b)
  (ha : isCauchy a)
: isCauchy b := by sorry

lemma cauchy_iff_cauchy_of_equiv {a b: Sequence}
  (hab: equiv a b)
: (isCauchy a ↔ isCauchy b) := by sorry

These names are my best attempt to follow the Mathlib naming conventions while still having the two names be unambiguous. However, I would like the second lemma to have a shorter / more memorable name, because I forsee reaching for it more often. Is there a way to do so?

[Aaron Liu]

This does not quite follow mathlib naming convention

[Aaron Liu]

unfortunately Equiv is already taken

[Aaron Liu]

Is this better?

import Mathlib

structure Sequence where
  seq : ℕ → ℚ

namespace Sequence

def Equiv (a b : Sequence) : Prop := sorry

def IsCauchy (a : Sequence) : Prop := sorry

lemma isCauchy_of_equiv_of_isCauchy {a b : Sequence}
    (hab : Equiv a b)
    (ha : IsCauchy a) :
    IsCauchy b := by
  sorry

lemma Equiv.isCauchy_congr {a b : Sequence}
    (hab : Equiv a b) :
    IsCauchy a ↔ IsCauchy b := by
  sorry

[Li Xuanji]

Ooh I failed to spot that congr was in the stdlib naming conventions file, not the Mathlib one. It seems to be what I need