awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h_1 :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
h : c⁻¹ * x * c⁻¹⁻¹ ∈ N
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (h : c⁻¹ * x * c ∈ N), c⁻¹ * x * c ∈ N
⊢ c⁻¹ * x * c ∈ N

Tactic:
rwa [inv_inv] at h

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
refine_2 : x * c * c⁻¹ = x
⊢ (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
        (a : ↥N) → ↥N)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c⁻¹ * x * c) ⋯) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx

Tactic:
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]

Premises used: mul_assoc, MulEquiv.coe_toMonoidHom, MonoidHom.restrict_apply, MulAut.conj_apply, MonoidHom.codRestrict_apply, Subtype.mk_eq_mk, mul_inv_cancel, one_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
refine_2 : x * (c * c⁻¹) = x
refine_2₁ : x * 1 = x
refine_2₂ refine_2₃ : x = x
⊢ x * c * c⁻¹ = x

Tactic:
rw [mul_assoc, mul_inv_cancel, mul_one]

Premises used: mul_assoc, mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
⊢ Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)

Tactic:
have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.restrict N).codRestrict _ h) := by
    rintro ⟨x, hx⟩
    refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
    · have h := hn.conj_mem _ hx c⁻¹
      rwa [inv_inv] at h
    simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
    rw [mul_assoc, mul_inv_cancel, mul_one]
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
rw :
  map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      ⊤ ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}
⊢ Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}) ⊤

Tactic:
rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]

Premises used: Iff.mpr, eq_top_iff, MonoidHom.range_eq_map, MonoidHom.range_eq_top
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
grw :
  map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      ⊤ ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}

Tactic:
grw [eq_top_iff.1 ht]

Premises used: eq_top_iff, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}

Tactic:
map_le_iff_le_comap.2 (normalClosure_le_normal ?_)

Premises used: Iff.mpr, Subgroup.map_le_iff_le_comap, Subgroup.normalClosure_le_normal
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
refine :
  {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg} ⊆
    (↑(comap
          (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N
            h)
          (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})) :
      Set ↥N)
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ≤
    normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}

Tactic:
refine map_le_iff_le_comap.2 (normalClosure_le_normal ?_)

Premises used: Iff.mpr, Subgroup.map_le_iff_le_comap, Subgroup.normalClosure_le_normal
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
rw :
  Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg ∈
    comap
      (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
⊢ {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg} ⊆
    (↑(comap
          (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N
            h)
          (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})) :
      Set ↥N)

Tactic:
rw [Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
simp :
  Membership.mem (γ := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
    (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) ⋯)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg ∈
    comap
      (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h)
      (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})

Tactic:
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
    MonoidHom.restrict_apply, mem_comap]

Premises used: MulEquiv.coe_toMonoidHom, MonoidHom.restrict_apply, Subgroup.mem_comap, MulAut.conj_apply, MonoidHom.codRestrict_apply
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ Membership.mem (γ := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
    (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) ⋯)

Tactic:
subset_normalClosure (Set.mem_singleton _)

Premises used: Set.mem_singleton, Subgroup.subset_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
hs :
  Surjective (α := ↥N) (β := ↥N)
    (⇑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h) :
      (a : ↥N) → ↥N)
⊢ Membership.mem (γ := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'})
    (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) ⋯)

Tactic:
exact subset_normalClosure (Set.mem_singleton _)

Premises used: Set.mem_singleton, Subgroup.subset_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_6
inst : Monoid G
g : ConjClasses G
⊢ Membership.mem (γ := Set (ConjClasses G)) (noncenter G) g ↔ g.carrier.Nontrivial

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Nontrivial, ConjClasses.noncenter
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G_1 : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G_1
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
N : Type u_5
inst_4 : Group N
M : Type u_6
inst_5 : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_6 : Group G
inst_7 : MulAction G M
a b : G
ha : Membership.mem (γ := Set G) {σ : G | ∀ (x : M), σ • x - x ∈ I} a
hb : Membership.mem (γ := Set G) {σ : G | ∀ (x : M), σ • x - x ∈ I} b
x : M
⊢ (a * b) • x - x ∈ I

Tactic:
simpa [mul_smul] using add_mem (ha (b • x)) (hb x)

Premises used: AddMemClass.add_mem, HSMul.hSMul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G_1 : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G_1
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
N : Type u_5
inst_4 : Group N
M : Type u_6
inst_5 : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_6 : Group G
inst_7 : MulAction G M
⊢ Membership.mem (γ := Set G) {σ : G | ∀ (x : M), σ • x - x ∈ I} 1

