How to use h'

Stream: new members

[tsuki hao]

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]

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]

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]

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]

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]

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]

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

[Martin Dvořák]

Thanks. I updated the post above.

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

[Kevin Buzzard]

Is this a Lean question or a maths question?

[Martin Dvořák]

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]

I have trouble switching between viewing H₁ ∪ H₂ as a set and viewing H₁ ∪ H₂ as a structure.

[Kyle Miller]

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

[Martin Dvořák]

Is there a mathlib declaration that would allow me to say " H₁ ∪ H₂ is a subgroup of G "?

[Kyle Miller]

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