# Zulip Chat Archive

## Stream: general

### Topic: deprecated folder -- deleting lemmas?

#### Kevin Buzzard (Jul 22 2021 at 14:26):

I am always a bit annoyed by the `deprecated`

directory, and so I spent some time over the last few weeks changing all the main classes in there (`is_submonoid`

, `is_subgroup`

etc, and `is_group_hom`

, `is_ring_hom`

etc) to structures (my understanding is that we still want these things around but not in the typeclass system). My `undeprecate`

branch just compiled for the first time the other day; I changed 87 files. It's #8178 .

There are still some loose ends here however, and I thought that maybe I should get some community input. What I would imagine the next step would be is to start removing imports of deprecated files. I had it in my head that there were a few places where these structures were really useful, however I am now less sure about this. The main examples where you see the advantage of the unbundled approach is in the rare-but-they-do-exist cases where `R`

is, say, a ring, and (in the middle of a long tactic proof) you define some `S : add_subgroup R`

and then do some stuff with it and then later on manage to show that it's closed under R's multiplication. With the deprecated system you had `S : set R`

with `[is_add_subgroup S]`

and you just add an instance of `[is_add_subring S]`

and keep going. With the new system you need to make a new `S' : subring R`

and all your hypotheses about `S`

now need to be beefed up to apply to `S'`

or else you can't rewrite with them. This turns out to be only a minor annoyance.

But the real reason I'm bringing this up is that once this change is made, there are some definitions and results in mathlib which are much harder to state, or rather can in theory be stated but only in a convoluted way. An example is `subtype.monoid`

, which looks like this in master (clean, but using the fact that `is_submonoid`

is a class) and like this on the branch where `is_submonoid`

becomes a structure. Notice the weird `[fact (is_submonoid s)]`

. Why is this here? Well, if I just wrote `(hs : is_submonoid s)`

then I could get `subtype.monoid`

compiling no problem, but the problems all start later when we're doing things like

```
lemma is_submonoid.coe_mul [fact (is_submonoid s)] (a b : s) :
((a * b : s) : M) = a * b := rfl
```

This is the version on my branch, which works fine. But without using `fact`

Lean has no way of figuring out what the multiplication is, because `M`

is a monoid but `s : set M`

so it's hard to get the _statement_ to typecheck.

As I say, the branch compiles right now, so one can look through the changed files and see the facts I've added. There aren't that many, and I know for sure that these results cannot really be used anywhere because these facts will not be in the typeclass system in general, I didn't make an instance of `fact (is_submonoid s)]`

anywhere. So one way forward would be simply to *delete* lemmas like `is_submonoid.coe_mul`

completely. Basically they have become unusable because of the change, and I see little point in keeping them. I'm aware that deleting lemmas is not something which is usually done so this is why I wanted to ask about it.

Some early work of Kenny on Galois theory used `is_add_subgroup`

and because I knew the material well and was confident that analogous `add_subgroup`

