awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
x : ↥H
n : ℕ
⊢ (↑(x ^ n) : G) = (↑x : G) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
x : ↥H
n : ℤ
⊢ (↑(x ^ n) : G) = (↑x : G) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : Preorder S
inst_4 : IsConcreteLE S G
x : ↥H
mk :
  ∀ (val : G) (property : val ∈ H),
    (inclusion ⋯ : (a : ↥H) → ↥H) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property) =
      Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property
⊢ (inclusion ⋯ : (a : ↥H) → ↥H) x = x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : Preorder S
inst_4 : IsConcreteLE S G
val : G
property : val ∈ H
⊢ (inclusion ⋯ : (a : ↥H) → ↥H) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
h : H ≤ K
x : G
hx : x ∈ H
⊢ (inclusion h : (a : ↥H) → ↥K) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) x hx) = Subtype.mk (p := fun (x : G) ↦ x ∈ K) x ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
h : H ≤ K
x : ↥K
hx : (↑x : G) ∈ H
mk :
  ∀ (val : G) (property : val ∈ K) (hx : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property) : G) ∈ H),
    (inclusion h : (a : ↥H) → ↥K)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property) : G) hx) =
      Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property
⊢ (inclusion h : (a : ↥H) → ↥K) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑x : G) hx) = x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
h : H ≤ K
val : G
property : val ∈ K
hx : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property) : G) ∈ H
⊢ (inclusion h : (a : ↥H) → ↥K)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property) : G) hx) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ K) val property

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : Preorder S
inst_4 : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
x : ↥H
mk :
  ∀ (val : G) (property : val ∈ H),
    Eq (α := ↥L)
      ((inclusion hKL : (a : ↥K) → ↥L)
          ((inclusion hHK : (a : ↥H) → ↥K) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property)) :
        ↥L)
      ((inclusion ⋯ : (a : ↥H) → ↥L) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property) : ↥L)
⊢ Eq (α := ↥L) ((inclusion hKL : (a : ↥K) → ↥L) ((inclusion hHK : (a : ↥H) → ↥K) x) : ↥L)
    ((inclusion ⋯ : (a : ↥H) → ↥L) x : ↥L)

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
H K : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : Preorder S
inst_4 : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
val : G
property : val ∈ H
⊢ Eq (α := ↥L)
    ((inclusion hKL : (a : ↥K) → ↥L)
        ((inclusion hHK : (a : ↥H) → ↥K) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property)) :
      ↥L)
    ((inclusion ⋯ : (a : ↥H) → ↥L) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) val property) : ↥L)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
H K : S
h : H ≤ K
a : ↥H
⊢ (↑((inclusion h : (a : ↥H) → ↥K) a) : G) = (↑a : G)

Tactic:
Set.coe_inclusion (SetLike.coe_subset_coe.mpr h) a

Premises used: Iff.mpr, SetLike.coe_subset_coe, Set.coe_inclusion
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Type u_4
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
inst_3 : LE S
inst_4 : IsConcreteLE S G
H K : S
h : H ≤ K
⊢ Eq (α := ↥H →* G)
    (MonoidHom.comp (↑K : [inst_5 : SetLike S G] → [inst_6 : SubgroupClass S G] → ↥K →* G) (inclusion h))
    (↑H : [inst_5 : SetLike S G] → [inst_6 : SubgroupClass S G] → ↥H →* G)

Tactic:
rfl

