awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
⊢ ∃ (x : G), (x ∈ (↑A : Set G) ∧ x ∈ (↑B : Set G)) ∧ ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z

Tactic:
⟨y, ⟨?_, hy⟩, z, hz, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
h₁ : y ∈ (↑A : Set G)
⊢ ∃ (x : G), (x ∈ (↑A : Set G) ∧ x ∈ (↑B : Set G)) ∧ ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z

Tactic:
refine ⟨y, ⟨?_, hy⟩, z, hz, rfl⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
this : y * z * z⁻¹ ∈ A
⊢ y ∈ (↑A : Set G)

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
h₁ : y * z * z⁻¹ ∈ A
⊢ y ∈ (↑A : Set G)

Tactic:
suffices y * z * z⁻¹ ∈ A by simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
⊢ y * z * z⁻¹ ∈ A

Tactic:
mul_mem hyz (inv_mem (h hz))

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
⊢ y * z * z⁻¹ ∈ A

Tactic:
exact mul_mem hyz (inv_mem (h hz))

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s : G
hs : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) s
g : G
hg : g ∈ H ⊔ K
⊢ (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K

Tactic:
simp only [mem_inf, mem_normalizer_iff] at hs

Premises used: Subgroup.mem_normalizer_iff, Subgroup.mem_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : g ∈ H ⊔ K
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
⊢ Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g

Tactic:
rw [sup_eq_closure] at hg

Premises used: Subgroup.sup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : g ∈ H ⊔ K
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
hg₁ : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
⊢ (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K

Tactic:
rw [sup_eq_closure] at hg

Premises used: Subgroup.sup_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
⊢ s * g * s⁻¹ ∈ H ⊔ K

Tactic:
closure_induction ?_ ?_ ?_ ?_ hg

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
refine_1 : ∀ (x : G) (hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
refine_2 : s * 1 * s⁻¹ ∈ H ⊔ K
refine_3 :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x)
    (hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y),
    s * x * s⁻¹ ∈ H ⊔ K → s * y * s⁻¹ ∈ H ⊔ K → s * (x * y) * s⁻¹ ∈ H ⊔ K
refine_4 :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x),
    s * x * s⁻¹ ∈ H ⊔ K → s * x⁻¹ * s⁻¹ ∈ H ⊔ K
⊢ s * g * s⁻¹ ∈ H ⊔ K

Tactic:
refine closure_induction ?_ ?_ ?_ ?_ hg
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
refine_1 : ∀ (hl : x ∈ (↑H : Set G)), s * x * s⁻¹ ∈ H ⊔ K
refine_1₁ : ∀ (hr : x ∈ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
⊢ s * x * s⁻¹ ∈ H ⊔ K

Tactic:
obtain hl | hr := (mem_union x _ _).mpr hx

Premises used: Set.mem_union, Iff.mpr
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
hl : x ∈ (↑H : Set G)
rwa rwa₁ rwa₂ rwa₃ : x ∈ H
⊢ s * x * s⁻¹ ∈ H

Tactic:
rwa [← hs.1]

Premises used: And.left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
hl : x ∈ (↑H : Set G)
⊢ s * x * s⁻¹ ∈ H ⊔ K

Tactic:
exact mem_sup_left (by rwa [← hs.1])

Premises used: Subgroup.mem_sup_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
hr : x ∈ (↑K : Set G)
rwa rwa₁ rwa₂ rwa₃ : x ∈ K
⊢ s * x * s⁻¹ ∈ K

Tactic:
rwa [← hs.2]

Premises used: And.right
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
hr : x ∈ (↑K : Set G)
⊢ s * x * s⁻¹ ∈ H ⊔ K

Tactic:
exact mem_sup_right (by rwa [← hs.2])

Premises used: Subgroup.mem_sup_right
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
⊢ s * 1 * s⁻¹ ∈ H ⊔ K

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x y : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y
hsx : s * x * s⁻¹ ∈ H ⊔ K
hsy : s * y * s⁻¹ ∈ H ⊔ K
⊢ s * (x * y) * s⁻¹ = s * x * s⁻¹ * (s * y * s⁻¹)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x y : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y
hsx : s * x * s⁻¹ ∈ H ⊔ K
hsy : s * y * s⁻¹ ∈ H ⊔ K
refine_3 : s * x * s⁻¹ * (s * y * s⁻¹) ∈ H ⊔ K
⊢ s * (x * y) * s⁻¹ ∈ H ⊔ K

Tactic:
rw [show s * (x * y) * s⁻¹ = (s * x * s⁻¹) * (s * y * s⁻¹) by simp]
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x y : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y
hsx : s * x * s⁻¹ ∈ H ⊔ K
hsy : s * y * s⁻¹ ∈ H ⊔ K
⊢ s * x * s⁻¹ * (s * y * s⁻¹) ∈ H ⊔ K

Tactic:
mul_mem hsx hsy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x y : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y
hsx : s * x * s⁻¹ ∈ H ⊔ K
hsy : s * y * s⁻¹ ∈ H ⊔ K
⊢ s * x * s⁻¹ * (s * y * s⁻¹) ∈ H ⊔ K

Tactic:
exact mul_mem hsx hsy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hsx : s * x * s⁻¹ ∈ H ⊔ K
⊢ (s * x⁻¹ * s⁻¹)⁻¹ ∈ H ⊔ K

Tactic:
simpa [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hsx : s * x * s⁻¹ ∈ H ⊔ K
⊢ s * x⁻¹ * s⁻¹ ∈ H ⊔ K

Tactic:
exact inv_mem_iff.mp (by simpa [← mul_assoc])

Premises used: inv_mem_iff, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s : G
hs : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) s
g : G
⊢ g ∈ (↑(H ⊔ K) : Set G) ↔ s * g * s⁻¹ ∈ (↑(H ⊔ K) : Set G)

Tactic:
⟨conj_mem_sup_of_mem_inf_normalizer_of_mem_inf hs g, ?_⟩

Premises used: Iff.intro, Subgroup.conj_mem_sup_of_mem_inf_normalizer_of_mem_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s : G
hs : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) s
g : G
refine : s * g * s⁻¹ ∈ (↑(H ⊔ K) : Set G) → g ∈ (↑(H ⊔ K) : Set G)
⊢ g ∈ (↑(H ⊔ K) : Set G) ↔ s * g * s⁻¹ ∈ (↑(H ⊔ K) : Set G)

Tactic:
refine ⟨conj_mem_sup_of_mem_inf_normalizer_of_mem_inf hs g, ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s : G
hs : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) s
g : G
⊢ s * g * s⁻¹ ∈ (↑(H ⊔ K) : Set G) → g ∈ (↑(H ⊔ K) : Set G)