versions weren't there, I took the trouble to refactor them and remove a deprecated import. If there are any other areas of mathlib where people want me to make the refactor from is_X to X then I'm in quite a good position to work on this stuff now because I know the tricks (and by this time next month I'll have forgotten them). However another point of view might be that because I made a PR which touches 87 files it might be best to get it merged ASAP. However I can certainly work on completely deleting those deprecated lemmas today or tomorrow.

#### Johan Commelin (Jul 22 2021 at 14:31):

Wowowow! Thanks a lot for this massive effort!

My first reaction is: we should get rid of those `fact`

-lemmas, and merge the rest ASAP.

#### Kevin Buzzard (Jul 22 2021 at 14:47):

OK I will remove the lemmas which cannot be being used because they have facty typeclasses; I can do it at Xena tonight.

#### Floris van Doorn (Jul 22 2021 at 14:47):

I think we should get rid of all these lemmas about `is_submonoid`

(at least, if there is a `submonoid`

alternative, which should be the case almost always). The only things we really want to keep are the translations between `is_submonoid`

and `submonoid`

: `submonoid.of`

(which maybe should be renamed `is_submonoid.submonoid`

to enable projection notation) and `submonoid.is_submonoid`

.

All declarations `foo`

about `is_submonoid`

that can be proven by `M.submonoid.foo`

should be removed.

#### Kevin Buzzard (Jul 22 2021 at 14:48):

Should this be done in this PR or in another one? Thanks for the input!

#### Kevin Buzzard (Jul 22 2021 at 14:48):

In general PR's which touch a huge number of files are really scary, but actually I'm only changing things which nobody else is working on so it's much less scary than you think.

#### Floris van Doorn (Jul 22 2021 at 14:51):

If you make separate PRs, you're changing the statement of a lot of lemmas in this PR that will be removed in the next PR.

So it will at least be easier to review if you decide to make a single PR. It also depends on how likely merge conflicts are (and your willingness to resolve them).

#### Floris van Doorn (Jul 22 2021 at 14:52):

If you think that a lot of proofs of lemmas that we want to keep use lemmas that we are removing, then it might be easier to make separate PRs.

#### Reid Barton (Jul 22 2021 at 15:02):

`is_submonoid.coe_mul`

is an API lemma about some `has_mul`

instance that you are also deleting, right?

#### Reid Barton (Jul 22 2021 at 15:06):

Oh that's the `subtype.monoid`

you mentioned

#### Reid Barton (Jul 22 2021 at 15:11):

Oh I'm confused now. `subtype.monoid`

used to be a def, but now it is an instance; how come?

#### Floris van Doorn (Jul 22 2021 at 15:38):

We want to remove `subtype.monoid`

and instead use `(hM : is_submonoid M).submonoid.monoid`

(if really needed).

#### Kevin Buzzard (Jul 22 2021 at 16:12):

Reid Barton said:

Oh I'm confused now.

`subtype.monoid`

used to be a def, but now it is an instance; how come?

My impression is that it used to be dangerous in some way to make it an instance; it was occasionally made a local instance IIRC.

#### Reid Barton (Jul 22 2021 at 16:21):

Like for example about 12 lines after its definition, on your branch :upside_down:

#### Kevin Buzzard (Jul 22 2021 at 16:33):

So just to be clear -- we have docs#is_subgroup.normal_in_normalizer stating in a deprecated way that a subgroup is normal in its normalizer, and this is never used in mathlib, and we also have docs#subgroup.normal_in_normalizer, which states this in the non-deprecated way, and the statement uses `subtype.group`

which is going to be removed, and so I am also going to remove `is_subgroup.normal_in_normalizer`

.

#### Kevin Buzzard (Jul 22 2021 at 16:34):

PS I think merge conflicts are highly unlikely unless there's some big refactor of algebra going on that I don't know about.

#### Kevin Buzzard (Jul 22 2021 at 17:14):

OK so that was less painful than expected -- all the facts I added are removed now.

#### Kevin Buzzard (Jul 22 2021 at 18:10):

@Floris van Doorn or anyone else who understands this stuff: right now `ring_theory.subring`

imports `deprecated.subring`

, but it's the other way around for submonoids. I propose switching this, having `deprecated.subring`

import `ring_theory.subring`

, and moving docs#set.to_subring into `deprecated.subring`

and renaming it to `is_subring.subring`

. This way I can work on removing all `import deprecated.subring`

from undeprecated mathlib. I have already achieved this with `deprecated.subfield`

.

#### Johan Commelin (Jul 22 2021 at 18:13):

Wouldn't it be easier to move `deprecated.*`

back into the main tree? Because that's the end goal anyway, right?

#### Floris van Doorn (Jul 22 2021 at 20:36):

I agree with Johan that we eventually want to remove the `deprecated`

folder entirely. My thought is to have 20-30 lines at the end of

https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/submonoid/basic.lean

(or perhaps in a separate file) about `is_submonoid`

, with just the results in

https://github.com/leanprover-community/mathlib/blob/468328daee53ea78e8522daa20893a434ce30b57/src/deprecated/submonoid.lean#L34-L59

and

https://github.com/leanprover-community/mathlib/blob/468328daee53ea78e8522daa20893a434ce30b57/src/deprecated/submonoid.lean#L410-L415

There might be a little bit more that we want to keep, if it doesn't have a good bundled analogue. But something like docs#is_submonoid.inter can be removed since we can take meets of bundled submonoids.

The same can be true about rings.

#### Eric Wieser (Jul 22 2021 at 20:43):

In the long run I'd be tempted to extract the proofs from things like `submonoid.has_inf`

and move them back out to `is_submonoid.inter`

#### Eric Wieser (Jul 22 2021 at 21:01):

But right now we prove the same thing from scratch in both places, so we may as well throw out the one we don't use

#### Kevin Buzzard (Jul 22 2021 at 22:41):

so right now I have removed all `import.deprecated.*`

from all mathlib files other than those in `src/deprecated`

(and `test`

), and a bunch of stuff has broken again, so in some sense I feel like I'm back to square one. I am now creating diffs like the following screenshot:

There are random places all over mathlib where people prove `is_group_hom`

for a map, and I'm replacing them with defs (if they don't seem to be there already) and adding a simp lemma. Am I going the right way? I could just add some deprecated imports back in and I'd have everything compiling again. So far I've added set.singleton_mul_hom to replace docs#set.singleton.is_mul_hom, multiset.map_add_monoid_hom to replace `is_add_monoid_hom (multiset.map f)`