Tactic:
simp [zero_mem]

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G_1 : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G_1
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
N : Type u_5
inst_4 : Group N
M : Type u_6
inst_5 : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_6 : Group G
inst_7 : MulAction G M
a : G
ha : Membership.mem (γ := Set G) {σ : G | ∀ (x : M), σ • x - x ∈ I} a
x : M
⊢ a⁻¹ • x - x ∈ I

Tactic:
simpa using sub_mem_comm_iff.mp (ha (a⁻¹ • x))

Premises used: Inv.inv, Iff.mp, HSMul.hSMul, sub_mem_comm_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
M : Type u_6
inst : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_1 : Group G
inst_2 : MulAction G M
σ : G
⊢ Membership.mem (γ := Subgroup G) (I.inertia G) σ ↔ ∀ (x : M), σ • x - x ∈ I

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
M : Type u_6
inst : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_1 : Group G
inst_2 : MulAction G M
H : Subgroup G
⊢ Subgroup.subgroupOf (I.inertia G) H = I.inertia ↥H

Tactic:
rfl

Premises used: Subgroup.subgroupOf, Set.Mem, setOf, Set.preimage, Subgroup.comap, AddSubgroup.inertia, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
M : Type u_6
inst : AddGroup M
I : AddSubgroup M
G : Type u_7
inst_1 : Group G
inst_2 : MulAction G M
H : Subgroup G
rw : Subgroup.map H.subtype (Subgroup.subgroupOf (I.inertia G) H) = I.inertia G ⊓ H
rw₁ rw₂ : I.inertia G ⊓ H = I.inertia G ⊓ H
⊢ Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H

Tactic:
rw [← AddSubgroup.subgroupOf_inertia, Subgroup.subgroupOf_map_subtype]

Premises used: AddSubgroup.subgroupOf_inertia, Subgroup.subgroupOf_map_subtype
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
S : Type u_3
G : Type u_4
inst : Inv G
inst_1 : SetLike S G
s : S
inst_2 : HasMemOrInvMem s
x : G
h : ¬x ∈ s
⊢ x ∈ s ∨ x⁻¹ ∈ s

Tactic:
have := mem_or_inv_mem s x
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
S : Type u_3
G : Type u_4
inst : Inv G
inst_1 : SetLike S G
s : S
inst_2 : HasMemOrInvMem s
x : G
h : ¬x ∈ s
this : x ∈ s ∨ x⁻¹ ∈ s
⊢ x⁻¹ ∈ s

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
S : Type u_3
G : Type u_4
inst : Inv G
inst_1 : SetLike S G
s : S
inst_2 : HasMemOrInvMem s
x : G
h : ¬x⁻¹ ∈ s
⊢ x ∈ s ∨ x⁻¹ ∈ s

Tactic:
have := mem_or_inv_mem s x
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
S : Type u_3
G : Type u_4
inst : Inv G
inst_1 : SetLike S G
s : S
inst_2 : HasMemOrInvMem s
x : G
h : ¬x⁻¹ ∈ s
this : x ∈ s ∨ x⁻¹ ∈ s
⊢ x ∈ s

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
S : Type u_3
G : Type u_4
inst : InvolutiveInv G
x_1 : SetLike S G
inst_1 : InvMemClass S G
H : S
x : G
⊢ x⁻¹ ∈ H ↔ x ∈ H

Tactic:
⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩

Premises used: Eq.rec, InvMemClass.inv_mem, inv_inv, Iff.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
rw : x * y⁻¹ ∈ H
⊢ x / y ∈ H

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H

Tactic:
mul_mem hx (inv_mem hy)

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H

Tactic:
exact mul_mem hx (inv_mem hy)

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
rw : x ^ n ∈ K
⊢ HPow.hPow (β := ℤ) x (↑n : ℤ) ∈ K

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K

Tactic:
pow_mem hx n

Premises used: pow_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K

Tactic:
exact pow_mem hx n

Premises used: pow_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
rw : (x ^ (n + 1))⁻¹ ∈ K
⊢ x ^ -[n+1] ∈ K

