Lagrange theorem in finset form

Stream: general

[Bolton Bailey]

I've been trying to prove a version of Lagrange's theorem so I don't have to deal with all this type theory as I work on theorems. What is the right way to make progress here?

import group_theory.subgroup.basic

instance subgroup_fintype {G : Type} [fintype G] [group G] {H : subgroup G} : fintype H :=
begin
  -- library_search
  sorry,
end

-- Version of Lagrange's theorem using the formalism of a closed subset
lemma card_closed_subset_dvd_card {α : Type} [fintype α] [group α] (s : finset α)
  (closed_under_mul : ∀ a b ∈ s, a * b ∈ s) (closed_under_inv : ∀ a ∈ s, a⁻¹ ∈ s)
  (id_mem : (1 : α) ∈ s)  :
  finset.card s ∣ fintype.card α :=
begin
  have s_subgroup : subgroup α := subgroup.mk (s : set α) _ _ _,
  have : s.card = fintype.card s_subgroup,
  { tidy,
    rw fintype.card_subtype, --why does this fail
    rw ← subgroup.mem_carrier, --why does this fail
   },
  rw this,
  convert subgroup.card_subgroup_dvd_card s_subgroup,
  sorry { tidy, },
  sorry { tidy, },
  sorry { tidy, },
end

[Kevin Buzzard]

That doesn't compile for me -- I get a failed to synthesize ⊢ fintype ↥s_subgroup.

[Bolton Bailey]

I'm getting that in the web editor too, but it works fine for me in vscode

[Bolton Bailey]

Maybe I need more imports

[Kevin Buzzard]

that's probably because you have an outdated version of mathlib on your computer. But it makes it difficult for me to debug

[Bolton Bailey]

The issue was that I was missing an instance I had defined, sorry, it should be fixed now

[Kevin Buzzard]

My guess is that the rewrite is failing because of some constructivist nonsense. Lean is finding a different proof of finiteness and you're not using convert so rotten luck. I wrote nat.card for a reason you know ;-) I might be wrong though.

[Kevin Buzzard]

In fact I would thoroughly recommend nat.card for use with finite groups. It is nonconstructive and returns the value 0 for infinite types, which is great in group theory because finite groups can't have size 0.

[Kevin Buzzard]

Yeah, this works:

  have : s.card = fintype.card s_subgroup,
  { tidy,
    classical,
    convert (fintype.card_subtype (λ t, t ∈ s_subgroup)).symm,

so the issue is that fintype stinks. convert works its way around the constructive mess because it knows that fintype is a subsingleton.

[Kevin Buzzard]

rw ← subgroup.mem_carrier fails because rw won't work under a binder; simp_rw ← subgroup.mem_carrier, works.

[Kevin Buzzard]

Oh! Another reason you'll have real problems is have s_subgroup : subgroup α := ...: this have needs to be a let because you're defining data here.

[Kevin Buzzard]

In fact changing that might fix up a whole bunch of stuff.

[Kevin Buzzard]

I would strongly recommend against all this tidy stuff by the way. Use tidy? to find out what it's doing and do that instead; it's much quicker :-)

[Bolton Bailey]

The documentation for let and have seems to be exactly the same, can you explain to me in what way they behave differently?

[Kevin Buzzard]

have a : \N := 37 promptly forgets that a = 37, and you're just left with a : nat that you know nothing about.

[Damiano Testa]

Btw, you also should not need closed_under_inv and inv_mem, right?

[Eric Wieser]

Note that have in tactic mode doesn't actually make lean forget, it just pretends it's forgotten until you conclude the tactic block