, `countp_add_monoid_hom`

to replace docs#multiset.countp.is_add_monoid_hom and so on. Should I cut my losses and stop or is this what we want?

#### Yakov Pechersky (Jul 22 2021 at 22:43):

Shouldn't simps take care of making the simp lemma for you?

#### Kevin Buzzard (Jul 22 2021 at 22:44):

I don't understand `simps`

. Is this what it does?

#### Kevin Buzzard (Jul 22 2021 at 22:44):

attribute#simps

#### Kevin Buzzard (Jul 22 2021 at 22:45):

I'm not very good at attributes.

#### Yakov Pechersky (Jul 22 2021 at 22:45):

Simps makes the boilerplate lemmas for equivs and I think bundled homs

#### Eric Rodriguez (Jul 22 2021 at 22:45):

I didn't get it before but I just put `@[simps?]`

before any definition and if the lemmas look reasonable I keep it in

#### Kevin Buzzard (Jul 22 2021 at 22:46):

Right now my question is whether I should be going down this rabbithole at all. I've changed 86 files, got mathlib compiling, then I deleted a few imports and now it's all broken again.

#### Eric Rodriguez (Jul 22 2021 at 22:46):

works fine most of the time, you can also make it `simp`

the RHS before making a lemma (I can't remember how though)

#### Yakov Pechersky (Jul 22 2021 at 22:48):

simps {rhs := true} iirc

#### Yakov Pechersky (Jul 22 2021 at 22:49):

(deleted)

#### Patrick Massot (Jul 22 2021 at 22:52):

Kevin, if you manage to convince some maintainer to merge #8317 then you'll have less deprecated group homs to handle.

#### Kevin Buzzard (Jul 22 2021 at 22:58):

Apparently you should be tagging `to_compl`

with `simps`

#### Patrick Massot (Jul 22 2021 at 22:59):

Me? Why?

#### Kevin Buzzard (Jul 23 2021 at 07:51):

Because above I was replacing `is_monoid_hom (foo : X -> Y) := ...`

with `foo_monoid_hom : X ->* Y := ...`

and then `@[simp] lemma foo_monoid_hom_coe : (foo_monoid_hom : X -> Y) = foo := rfl`

and Yakov told me I should be using `@[simps]`

.

#### Kevin Buzzard (Jul 24 2021 at 19:57):

Yakov Pechersky said:

Shouldn't simps take care of making the simp lemma for you?

Wait a minute. I'm now doing this `simps`

thing and I've noticed that it's not making `coe`

lemmas, it's making `apply`

lemmas. For example in the deprecated days we had `multiset.map_is_add_monoid_hom`

(a proof that `map f : multiset α → multiset β`

preserves 0 and addition) and I'm changing it to

```
def multiset.map_add_monoid_hom (f : α → β) : multiset α →+ multiset β := ...
```

If I `@[simps]`

this I get

```
multiset.map_add_monoid_hom_apply: ⇑(map_add_monoid_hom f) s = map f s
```

whereas I was proposing

```
@[simp] lemma map_add_monoid_hom_coe (f : α → β) :
(map_add_monoid_hom f : multiset α → multiset β) = map f := rfl
```

and of course the linter doesn't like both. Which one should be in mathlib? Or isn't it as simple as that?

#### Eric Wieser (Jul 24 2021 at 22:31):

`simps`

hasn't been taught to distinguish coe from apply (yet)

#### Eric Wieser (Jul 24 2021 at 22:32):

IMO we should teach it to though

#### Floris van Doorn (Jul 24 2021 at 23:26):

You can get those lemmas with `@[simps {fully_applied := ff}]`

. See docs#simps_cfg for more info.

There is no way yet to tell simps that for certain projections you should always have `{fully_applied := ff}`

.

#### Kevin Buzzard (Jul 25 2021 at 08:11):

Thanks! I don't know whether they are good simp lemmas in practice but if we're moving away from the `is_`

structures completely then one of them at least seems to be necessary

#### Eric Wieser (Jul 25 2021 at 08:38):

Can you tell it to call the unapplied lemmas `coe_foo`

rather than `foo_apply`

though Floris?

#### Patrick Stevens (Jul 25 2021 at 14:24):

A piece of GitHub usage you might not have known: if you are deciding whether or not to use two PRs, A and then B (which depends on A), one option is to make PR A, then raise PR B with a base of A rather than a base of `master`

. (That is, it is a pull request for merging B into A, not into master.) That way, both PRs can be reviewed independently, with PR B being reviewed as though A had already been merged into master, but really you haven't actually merged A into master. When the whole stack of PRs is ready to merge, you can merge B into A, and then Bors squash-merge A into master. See https://blog.logrocket.com/using-stacked-pull-requests-in-github/ for a longer-form explanation with screenshots. (This workflow may or may not be any use for what you want to do here; I just saw some words upthread which suggested this might be appropriate.)

#### Eric Wieser (Jul 25 2021 at 14:36):

Was that intended for a different thread?

#### Floris van Doorn (Jul 25 2021 at 18:15):

Eric Wieser said:

Can you tell it to call the unapplied lemmas

`coe_foo`

rather than`foo_apply`

though Floris?

Currently the setup is

```
initialize_simps_projections add_hom (to_fun → apply)
```

If you want the `coe`

naming uniformly, you can replace it with

```
initialize_simps_projections add_hom (to_fun → coe as_prefix)
```

Not sure if that is preferred throughout the whole library, though.

#### Eric Wieser (Jul 25 2021 at 20:43):

Sure, but what I'm asking is how to make `@[simps apply]`

output `f_hom_apply : ⇑f_hom x = f x`

and `@[simps coe]`

output `coe_f_hom : ⇑f_hom = f`

#### Eric Wieser (Jul 25 2021 at 20:44):

Or at least, a way to get both via simps, the exact spelling needed doesn't matter, only the lemmas it generates

#### Floris van Doorn (Jul 25 2021 at 22:26):

This is possible, as long as you write the `coe`

projection as `[simps? coe {fully_applied := ff}]`

You have to change the initialization to the following:

```
/-- See Note [custom simps projection] -/
def add_hom.simps.coe (e : α →+ β) : α → β := e
initialize_simps_projections add_hom (to_fun → apply, to_fun → coe, -coe as_prefix)
```

(apparently you have to give the coercion explicitly for the second name of the `to_fun`

projection)

Here is a full example:

```
import tactic.simps
structure equiv (α : Sort*) (β : Sort*) :=
(to_fun : α → β)
local infix ` ≃ `:25 := equiv
variables {α β γ : Sort*}
instance : has_coe_to_fun $ α ≃ β := ⟨_, equiv.to_fun⟩
/-- See Note [custom simps projection] -/
def equiv.simps.coe (e : α ≃ β) : α → β := e
initialize_simps_projections? equiv (to_fun → apply, to_fun → coe, -coe as_prefix)
/-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
protected def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁⟩
attribute [simps? coe {fully_applied := ff}] equiv.trans
/-
[simps] > adding projection equiv.coe_trans:
> ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ),
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-/
attribute [simps?] equiv.trans
/-
[simps] > adding projection equiv.trans_apply:
> ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ) (ᾰ : α),
⇑(e₁.trans e₂) ᾰ = (⇑e₂ ∘ ⇑e₁) ᾰ
-/
```

This is assuming that with `@[simps]`

(without options) you want to generate the `apply`

lemma and not the `coe`

lemma.

#### Eric Wieser (Jul 25 2021 at 22:49):

I guess the only thing that would be left to ask for would be for `coe`

to imply `fully_applied:=ff`

#### Floris van Doorn (Jul 26 2021 at 05:43):

That's a todo in #5489

#### Kyle Miller (Aug 07 2021 at 21:47):

I was just thinking about ways the ways we tend to attach properties to terms.

- Typeclasses let you associate data to a term more or less syntactically: if a term has a particular form, then you can provide some additional structure. A downside is that rewriting an expression tends to break the connection.
- "Bundling" the property by defining a structure along with coercions to the underlying data. This solves the rewrite problem, but the structure isn't
*literally*the data. Attaching multiple different kinds of data can require a carefully designed hierarchy.

One that doesn't seem to be used much is tagging. This is a general tagging function I was just playing with:

```
@[reducible] def attach {α : Sort*} (β : α → Sort*) (x : α) (h : β x) : α := x
```

You can use this to define sets with an attached proof that they are subgroups:

```
abbreviation the_subgroup {α : Type*} [group α] (s : set α) (h : is_subgroup s) :=
attach is_subgroup s h
```

Then, for example,

```
lemma the_subgroup.mem_inter_iff
(s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
(h'' : is_subgroup (s ∩ s')) :
x ∈ the_subgroup (s ∩ s') h'' ↔ x ∈ the_subgroup s h ∧ x ∈ the_subgroup s' h' :=
by rw set.mem_inter_iff
```

Theoretically, the `the_subgroup`

terms in an expression are able to help you apply lemmas that need a proof of `is_subgroup`

, but otherwise the tags will be ignored.

Here are some basic examples (sorry, it's for an older version of mathlib, before @Kevin Buzzard's recent changes...). I haven't really tested the idea, but I thought I'd throw it out there in case it's somehow interesting.

```
import data.int.parity
import deprecated.subgroup
import tactic
@[reducible]
def attach {α : Sort*} (β : α → Sort*) (x : α) (h : β x) : α := x
abbreviation the_even (n : ℤ) (h : even n) := attach even n h
abbreviation the_odd (n : ℤ) (h : odd n) := attach odd n h
lemma the_even_add_one_eq (n : ℤ) (h : even n) :
the_even n h + 1 = the_odd (n + 1) (by simp [int.even_add_one, h]) :=
rfl
abbreviation the_subgroup {α : Type*} [group α] (s : set α) (h : is_subgroup s) :=
attach is_subgroup s h
variables {α : Type*} [group α]
instance (s : set α) (h : is_subgroup s) : is_subgroup (the_subgroup s h) := h
lemma the_subgroup_attach (s : set α) [is_subgroup s] : s = the_subgroup s infer_instance := rfl
lemma the_subgroup.inter (s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') :
the_subgroup s h ∩ the_subgroup s' h' = the_subgroup (s ∩ s') infer_instance :=
rfl
lemma subgroup.of_eq (s : set α) [h : is_subgroup s] : (subgroup.of s : set α) = the_subgroup s h :=
rfl
lemma the_subgroup.mem_inter_iff
(s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
(h'' : is_subgroup (s ∩ s')) :
x ∈ the_subgroup (s ∩ s') h'' ↔ x ∈ the_subgroup s h ∧ x ∈ the_subgroup s' h' :=
by rw set.mem_inter_iff
```

#### Yakov Pechersky (Aug 08 2021 at 01:22):

Aren't these just subtypes of "set X"?

#### Kyle Miller (Aug 08 2021 at 01:59):

@Yakov Pechersky A term with `attach`

ed data is definitionally equal to that term -- there aren't any new types here -- for the subgroup example, `the_subgroup s h`

is trivially defeq to `s`

. It's true that the terms for which you can write a `the_subgroup`

term correspond to terms of a subtype (in particular, `{s : set α // is_subgroup s}`

), but nothing is explicitly constructed. This lets you manipulate tagged terms easier, I think. For example you can sort the attached data:

```
lemma attach_swap
{α : Sort*} (β β' : α → Sort*) (x : α) (h : β x) (h' : β' x) :
attach β (attach β' x h') h = attach β' (attach β x h) h' := rfl
```

In principle, you can also attach data other than proofs, and then they would in a sense "just" be sigma types. One difference from a sigma type is that the additional data is sort of discarded, and it's only used to help fill in implicit arguments during elaboration or when proving things.

#### Yakov Pechersky (Aug 08 2021 at 02:01):

So your attach is like constructing a term of a subtype then instantly coercing it back to the original type

#### Kyle Miller (Aug 08 2021 at 02:13):

Sure, if you want there to be a type involved to explain it. (Are you suggesting it would be better that way? This is just meant add some data to the AST that's easy to access and easy to ignore. Also, if it were using subtypes, it would have to be done in a way that that coercion you describe doesn't get `simp`

ed away.)

#### Yakov Pechersky (Aug 08 2021 at 02:20):

I'm saying that `attach`

is fine for constructing such tagged terms. What about requiring such tagged terms, as an argument for a def or a proof? Then you are proving the data and the proof separately, to be able to say `lemma ex (x : X) (h : P x) : Q (attach x h) := ...`

. I guess I'm not fully understanding what `attach`

gives you that subtypes do not.

#### Yakov Pechersky (Aug 08 2021 at 02:21):

I am not saying that subtypes are the solution to the problem, but rather, I want to appreciate what you propose!

#### Yakov Pechersky (Aug 08 2021 at 02:26):

Ah, here's a difference where your approach is "trivially defeq" but the subtype one isn't:

```
import deprecated.subgroup
import tactic
abbreviation the_subgroup {α : Type*} [group α] (s : set α) (h : is_subgroup s) : set α :=
(⟨s, h⟩ : subtype is_subgroup)
attribute [class] is_subgroup
variables {α : Type*} [group α]
lemma the_subgroup.mem_inter_iff
(s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
(h'' : is_subgroup (s ∩ s')) :
x ∈ the_subgroup (s ∩ s') h'' ↔ x ∈ the_subgroup s h ∧ x ∈ the_subgroup s' h' :=
-- by rw set.mem_inter_iff
begin
rw set.mem_inter_iff, -- fails
sorry
end
@[reducible]
def attach {α : Sort*} (β : α → Sort*) (x : α) (h : β x) : α := x
abbreviation the_subgroup' {α : Type*} [group α] (s : set α) (h : is_subgroup s) : set α :=
attach is_subgroup s h
lemma the_subgroup'.mem_inter_iff
(s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
(h'' : is_subgroup (s ∩ s')) :
x ∈ the_subgroup' (s ∩ s') h'' ↔ x ∈ the_subgroup' s h ∧ x ∈ the_subgroup' s' h' :=
by rw set.mem_inter_iff -- works
```

#### Yakov Pechersky (Aug 08 2021 at 02:27):

The subtype approach requires a `by convert set.mem_inter_iff _ _ _`

#### Kyle Miller (Aug 08 2021 at 02:30):

This is all very untested, but the design constraints I was going for are (1) that rewrites should work with tagged data, and (2) that the tags don't unintentionally disappear (I suspect `simp`

will gobble them up if they were subtypes). Using subtypes is an interesting idea, but I think things tend to work out better following the principle "if a function could take a sigma type, existential, or subtype, make it take the components separately."