Premises used: Set.Mem, SubgroupClass.subtype, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
p q : Subgroup G
h : Eq.{u_1 + 1} (α := Set G) ((fun (s : Subgroup G) ↦ s.carrier) p) ((fun (s : Subgroup G) ↦ s.carrier) q)
obtain :
  ∀ (hp : Set G) (mul_mem' : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp)
    (one_mem' : 1 ∈ { carrier := hp, mul_mem' := @mul_mem' : Subsemigroup G }.carrier)
    (inv_mem' :
      ∀ {x : G},
        x ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier →
          x⁻¹ ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set G)
        ((fun (s : Subgroup G) ↦ s.carrier)
          { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
        ((fun (s : Subgroup G) ↦ s.carrier) q)),
    { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } = q
⊢ p = q

Tactic:
obtain ⟨⟨⟨hp, _⟩, _⟩, _⟩ := p
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
q : Subgroup G
hp : Set G
mul_mem' : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem' : 1 ∈ { carrier := hp, mul_mem' := @mul_mem' : Subsemigroup G }.carrier
inv_mem' :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (s : Subgroup G) ↦ s.carrier)
      { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
    ((fun (s : Subgroup G) ↦ s.carrier) q)
obtain :
  ∀ (hq : Set G) (mul_mem'_1 : ∀ {a b : G}, a ∈ hq → b ∈ hq → a * b ∈ hq)
    (one_mem'_1 : 1 ∈ { carrier := hq, mul_mem' := @mul_mem'_1 : Subsemigroup G }.carrier)
    (inv_mem'_1 :
      ∀ {x : G},
        x ∈ { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1 : Submonoid G }.carrier →
          x⁻¹ ∈ { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1 : Submonoid G }.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set G)
        ((fun (s : Subgroup G) ↦ s.carrier)
          { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
        ((fun (s : Subgroup G) ↦ s.carrier)
          { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1, inv_mem' := @inv_mem'_1 })),
    { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } =
      { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1, inv_mem' := @inv_mem'_1 }
⊢ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } = q

Tactic:
obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
hp : Set G
mul_mem' : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem' : 1 ∈ { carrier := hp, mul_mem' := @mul_mem' : Subsemigroup G }.carrier
inv_mem' :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid G }.carrier
hq : Set G
mul_mem'_1 : ∀ {a b : G}, a ∈ hq → b ∈ hq → a * b ∈ hq
one_mem'_1 : 1 ∈ { carrier := hq, mul_mem' := @mul_mem'_1 : Subsemigroup G }.carrier
inv_mem'_1 :
  ∀ {x : G},
    x ∈ { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1 : Submonoid G }.carrier →
      x⁻¹ ∈ { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1 : Submonoid G }.carrier
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (s : Subgroup G) ↦ s.carrier)
      { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' })
    ((fun (s : Subgroup G) ↦ s.carrier)
      { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1, inv_mem' := @inv_mem'_1 })
⊢ { carrier := hp, mul_mem' := @mul_mem', one_mem' := one_mem', inv_mem' := @inv_mem' : Subgroup G } =
    { carrier := hq, mul_mem' := @mul_mem'_1, one_mem' := one_mem'_1, inv_mem' := @inv_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
x : G
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s : Submonoid G
x : G
h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier
⊢ x ∈ { toSubmonoid := s, inv_mem' := @h_inv : Subgroup G } ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s : Submonoid G
h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier
⊢ (↑{ toSubmonoid := s, inv_mem' := @h_inv : Subgroup G } : Set G) = (↑s : Set G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s t : Submonoid G
h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier
h_inv' : ∀ {x : G}, x ∈ t.carrier → x⁻¹ ∈ t.carrier
⊢ { toSubmonoid := s, inv_mem' := @h_inv : Subgroup G } ≤ { toSubmonoid := t, inv_mem' := @h_inv' } ↔ s ≤ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
⊢ (↑K.toSubmonoid : Set G) = (↑K : Set G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
x : G
⊢ x ∈ K.toSubmonoid ↔ x ∈ K

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
⊢ (↑p.toSubmonoid : Set G) = (↑q.toSubmonoid : Set G)

Tactic:
have := SetLike.ext'_iff.1 h
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : (↑p.toSubmonoid : Set G) = (↑q.toSubmonoid : Set G)
⊢ (↑p : Set G) = (↑q : Set G)

Tactic:
rw [coe_toSubmonoid, coe_toSubmonoid] at this

Premises used: Subgroup.coe_toSubmonoid
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : (↑p : Set G) = (↑q : Set G)
⊢ p = q

Tactic:
SetLike.ext'_iff.2 this

Premises used: Iff.mpr, SetLike.ext'_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : (↑p : Set G) = (↑q : Set G)
⊢ p = q

Tactic:
exact SetLike.ext'_iff.2 this

Premises used: Iff.mpr, SetLike.ext'_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
⊢ p.toSubmonoid = q.toSubmonoid ↔ p = q

Tactic:
toSubmonoid_injective.eq_iff

Premises used: Function.Injective.eq_iff, Subgroup.toSubmonoid_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
⊢ StrictMono.{u_1, u_1} (α := Subgroup G) toSubmonoid

Tactic:
fun _ _ =>
  id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
⊢ Monotone.{u_1, u_1} (α := Subgroup G) toSubmonoid

Tactic:
toSubmonoid_strictMono.monotone

Premises used: StrictMono.monotone, Subgroup.toSubmonoid_strictMono
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
p q : Subgroup G
⊢ p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ (↑s : Set G).Nonempty

Tactic:
⟨1, one_mem _⟩

Premises used: Set.Nonempty, Exists.intro, OneMemClass.one_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K_1 K : Subgroup G
s : Set G
hs : s = (↑K : Set G)
x : G
hx : x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
simpa [hs] using hx
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
s : Set G
hs : s = (↑K : Set G)
⊢ K.copy s hs = K

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : ∀ (x : G), x ∈ H ↔ x ∈ K
⊢ H = K

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ 1 ∈ H

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : G
⊢ x ∈ H → y ∈ H → x * y ∈ H

Tactic:
mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
⊢ x ∈ H → x⁻¹ ∈ H

Tactic:
inv_mem

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : G
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
div_mem hx hy

Premises used: div_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
⊢ x⁻¹ ∈ H ↔ x ∈ H

Tactic:
inv_mem_iff

Premises used: Set.Mem, inv_mem_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
P : G → Prop
⊢ (∃ (x : G), x ∈ K ∧ P x⁻¹) ↔ ∃ (x : G), x ∈ K ∧ P x

Tactic:
exists_inv_mem_iff_exists_mem

Premises used: exists_inv_mem_iff_exists_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : G
h : x ∈ H
⊢ y * x ∈ H ↔ y ∈ H

Tactic:
mul_mem_cancel_right h

Premises used: mul_mem_cancel_right
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : G
h : x ∈ H
⊢ x * y ∈ H ↔ y ∈ H

Tactic:
mul_mem_cancel_left h

Premises used: mul_mem_cancel_left
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
x : G
hx : x ∈ K
⊢ ∀ (n : ℕ), x ^ n ∈ K

Tactic:
pow_mem hx

Premises used: pow_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
x : G
hx : x ∈ K
⊢ ∀ (n : ℤ), x ^ n ∈ K

Tactic:
zpow_mem hx

Premises used: zpow_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
let : ∀ (x : G) (hx : x ∈ s), 1 ∈ s
⊢ 1 ∈ s

Tactic:
let ⟨x, hx⟩ := hsn
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
x : G
hx : x ∈ s
⊢ 1 ∈ s

Tactic:
simpa using hs x hx x hx
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
x : G
hx : x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
simpa using hs 1 one_mem x hx

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
inv_mem : ∀ (x : G), x ∈ s → x⁻¹ ∈ s
a b : G
hx : a ∈ s
hy : b ∈ s
⊢ a * b ∈ s

Tactic:
simpa using hs _ hx _ (inv_mem _ hy)
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : ↥H
⊢ (↑(x * y) : G) = (↑x : G) * (↑y : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq.{u_1 + 1} (α := G) (↑1 : G) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : ↥H
⊢ (↑x⁻¹ : G) = (↑x : G)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : ↥H
⊢ (↑(x / y) : G) = (↑x : G) / (↑y : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
hx : x ∈ H
⊢ (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) x hx) : G) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : ↥H
n : ℕ
⊢ (↑(x ^ n) : G) = (↑x : G) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : ↥H
n : ℤ
⊢ (↑(x ^ n) : G) = (↑x : G) ^ n

Tactic:
dsimp
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
h : g ∈ H
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) g h = 1 ↔ g = 1

Tactic:
Submonoid.mk_eq_one ..

Premises used: Set.Mem, Submonoid.mk_eq_one
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
x : ↥s
⊢ (s.subtype : (a : ↥s) → G) x = (↑x : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
s : Subgroup G
⊢ Injective (α := ↥s) (β := G) (⇑s.subtype : (a : ↥s) → G)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq (α := (a : ↥H) → G) (⇑H.subtype : (a : ↥H) → G) (Subtype.val (p := fun (x : G) ↦ x ∈ H))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
a : ↥H
⊢ (↑((inclusion h : (a : ↥H) → ↥K) a) : G) = (↑a : G)

Tactic:
Set.coe_inclusion h a

Premises used: Set.coe_inclusion
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ Injective (α := ↥H) (β := ↥K) (⇑(inclusion h) : (a : ↥H) → ↥K)

Tactic:
Set.inclusion_injective h

Premises used: Set.inclusion_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
x y : ↥H
⊢ Eq (α := ↥K) ((inclusion h : (a : ↥H) → ↥K) x : ↥K) ((inclusion h : (a : ↥H) → ↥K) y : ↥K) ↔ x = y

Tactic:
(inclusion_injective h).eq_iff

Premises used: Function.Injective.eq_iff, Subgroup.inclusion_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H ≤ K
⊢ K.subtype.comp (inclusion hH) = H.subtype

Tactic:
rfl

Premises used: Set.Mem, Subgroup.subtype, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H_1 : Subgroup G
inst_2 : IsMulCommutative G
H : Subgroup G
⊢ ∀ (n : G), n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H

Tactic:
simp [mul_comm']

Premises used: mul_comm'
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * n * g⁻¹⁻¹ ∈ H

Tactic:
nH.conj_mem n hn g⁻¹

Premises used: Inv.inv, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
h : g = g⁻¹⁻¹
⊢ g⁻¹ * n * g ∈ H

Tactic:
convert! nH.conj_mem n hn g⁻¹

Premises used: Inv.inv, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
h h₁ : g = g
⊢ g = g⁻¹⁻¹

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
⊢ a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H

Tactic:
have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
nH : H.Normal
a b : G
⊢ a * b ∈ H ↔ b * a ∈ H

Tactic:
⟨nH.mem_comm, nH.mem_comm⟩

Premises used: Subgroup.Normal.mem_comm, Iff.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
rw : a * (b * n * b⁻¹) * a⁻¹ ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S
⊢ n ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
rw [hb, ha]
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ a * (b * n * b⁻¹) * a⁻¹ ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
simp only [mul_assoc, mul_inv_rev]

Premises used: mul_assoc, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
⊢ Membership.mem (γ := Set G) {g : G | ∀ (n : G), n ∈ S ↔ g * n * g⁻¹ ∈ S} 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
rw : n ∈ S ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ S
⊢ n ∈ S ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ S

Tactic:
rw [ha (a⁻¹ * n * a⁻¹⁻¹)]

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ S

Tactic:
simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]

Premises used: mul_assoc, inv_inv, mul_inv_cancel, mul_one, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
⊢ Membership.mem (γ := Subgroup G) (normalizer S) g ↔ ∀ (h : G), h ∈ S ↔ g * h * g⁻¹ ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
rw : Membership.mem (γ := Subgroup G) (normalizer S) g⁻¹ ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
rw₁ : (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g⁻¹⁻¹ ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
rw₂ rw₃ : (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
⊢ Membership.mem (γ := Subgroup G) (normalizer S) g ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S

Tactic:
rw [← inv_mem_iff, mem_set_normalizer_iff, inv_inv]

Premises used: inv_mem_iff, Subgroup.mem_set_normalizer_iff, inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : Membership.mem (γ := Subgroup G) (normalizer S) g
n : G
rw : g * (n * g) * g⁻¹ ∈ S ↔ g * n ∈ S
rw₁ : g * (n * g * g⁻¹) ∈ S ↔ g * n ∈ S
rw₂ rw₃ : g * n ∈ S ↔ g * n ∈ S
⊢ n * g ∈ S ↔ g * n ∈ S

Tactic:
rw [h, mul_assoc, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
rw : n ∈ S ↔ g * (n * g⁻¹) ∈ S
rw₁ : n ∈ S ↔ n * g⁻¹ * g ∈ S
rw₂ rw₃ : n ∈ S ↔ n ∈ S
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S

Tactic:
rw [mul_assoc, ← h, inv_mul_cancel_right]

Premises used: mul_assoc, inv_mul_cancel_right