# Zulip Chat Archive

## 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`

.

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

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