## Stream: new members

### Topic: Coercion nightmares

#### Antoine Chambert-Loir (Apr 05 2022 at 12:57):

A subgroup of a subgroup is a subgroup, but this proof looks ridiculous. Am I that much ignorant ?

import tactic

import group_theory.subgroup.basic

variable (α : Type*)

example : ∀ (s : set α) (t : set ↥s), ∃ (u : set α),
∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
begin
intros s t,
let j : ↥s → α := λ x, ↑x,
use j '' t,
intro a,
split,
{ intro ha,
simp only [set.mem_image, set_coe.exists] at ha,
obtain ⟨b, hb, hb', hb''⟩ := ha,
suffices : a = b,
{ rw this, use hb, exact hb' },
rw ← hb'',
refl },
{ rintro ⟨hs', hs''⟩,
simp only [set.mem_image, set_coe.exists],
use a, use hs', apply and.intro hs'',
refl }
end

variable [hα : group α]

example : ∀ (G : @subgroup α hα) (H : subgroup G),
∃ (H' : subgroup α), ∀ (a : α), a ∈ H' ↔
∃ (ha : a ∈ G), (⟨a, ha⟩ : ↥G) ∈ H :=
begin
intros G H,
have j : G →* α := subgroup.subtype G,
use H.map (G.subtype),
intro a,
split,
{ intro ha,
simp only [subgroup.mem_map, exists_prop] at ha,
obtain ⟨b, hb, hb'⟩ := ha,
suffices : a = b,
{ have this': a ∈ G,
{ rw this, exact set_like.coe_mem b, },
use this',
have this' : b = ⟨a, this'⟩,
{ exact subtype.eq (eq.symm this), },
rw this' at hb, exact hb },
rw ← hb',
refine congr _ rfl,
refine subgroup.coe_subtype G },
{ rintro ⟨ha, ha'⟩,
simp only [subgroup.mem_map, subgroup.coe_subtype, exists_prop],
use (⟨a, ha⟩),
apply and.intro ha',
exact subtype.coe_mk a ha },
end


#### Kevin Buzzard (Apr 05 2022 at 13:01):

The trick is to use map and comap to push sets forwards and backwards along the map from \u s to alpha

#### Johan Commelin (Apr 05 2022 at 13:04):

And sometimes it turns out to be better to work with injective group homs.

#### Riccardo Brasca (Apr 05 2022 at 13:04):

The map is docs#subgroup.subtype

#### Antoine Chambert-Loir (Apr 05 2022 at 13:18):

The whole role of this is to be able teach Lean that fixing_subgroup (fixing_subgroup M s) t = fixing_subgroup M (s \cup t), but Lean resists…

#### Kevin Buzzard (Apr 05 2022 at 13:18):

example (s : set α) (t : set ↥s) : ∃ (u : set α),
∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
begin
-- move s, t before the colon to save intro
use (coe : s → α) '' t, -- the map is already there and this is the simp normal form
finish, -- this is now just logic nonsense, unpacking and repacking
end


some tips @Antoine Chambert-Loir

#### Antoine Chambert-Loir (Apr 05 2022 at 13:27):

I learn about finish!

#### Antoine Chambert-Loir (Apr 05 2022 at 13:30):

By the way, do you understand why I needed to specify @subgroup hM M (where hM : group M) in the second proof above ? — subgroup M didn't suffice to find an instance of group M.

This is weird

#### Riccardo Brasca (Apr 05 2022 at 13:32):

ah, wait, this is because you named the instance

#### Riccardo Brasca (Apr 05 2022 at 13:33):

variable [group α]

example : ∀ (G : subgroup α) (H : subgroup G),
∃ (H' : subgroup α), ∀ (a : α), a ∈ H' ↔
∃ (ha : a ∈ G), (⟨a, ha⟩ : ↥G) ∈ H :=


should be OK

#### Riccardo Brasca (Apr 05 2022 at 13:34):

If you give a name to a variable between square brackets, then Lean will not include it unless you mention it. So with variable [hα : group α] it doesn't know that α  is a group

#### Antoine Chambert-Loir (Apr 05 2022 at 13:35):

In any case, now I can at least state what I wish to prove :

lemma certainly_easy_to_prove_nightmare_to_state {s t : set α} : fixing_subgroup M (s ∪ t) =
(fixing_subgroup (fixing_subgroup M s) t).map (fixing_subgroup M s).subtype :=
sorry


#### Riccardo Brasca (Apr 05 2022 at 13:35):

If you need to give it a name and use it several time you can write include hα.

#### Riccardo Brasca (Apr 05 2022 at 13:49):

It seems we are missing a reasonable API for fixing_subgroup. For example the first sorry here

variables {M : Type*} [group M] [mul_action M α]

lemma certainly_easy_to_prove_nightmare_to_state {s t : set α} : fixing_subgroup M (s ∪ t) =
(fixing_subgroup (fixing_subgroup M s) t).map (fixing_subgroup M s).subtype :=
begin
ext x,
split,
{ intros hx,
refine ⟨⟨x, _⟩, ⟨_, _⟩⟩,
{ sorry },
{ sorry },
{ sorry } },
{ rintros hx ⟨y, hy₁ | hy₂⟩,
{ sorry },
{ sorry } }
end


should follow from some monotonicity of fixing_subgroup, that I don't find.

#### Kevin Buzzard (Apr 05 2022 at 13:50):

@Antoine Chambert-Loir

import tactic

import group_theory.subgroup.basic

variable (α : Type*)

example (s : set α) (t : set ↥s) : ∃ (u : set α),
∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
begin
use (coe : s → α) '' t,
intro a,
split,
{ -- We begin by abusing definitional equality and use the rfl trick.
rintro ⟨⟨b, hbs⟩, hbt, rfl⟩, -- The rfl trick *defines* a to be b, substitutes in and then just rerases a.
exact ⟨hbs, hbt⟩ }, -- Can now just make the term
{ rintro ⟨has, hat⟩,
-- the proof should now be one line, of the form exact ⟨⟨t₁, t₂⟩, ⟨t₃, t₄, t₅⟩⟩.
-- Let's *experiment* now in tactic mode, and then use the refine tactic to make the
-- term we need.
-- use a, Oh this made progress. I now randomly have two goals but they
-- both look pretty simple. I'll take that.
-- But actually use just ran the refine tactic on something else.
-- Let's see what use a actually did:
refine ⟨⟨a, _⟩, _⟩,  -- The two underscores are the new goals.
{ -- two goals so make a new bracket
-- use has closes this goal! Now let's think about how to write it using refine
exact has, }, -- the first _ was just the term has.
{ -- second goal
-- apply and.intro hat, looks like a good first move. But apply just used refine:
refine and.intro hat _,
refl -- now solves the goal!
-- but if the proof was refl we can just use rfl on the previous line
}
}
-- Therefore, the one line proof is exact ⟨⟨a, has⟩, and.intro hat rfl⟩,
end


#### Antoine Chambert-Loir (Apr 05 2022 at 13:53):

@Riccardo Brasca , Yes, docs#fixing_subgroup is defined « par la bande » in the files devoted to Galois theory. I believe one needs to transfer them somewhere in the files related to docs#mul_action, as well as adding much stuff. For example, I found useful to have

lemma mem_fixing_subgroup_iff (s : set α) (g : M) :
g ∈ fixing_subgroup M s ↔ ∀ (y : α) (hy : y ∈ s), g • y = y := ⟨λ hg y hy, hg ⟨y, hy⟩, λ h ⟨y, hy⟩, h y hy⟩


#### Riccardo Brasca (Apr 05 2022 at 13:54):

I totally agree that lemma should be immediately after the definition, that should be elsewhere

#### Riccardo Brasca (Apr 05 2022 at 13:55):

There is docs#mul_action.stabilizer

#### Riccardo Brasca (Apr 05 2022 at 13:56):

With an API, but it is for a singleton (I didn't check the whole file).

#### Kevin Buzzard (Apr 05 2022 at 13:59):

example (s : set α) (t : set ↥s) : ∃ (u : set α),
∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
⟨(coe : s → α) '' t,λ a, ⟨by {rintro ⟨⟨b, hbs⟩, hbt, rfl⟩,exact ⟨hbs, hbt⟩},
-- no rfl trick here so can do it all in term mode
λ ha, ⟨⟨a, ha.some⟩, ⟨ha.some_spec, rfl⟩⟩⟩⟩


#### Kevin Buzzard (Apr 05 2022 at 14:01):

The rfl trick in rintro involves a "deep eq.rec" so you don't want to translate it into term mode, my guess is that the term generated by the rintro rfl tactic is really nasty.

#### Kevin Buzzard (Apr 05 2022 at 14:01):

Oh by the way I used the axiom of choice with exists.some and exists.some_spec

#### Reid Barton (Apr 05 2022 at 15:02):

quite unnecessarily though: λ ⟨ha₁, ha₂⟩, ⟨⟨a, ha₁⟩, ⟨ha₂, rfl⟩⟩

#### Kevin Buzzard (Apr 05 2022 at 16:48):

I thought that term mode lambda pointies were discouraged!

#### Reid Barton (Apr 05 2022 at 16:48):

Only for defining data

#### Reid Barton (Apr 05 2022 at 16:51):

It will produce a term with a whatever.rec` in a place that usually isn't the best place for it

#### Reid Barton (Apr 05 2022 at 16:51):

but for a proof we don't care

Last updated: Dec 20 2023 at 11:08 UTC