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


#### 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 "?