Tactic:
rw [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K

Tactic:
inv_mem (pow_mem hx n.succ)

Premises used: InvMemClass.inv_mem, pow_mem, Nat.succ
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
M : Type u_3
S : Type u_4
inst : DivInvMonoid M
inst_1 : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K

Tactic:
exact inv_mem (pow_mem hx n.succ)

Premises used: InvMemClass.inv_mem, pow_mem, Nat.succ
-- 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
P : G → Prop
mp : (∃ (x : G), x ∈ H ∧ P x⁻¹) → ∃ (x : G), x ∈ H ∧ P x
mpr : (∃ (x : G), x ∈ H ∧ P x) → ∃ (x : G), x ∈ H ∧ P x⁻¹
⊢ (∃ (x : G), x ∈ H ∧ P x⁻¹) ↔ ∃ (x : G), x ∈ H ∧ P x

Tactic:
constructor
-- 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
P : G → Prop
x : G
x_in : x ∈ H
hx : P x⁻¹
⊢ P x⁻¹

Tactic:
simp [hx]
-- 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
P : G → Prop
x : G
x_in : x ∈ H
hx : P x⁻¹
⊢ ∃ (x : G), x ∈ H ∧ P x

Tactic:
exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩
-- 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
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ P x⁻¹⁻¹

Tactic:
simp [hx]
-- 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
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ (x : G), x ∈ H ∧ P x⁻¹

Tactic:
exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩
-- 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 y : G
h : x ∈ H
hba : y * x ∈ H
⊢ y ∈ H

Tactic:
simpa using mul_mem hba (inv_mem h)

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- 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 y : G
h : x ∈ H
hab : x * y ∈ H
⊢ y ∈ H

Tactic:
simpa using mul_mem (inv_mem h) hab

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- 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
⊢ (↑x⁻¹ : G) = (↑x : G)⁻¹

Tactic:
rfl

Premises used: 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 L : S
⊢ (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G) ↔ H ≤ K ∨ H ≤ L

Tactic:
⟨fun h ↦ ?_, fun h x xH ↦ h.imp (mem_of_le_of_mem · xH) (mem_of_le_of_mem · xH)⟩

Premises used: mem_of_le_of_mem, Iff.intro, Or.imp
-- 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 L : S
refine : ∀ (h : (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G)), H ≤ K ∨ H ≤ L
⊢ (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G) ↔ H ≤ K ∨ H ≤ L

Tactic:
refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (mem_of_le_of_mem · xH) (mem_of_le_of_mem · xH)⟩
-- 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 L : S
h : (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G)
rw : (∃ (x : G), x ∈ H ∧ ¬x ∈ K) → (↑H : Set G) ⊆ (↑L : Set G)
⊢ H ≤ K ∨ H ≤ L

Tactic:
rw [or_iff_not_imp_left, SetLike.not_le_iff_exists, ← SetLike.coe_subset_coe]

Premises used: SetLike.coe_subset_coe, Classical.or_iff_not_imp_left, SetLike.not_le_iff_exists
-- 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 L : S
h : (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G)
⊢ (∃ (x : G), x ∈ H ∧ ¬x ∈ K) → (↑H : Set G) ⊆ (↑L : Set G)

Tactic:
fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp

Premises used: Membership.mem, Or.resolve_left, Set.Subset, SetLike.coe, Iff.mp, Or.elim, _private.0.SubgroupClass.subset_union.match_1, mul_mem_cancel_right, mul_mem_cancel_left, MulMemClass.mul_mem
-- 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 L : S
h : (↑H : Set G) ⊆ (↑K : Set G) ∪ (↑L : Set G)
⊢ (∃ (x : G), x ∈ H ∧ ¬x ∈ K) → (↑H : Set G) ⊆ (↑L : Set G)

Tactic:
exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp
-- 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 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
S : Type u_4
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
x : ↥H
⊢ ((↑H : [inst_3 : SetLike S G] → [inst_4 : SubgroupClass S G] → ↥H →* G) : (a : ↥H) → G) x = (↑x : G)

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
⊢ Injective (α := ↥H) (β := G) (⇑(↑H : [inst_3 : SetLike S G] → [inst_4 : SubgroupClass S G] → ↥H →* G) : (a : ↥H) → G)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- 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
⊢ Eq (α := (a : ↥H) → G) (⇑(↑H : [inst_3 : SetLike S G] → [inst_4 : SubgroupClass S G] → ↥H →* G) : (a : ↥H) → G)
    (Subtype.val (p := fun (x : G) ↦ x ∈ H))

Tactic:
rfl