# Zulip Chat Archive

## Stream: new members

### Topic: How to use h'

#### tsuki hao (Jul 18 2023 at 13:02):

```
import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
def IsA (S : Type u) {α : Type v} [SetLike S α] (s : Set α) : Prop :=
∃ (m : S), (m : Set α) = s
variable (G : Type _ ) [Group G]
example (H₁ H₂ : Subgroup G) (h : IsA (Subgroup G) (H₁ ∪ H₂)) : H₁ ≤ H₂ ∨ H₂ ≤ H₁ := by
by_contra h'
sorry
```

Can somone tell me how the h' should be used here?

#### Kevin Buzzard (Jul 18 2023 at 13:27):

Your question is vague. You can use `h'`

in lots of ways. What do you want to turn `h'`

into? Can you write your question in Lean rather than in text?

Here is a possible continuation:

```
simp only [SetLike.le_def] at h'
push_neg at h'
rcases h' with ⟨⟨x, hx1, hx2⟩, ⟨y, hy2, hy1⟩⟩
```

#### Kyle Miller (Jul 18 2023 at 13:42):

Maybe you'd start like this instead of `by_contra`

?

```
example (H₁ H₂ : Subgroup G) (h : IsA (Subgroup G) (H₁ ∪ H₂)) : H₁ ≤ H₂ ∨ H₂ ≤ H₁ := by
obtain ⟨H, h'⟩ := h
replace h' := Set.ext_iff.mp h'
simp only [SetLike.mem_coe, Set.mem_union] at h'
/-
H₁ H₂ H : Subgroup G
h' : ∀ (x : G), x ∈ H ↔ x ∈ H₁ ∨ x ∈ H₂
⊢ H₁ ≤ H₂ ∨ H₂ ≤ H₁
-/
sorry
```

#### tsuki hao (Jul 18 2023 at 14:16):

Kevin Buzzard said:

Your question is vague. You can use

`h'`

in lots of ways. What do you want to turn`h'`

into? Can you write your question in Lean rather than in text?Here is a possible continuation:

`simp only [SetLike.le_def] at h' push_neg at h' rcases h' with ⟨⟨x, hx1, hx2⟩, ⟨y, hy2, hy1⟩⟩`

Thanks for your answer, that's exactly what I was looking for

#### tsuki hao (Jul 18 2023 at 14:16):

Kyle Miller said:

Maybe you'd start like this instead of

`by_contra`

?`example (H₁ H₂ : Subgroup G) (h : IsA (Subgroup G) (H₁ ∪ H₂)) : H₁ ≤ H₂ ∨ H₂ ≤ H₁ := by obtain ⟨H, h'⟩ := h replace h' := Set.ext_iff.mp h' simp only [SetLike.mem_coe, Set.mem_union] at h' /- H₁ H₂ H : Subgroup G h' : ∀ (x : G), x ∈ H ↔ x ∈ H₁ ∨ x ∈ H₂ ⊢ H₁ ≤ H₂ ∨ H₂ ≤ H₁ -/ sorry`

Thank you, maybe it's ok to write like this, I'll try it later

#### Martin Dvořák (Jul 18 2023 at 14:28):

I was trying to do it as an exercise and got stuck here:

```
import Mathlib.Tactic
import Mathlib.GroupTheory.Subgroup.Basic
def IsA (S : Type) {α : Type} [SetLike S α] (s : Set α) : Prop :=
∃ (m : S), (m : Set α) = s
example {G : Type} [Group G] (H₁ H₂ : Subgroup G) (hyp : IsA (Subgroup G) (H₁ ∪ H₂)) :
H₁ ≤ H₂ ∨ H₂ ≤ H₁ :=
by
by_contra contr
push_neg at contr
obtain ⟨a, a_in, a_ni⟩ : ∃ a ∈ H₁, a ∉ H₂
· exact Iff.mp Set.not_subset contr.1
obtain ⟨b, b_in, b_ni⟩ : ∃ b ∈ H₂, b ∉ H₁
· exact Iff.mp Set.not_subset contr.2
clear contr
have a_in_union : a ∈ (H₁ ∪ H₂ : Set G)
· exact Set.mem_union_left (↑H₂) a_in
have b_in_union : b ∈ (H₁ ∪ H₂ : Set G)
· exact Set.mem_union_right (↑H₁) b_in
have ab_in_union : a * b ∈ (H₁ ∪ H₂ : Set G)
· sorry
sorry
```

I think I need to access something like `hyp.mul_mem'`

but differently. How can I do it?

Also, is there a better way to write `a ∈ (H₁ : Set G) ∪ (H₂ : Set G)`

and so on?

#### Kyle Miller (Jul 18 2023 at 14:29):

I'd expect `a ∈ (H₁ ∪ H₂ : Set G)`

to work

#### Martin Dvořák (Jul 18 2023 at 14:29):

Thanks. I updated the post above.

I still don't know how to prove `a * b ∈ (H₁ ∪ H₂ : Set G)`

tho.

#### Kevin Buzzard (Jul 18 2023 at 15:11):

Is this a Lean question or a maths question?

#### Martin Dvořák (Jul 18 2023 at 15:18):

Lean question. I have:

`a ∈ (H₁ ∪ H₂ : Set G)`

`b ∈ (H₁ ∪ H₂ : Set G)`

`IsA (Subgroup G) (H₁ ∪ H₂)`

I need:

`a * b ∈ (H₁ ∪ H₂ : Set G)`

I just don't know how to access `mul_mem'`

of the hypothesis.

#### Martin Dvořák (Jul 18 2023 at 15:21):

I have trouble switching between viewing `H₁ ∪ H₂`

as a set and viewing `H₁ ∪ H₂`

as a structure.

#### Kyle Miller (Jul 18 2023 at 15:26):

This `IsA`

thing isn't great to work with directly. In this message I gave a couple tactics to eliminate it

#### Martin Dvořák (Jul 18 2023 at 15:29):

Is there a mathlib declaration that would allow me to say " `H₁ ∪ H₂`

is a subgroup of `G`

"?

#### Kyle Miller (Jul 18 2023 at 15:32):

Yeah, docs#IsSubgroup. See also this thread from today, which this topic is continuing.

Last updated: Dec 20 2023 at 11:08 UTC