Tactic:
simpa [← mul_assoc] using conj_mem_sup_of_mem_inf_normalizer_of_mem_inf (inv_mem hs) (s * g * s⁻¹)

Premises used: HMul.hMul, mul_assoc, InvMemClass.inv_mem, Inv.inv, Subgroup.conj_mem_sup_of_mem_inf_normalizer_of_mem_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
hHnK : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑K : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(H ⊔ K) : Set G))

Tactic:
(inf_of_le_left hHnK).symm.trans_le (H.normalizer_inf_normalizer_le_normalizer_sup K)

Premises used: inf_of_le_left, Eq.trans_le, Subgroup.normalizer_inf_normalizer_le_normalizer_sup, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
hHnK : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑K : Set G))
rw : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(H ⊔ K) : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(K ⊔ H) : Set G))

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
hHnK : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑K : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(H ⊔ K) : Set G))

Tactic:
normalizer_le_normalizer_sup_of_normalizer_le_left hHnK

Premises used: Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
hHnK : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑K : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(H ⊔ K) : Set G))

Tactic:
exact normalizer_le_normalizer_sup_of_normalizer_le_left hHnK

Premises used: Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
hK : K.Normal
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(H ⊔ K) : Set G))

Tactic:
normalizer_le_normalizer_sup_of_normalizer_le_left le_normalizer_of_normal

Premises used: Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_left, Subgroup.le_normalizer_of_normal
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ H ⊔ K
g : G
rw : ∀ (hmem : n ∈ (↑H : Set G) * (↑K : Set G)) (g : G), g * n * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)
⊢ g * n * g⁻¹ ∈ H ⊔ K

Tactic:
rw [← SetLike.mem_coe, normal_mul] at hmem ⊢

Premises used: Subgroup.normal_mul, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ (↑H : Set G) * (↑K : Set G)
g : G
rcases :
  ∀ (h : G) (hh : h ∈ (↑H : Set G)) (k : G) (hk : k ∈ (↑K : Set G)),
    g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)
⊢ g * n * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)

Tactic:
rcases hmem with ⟨h, hh, k, hk, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
⊢ g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)

Tactic:
⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, Inv.inv, Set.image2, And.intro, Exists.intro, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
refine : (fun (x1 x2 : G) ↦ x1 * x2) (g * h * g⁻¹) (g * k * g⁻¹) = g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹
⊢ g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)

Tactic:
refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
⊢ (fun (x1 x2 : G) ↦ x1 * x2) (g * h * g⁻¹) (g * k * g⁻¹) = g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹

Tactic:
simp only [mul_assoc, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
x : X
hx : x ∈ t
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := G) 1 x ∈ t

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g' • x ∈ t

Tactic:
hst g' hg' x hx
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g' • x ∈ t

Tactic:
exact hst g' hg' x hx
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g'⁻¹ • x ∈ t

Tactic:
hst g'⁻¹ (hs g' hg') x hx

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g g' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g'⁻¹ • x ∈ t

