How to write known conditions

Stream: new members

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic

variable (G : Type _ ) [Group G]

set_option autoImplicit false

example (H₁ H₂ : Subgroup G) (h : H₁ ∪ H₂ : Subgroup G ) : H₁ ⊆ H₂ ∨ H₂ ⊆ H₁ := by
  sorry

Can I ask what is wrong with me describing H1 and H2 is still being subgroups

[Eric Wieser]

You can't write h : x : X to mean "a proof that x has type X"

[Eric Wieser]

What you probably want is ∃ H12 : Subgroup G, (H12 : Set G) = H₁ ∪ H₂

[Eric Wieser]

Which says "there is some subgroup H12 that has the same elements as the union of the elements of H1 and H2"

[Kyle Miller]

The predicate is marked as being deprecated, but a natural way to write this is (h : IsSubgroup (H₁ ∪ H₂)). (I'm not sure the predicate docs#IsSubgroup is really deprecated; it's more that if you're working with subgroups you should strongly prefer terms of Subgroup. However, in this case the question really is about whether a given set is a subgroup.)

Eric's (h : ∃ H12 : Subgroup G, (H12 : Set G) = H₁ ∪ H₂) is good too.

[Kyle Miller]

By the way, the conclusion should be written as H₁ ≤ H₂ ∨ H₂ ≤ H₁ since we use ≤ for everything that's not a Set. (This is the symbol for posets in general.)

[Kyle Miller]

@Eric Wieser Should there be some sort of predicate that SetLike provides for this existential version?

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
  sorry

[Kyle Miller]

With some notation, then we could make something that looks like h : x : X, which is kind of fun.

notation:0 s ":~" t => IsA t s

example (H₁ H₂ : Subgroup G) (h : H₁ ∪ H₂ :~ Subgroup G) : H₁ ≤ H₂ ∨ H₂ ≤ H₁ := by
  sorry

(I doubt this comes up enough in mathlib where notation is worth it though.)

[Eric Wieser]

I think it would be better to go the other way

[Kyle Miller]

What's the thing here that has directions to go?

[Eric Wieser]

Defining Subgroup in terms of IsSubgroup, perhaps simply as { S : Set G // IsSubgroup G }

[tsuki hao]

Thanks to all of you, I have successfully resolved this issue！