#### Yakov Pechersky (Aug 08 2021 at 02:33):

Another way tagged data works is, of course, with structures.

#### Yakov Pechersky (Aug 08 2021 at 02:34):

Which are inherently even more opaque than subtypes.

#### Kyle Miller (Aug 08 2021 at 02:40):

A place tags are sort of used already in mathlib is to create "new" types for having a different collection of instances. There's a variation I haven't seen (though it's possible it's there somewhere, mathlib is big!) where there are additional unused arguments whose purpose is to parameterize instances. One example might be where you want to take a docs#add_torsor, choose an origin, and treat it like an additive group.

#### Kyle Miller (Aug 08 2021 at 02:48):

This could potentially also be a way to have a set remember that it comes from a `set_like`

, which might be an alternative to things like `is_subgroup`

.

```
def sets (α : Type*) {β : Type*} [set_like α β] : set (set β) :=
{s : set β | ∃ (x : α), s = (x : set β)}
abbreviation the (α : Type*) {β : Type*} [set_like α β] (s : set β)
(h : s ∈ sets α) := attach _ s h
lemma some_set {α : Type*} {β : Type*} [set_like α β] {s : set β} (h : s ∈ sets α) :
(h.some : set β) = s := h.some_spec.symm
lemma the_subgroup.inter {α : Type*} [group α] (s t : set α)
(h : s ∈ sets (subgroup α)) (h' : t ∈ sets (subgroup α)) :
the (subgroup α) s h ∩ the (subgroup α) t h' =
the (subgroup α) (s ∩ t) (by { use h.some ⊓ h'.some, simp [some_set]}) := rfl
```

#### Kyle Miller (Aug 08 2021 at 02:50):

(There's probably some way to not have to write lemmas like `the_subgroup.inter`

. I just chose it for demonstration.)

Last updated: Dec 20 2023 at 11:08 UTC