Tactic:
exact hst g'⁻¹ (hs g' hg') x hx

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x_1 y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure s) x_1
hy : Membership.mem (γ := Subgroup G) (closure s) y
h₁ : ∀ {x : X} (hx : x ∈ t), x_1 • x ∈ t
h₂ : ∀ {x : X} (hx : x ∈ t), y • x ∈ t
x : X
hx : x ∈ t
mul : x_1 • y • x ∈ t
⊢ (x_1 * y) • x ∈ t

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x_1 y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure s) x_1
hy : Membership.mem (γ := Subgroup G) (closure s) y
h₁ : ∀ {x : X} (hx : x ∈ t), x_1 • x ∈ t
h₂ : ∀ {x : X} (hx : x ∈ t), y • x ∈ t
x : X
hx : x ∈ t
⊢ x_1 • y • x ∈ t

Tactic:
h₁ (h₂ hx)
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x_1 y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure s) x_1
hy : Membership.mem (γ := Subgroup G) (closure s) y
h₁ : ∀ {x : X} (hx : x ∈ t), x_1 • x ∈ t
h₂ : ∀ {x : X} (hx : x ∈ t), y • x ∈ t
x : X
hx : x ∈ t
⊢ x_1 • y • x ∈ t

Tactic:
exact h₁ (h₂ hx)
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : Membership.mem (γ := Subgroup G) (closure s) g
x : X
hx : x ∈ t
one : ∀ {x : X} (hx : x ∈ t), HSMul.hSMul.{u_2, u_5, u_5} (α := G) 1 x ∈ t
mem : ∀ (g' : G) (hg' : g' ∈ s) {x : X} (hx : x ∈ t), g' • x ∈ t
inv_mem : ∀ (g' : G) (hg' : g' ∈ s) {x : X} (hx : x ∈ t), g'⁻¹ • x ∈ t
mul :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure s) x →
      Membership.mem (γ := Subgroup G) (closure s) y →
        ∀ (h₁ : ∀ {x_1 : X} (hx : x_1 ∈ t), x • x_1 ∈ t) (h₂ : ∀ {x : X} (hx : x ∈ t), y • x ∈ t) {x_1 : X}
          (hx : x_1 ∈ t), (x * y) • x_1 ∈ t
⊢ g • x ∈ t

Tactic:
induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)

Premises used: Subgroup.mul, InvMemClass.inv_mem, Subgroup.one, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ Eq (α := Set G) ((fun (y : G) ↦ h • y) '' (fun (x : G) ↦ g * x) ⁻¹' s)
    (preimage (β := G) (fun (x : G) ↦ g * x) ((fun (y : G) ↦ h • y) '' s))

Tactic:
simp [preimage_preimage, mul_assoc]

Premises used: Set.preimage_preimage, mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
h : ↥H.op
s : Set G
⊢ Eq (α := Set G) ((fun (y : G) ↦ h • y) '' (fun (x : G) ↦ g * x) ⁻¹' s)
    (preimage (β := G) (fun (x : G) ↦ g * x) ((fun (y : G) ↦ h • y) '' s))

Tactic:
smul_opposite_image_mul_preimage' g h s

Premises used: Subgroup.smul_opposite_image_mul_preimage', Subtype.val
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S_1 : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
inst_2 : Monoid α
inst_3 : MulDistribMulAction α G
S : Subgroup G
⊢ map (((MulDistribMulAction.toMonoidEnd α G : MonoidHom.{u_1, u_2} α (Monoid.End G)) : (a : α) → Monoid.End G) 1) S = S

Tactic:
simpa only [map_one] using S.map_id

Premises used: Subgroup.map_id, map_one
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
a : α
S : Subgroup G
⊢ a • S =
    map (((MulDistribMulAction.toMonoidEnd α G : MonoidHom.{u_1, u_2} α (Monoid.End G)) : (a : α) → Monoid.End G) a) S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
a : α
S : Subgroup G
⊢ (↑(a • S) : Set G) = a • (↑S : Set G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
a : α
S : Subgroup G
⊢ (a • S).toSubmonoid = a • S.toSubmonoid

Tactic:
rfl

Premises used: Submonoid.map, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
m : G
a : α
S : Subgroup G
⊢ m ∈ S → a • m ∈ a • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set G))

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
inst_2 : Monoid α
inst_3 : MulDistribMulAction α G
⊢ CovariantClass α (Subgroup G) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => image_mono⟩

Premises used: CovariantClass.mk, Set.image_mono
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
m : G
a : α
S : Subgroup G
⊢ m ∈ a • S ↔ ∃ s ∈ S, a • s = m

Tactic:
(Set.mem_smul_set : m ∈ a • (S : Set G) ↔ _)

Premises used: Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
a : α
⊢ HSMul.hSMul (β := Subgroup G) a ⊥ = ⊥

Tactic:
map_bot _

Premises used: Subgroup.map_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊔ T) = a • S ⊔ a • T

Tactic:
map_sup _ _ _

Premises used: Subgroup.map_sup, Set.Mem, setOf
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Monoid α
inst_2 : MulDistribMulAction α G
a : α
s : Set G
⊢ HSMul.hSMul (β := Subgroup G) a (closure s) = closure (a • s)

Tactic:
MonoidHom.map_closure _ _

Premises used: MonoidHom.map_closure