Fintype.card and subgroups

Stream: mathlib4

[Patrick Massot]

I'd like to add to mathlib

variable {M : Type*} [MulOneClass M]  (S : Submonoid M)

@[to_additive]
theorem eq_bot_of_subsingleton [Subsingleton S] : S = ⊥ := by
  rw [eq_bot_iff_forall]
  intro y hy
  change ((⟨y, hy⟩ : S) : M) = (1 : S)
  rw [Subsingleton.elim (⟨y, hy⟩ : S) 1]

open Fintype in
lemma eq_bot_iff_card [Fintype S] : S = ⊥ ↔ card S = 1 := by
  suffices (∀ x ∈ S, x = 1) ↔ ∃ x ∈ S, ∀ a ∈ S, a = x by
    simpa [eq_bot_iff_forall, card_eq_one_iff]
  constructor
  · intro h
    use 1, S.one_mem
  · rintro ⟨y, -, hy'⟩ x hx
    calc x = y := hy' x hx
    _      = 1 := (hy' 1 S.one_mem).symm

But mathlib complains Finset should not be defined too early. What is the natural home for those lemmas?

[Damiano Testa]

#find_home! eq_bot_iff_card suggests:

[Mathlib.Data.Finsupp.Defs,
 Mathlib.Algebra.Category.MonCat.Limits,
 Mathlib.Topology.Algebra.Order.Archimedean,
 Mathlib.GroupTheory.GroupAction.Basic,
 Mathlib.GroupTheory.Submonoid.Membership]

[Patrick Massot]

Does it take into accounts the interdictions?

[Damiano Testa]

I do not think so, nor does it really take into account tactics... but maybe it is a start?

[Patrick Massot]

This is a stupid question actually.

[Patrick Massot]

If it suggests these are possible homes then it means those files import Fintype without upsetting Lean.

[Damiano Testa]

Well, probably the tactic could do that, but right now it is not too refined: it is a spin-off of the tactic that generates import graphs, so it has those functionalities in mind.

[Damiano Testa]

What the command should do is give a list of all the files where the given declaration could be placed without having to add any import, listing only the minimal such files.

It actually does not return exactly this, but a good approximation.

[Damiano Testa]

In reality, it checks that all the constants that are appear in the proof term of the given declaration are available in the files of the given list (listing the import-minimal ones). However, if you use notation or tactics that are unavailable in those files, the command will not know this.

[Thomas Browning]

Don't we already have docs#Subgroup.card_eq_one ?

[Damiano Testa]

Also, the other lemma produces this:

#find_home! eq_bot_of_subsingleton
[Mathlib.GroupTheory.Submonoid.Operations]

[Damiano Testa]

Oh, I thought that this was in namespace Submonoid...

[Thomas Browning]

Oh, sorry, these are submonoid lemmas

[Damiano Testa]

If only Patrick knew about #mwe...

[Patrick Massot]

Actually I was originally interested in the subgroup version and I failed to find this. The reason is of course cardinal hell: your lemma is about Nat.card and I was looking at Fintype.card.

[Thomas Browning]

I've found that Nat.card works quite well for subgroups, since the junk value of 0 is perfect for divisibility

[Thomas Browning]

(For instance, docs#Subgroup.card_mul_index)

[Patrick Massot]

I opened #7614.