awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
refine_3 : ∀ (g_1 : G), g_1 * g = g * g_1
⊢ g ∈ (↑(Subgroup.center G) : Set G)

Tactic:
rw [SetLike.mem_coe, Subgroup.mem_center_iff]

Premises used: Subgroup.mem_center_iff, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
refine_3 : h * g * h⁻¹ = g
⊢ h * g = g * h

Tactic:
rw [← mul_inv_eq_iff_eq_mul]

Premises used: mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ = g

Tactic:
hg ?_ mem_carrier_mk

Premises used: ConjClasses.mem_carrier_mk
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
refine_3 : h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ h * g * h⁻¹ = g

Tactic:
refine hg ?_ mem_carrier_mk

Premises used: ConjClasses.mem_carrier_mk
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
refine_3 : Eq (α := ConjClasses G) (ConjClasses.mk (h * g * h⁻¹)) (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)

Tactic:
rw [mem_carrier_iff_mk_eq]

Premises used: ConjClasses.mem_carrier_iff_mk_eq
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
refine_3 : IsConj (h * g * h⁻¹) g
⊢ Eq (α := ConjClasses G) (ConjClasses.mk (h * g * h⁻¹)) (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)

Tactic:
apply mk_eq_mk_iff_isConj.mpr

Premises used: Iff.mpr, ConjClasses.mk_eq_mk_iff_isConj
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
refine_3 : ∃ (c : G), c * g * c⁻¹ = h * g * h⁻¹
⊢ IsConj (h * g * h⁻¹) g

Tactic:
rw [isConj_comm, isConj_iff]

Premises used: isConj_iff, isConj_comm
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ ∃ (c : G), c * g * c⁻¹ = h * g * h⁻¹

Tactic:
⟨h, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton
h : G
⊢ ∃ (c : G), c * g * c⁻¹ = h * g * h⁻¹

Tactic:
exact ⟨h, rfl⟩
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
⊢ Membership.mem (γ := Subgroup G) (centralizer s) g ↔ ∀ h ∈ s, h * g = g * h

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
⊢ Membership.mem (γ := Subgroup G) (centralizer s) g ↔ ∀ h ∈ s, ⁅h, g⁆ = 1

Tactic:
simp only [commutatorElement_def, mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]

Premises used: commutatorElement_def, Subgroup.mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
⊢ Membership.mem (γ := Subgroup G) (centralizer s) g ↔ ∀ h ∈ s, ⁅g, h⁆ = 1

Tactic:
forall₂_congr fun _ _ ↦ ?_

Premises used: Set.Mem, setOf, Set.centralizer, forall₂_congr
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
refine : ∀ x ∈ s, x * g = g * x ↔ ⁅g, x⁆ = 1
⊢ Membership.mem (γ := Subgroup G) (centralizer s) g ↔ ∀ h ∈ s, ⁅g, h⁆ = 1

Tactic:
refine forall₂_congr fun _ _ ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
s : Set G
x : G
h : x ∈ s
rw : x * g = g * x ↔ g * x * g⁻¹ * x⁻¹ = 1
rw₁ : x * g = g * x ↔ g * x * g⁻¹ = 1 * x
rw₂ : x * g = g * x ↔ g * x = 1 * x * g
rw₃ : x * g = g * x ↔ g * x = x * g
rw₄ rw₅ : g * x = x * g ↔ g * x = x * g
⊢ x * g = g * x ↔ ⁅g, x⁆ = 1

Tactic:
rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]

Premises used: commutatorElement_def, eq_comm, mul_inv_eq_iff_eq_mul, one_mul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g k : G
simp : g * k = k * g ↔ k * g = g * k
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) k ↔ k * g = g * k

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]

Premises used: Subgroup.mem_centralizer_iff, forall_eq, Set.mem_singleton_iff
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g k : G
⊢ g * k = k * g ↔ k * g = g * k

Tactic:
eq_comm

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g k : G
⊢ g * k = k * g ↔ k * g = g * k

Tactic:
exact eq_comm

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (centralizer Set.univ) (center G)

Tactic:
SetLike.ext' (Set.centralizer_univ G)

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ centralizer (↑K : Set G) ↔ K ≤ centralizer (↑H : Set G)

Tactic:
⟨fun h x hx _y hy => (h hy x hx).symm, fun h x hx _y hy => (h hy x hx).symm⟩

Premises used: Iff.intro, Eq.symm
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ LE.le (α := Subgroup G) (center G) (centralizer s)

Tactic:
Set.center_subset_centralizer s

Premises used: Set.Mem, setOf, Set.center, Set.centralizer, Set.Subset, Set.center_subset_centralizer
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s t : Set G
h : s ⊆ t
⊢ LE.le (α := Subgroup G) (centralizer t) (centralizer s)

Tactic:
Submonoid.centralizer_le h

Premises used: Set.Mem, Submonoid.centralizer_le
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (centralizer s) ⊤ ↔ s ⊆ (↑(center G) : Set G)

Tactic:
SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Premises used: Set.centralizer_eq_top_iff_subset, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ (↑(centralizer s) : Set G)
h : G
hh : h ∈ s
rw : (f : (a : G) → G') (h * g) = HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')
rw₁ : Eq.{u_2 + 1} (α := G') ((f : (a : G) → G') (h * g) : G') ((f : (a : G) → G') (g * h) : G')
rw₂ rw₃ : Eq.{u_2 + 1} (α := G') ((f : (a : G) → G') (g * h) : G') ((f : (a : G) → G') (g * h) : G')
⊢ HMul.hMul (α := G') (β := G') ((f : (a : G) → G') h : G') ((f : (a : G) → G') g : G') =
    HMul.hMul (α := G') (β := G') ((f : (a : G) → G') g : G') ((f : (a : G) → G') h : G')

Tactic:
rw [← map_mul, ← map_mul, hg h hh]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
inst_2 : H.Normal
g : G
hg : Membership.mem (γ := Subgroup G) (centralizer (↑H : Set G)) g
i h : G
hh : h ∈ (↑H : Set G)
⊢ h * (i * g * i⁻¹) = i * g * i⁻¹ * h

Tactic:
simpa [-mul_left_inj, -mul_right_inj, mul_assoc]
      using congr(i * $(hg _ <| ‹H.Normal›.conj_mem _ hh i⁻¹) * i⁻¹)

Premises used: mul_assoc, mul_left_inj, mul_right_inj, Inv.inv, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
⊢ Characteristic (centralizer (↑H : Set G))

Tactic:
Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_

Premises used: Iff.mpr, Subgroup.characteristic_iff_comap_le, MulEquiv.injective
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
refine :
  ∀ (ϕ : G ≃* G) (g : G) (hg : g ∈ comap ϕ.toMonoidHom (centralizer (↑H : Set G))) (h : G) (hh : h ∈ (↑H : Set G)),
    Eq (α := G) ((ϕ : (a : G) → G) (h * g) : G) ((ϕ : (a : G) → G) (g * h) : G)
⊢ Characteristic (centralizer (↑H : Set G))

Tactic:
refine Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer (↑H : Set G))
h : G
hh : h ∈ (↑H : Set G)
rw :
  HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) h : G) ((ϕ : (a : G) → G) g : G) =
    HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) g : G) ((ϕ : (a : G) → G) h : G)
⊢ Eq (α := G) ((ϕ : (a : G) → G) (h * g) : G) ((ϕ : (a : G) → G) (g * h) : G)

Tactic:
rw [map_mul, map_mul]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer (↑H : Set G))
h : G
hh : h ∈ (↑H : Set G)
⊢ HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) h : G) ((ϕ : (a : G) → G) g : G) =
    HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) g : G) ((ϕ : (a : G) → G) h : G)

Tactic:
hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)

Premises used: Subgroup.characteristic_iff_le_comap, Iff.mp, DFunLike.coe
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer (↑H : Set G))
h : G
hh : h ∈ (↑H : Set G)
⊢ HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) h : G) ((ϕ : (a : G) → G) g : G) =
    HMul.hMul (α := G) (β := G) ((ϕ : (a : G) → G) g : G) ((ϕ : (a : G) → G) h : G)

Tactic:
exact hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)

Premises used: Subgroup.characteristic_iff_le_comap, Iff.mp, DFunLike.coe
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
⊢ K ≤ centralizer (↑K : Set G) ↔ IsMulCommutative.{u_1} ↥K

Tactic:
⟨fun h ↦ ⟨⟨fun x y ↦ Subtype.ext <| h y.2 x x.2⟩⟩,
    fun _ x hx y hy ↦ congrArg Subtype.val <| mul_comm' ⟨y, hy⟩ ⟨x, hx⟩⟩

Premises used: Iff.intro, IsMulCommutative.mk, Std.Commutative.mk, Subtype.val, Subtype.property, Subtype.ext
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : IsMulCommutative.{u_1} ↥H
⊢ H ≤ centralizer (↑H : Set G)

Tactic:
le_centralizer_iff_isMulCommutative.mpr h

Premises used: Iff.mpr, Subgroup.le_centralizer_iff_isMulCommutative
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ LE.le (α := Subgroup G) (closure s) (centralizer (↑(centralizer s) : Set G))

Tactic:
closure_le _ |>.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Subgroup.closure_le, Set.subset_centralizer_centralizer
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (centralizer (↑(closure s) : Set G)) (centralizer s)

Tactic:
le_antisymm (centralizer_le subset_closure)
    (le_centralizer_iff.mp (closure_le_centralizer_centralizer s))

Premises used: Subgroup.le_centralizer_iff, Subgroup.closure_le_centralizer_centralizer, Subgroup.subset_closure, le_antisymm, Subgroup.centralizer_le, Iff.mp
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
hx : Membership.mem (γ := Subgroup G) (⨅ g ∈ s, centralizer {g}) x
⊢ Membership.mem (γ := Subgroup G) (centralizer s) x

Tactic:
simpa only [mem_iInf, mem_centralizer_singleton_iff, eq_comm (a := x * _)] using hx

Premises used: Subgroup.mem_iInf, eq_comm, Subgroup.mem_centralizer_singleton_iff
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (centralizer Set.univ) (⨅ g ∈ s, centralizer {g})
rw₁ : Eq (α := Subgroup G) (centralizer (↑⊤ : Set G)) (⨅ g ∈ s, centralizer {g})
rw₂ : Eq (α := Subgroup G) (centralizer (↑(closure s) : Set G)) (⨅ g ∈ s, centralizer {g})
rw₃ : Eq (α := Subgroup G) (centralizer s) (⨅ g ∈ s, centralizer {g})
rw₄ rw₅ : Eq.{u_1 + 1} (α := Subgroup G) (⨅ g ∈ s, centralizer {g}) (⨅ g ∈ s, centralizer {g})
⊢ Eq (α := Subgroup G) (center G) (⨅ g ∈ s, centralizer {g})

Tactic:
rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]

Premises used: Subgroup.centralizer_univ, Subgroup.centralizer_closure, Subgroup.coe_top, Subgroup.centralizer_eq_iInf
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
rw : Eq.{u_1 + 1} (α := Subgroup G) (⨅ g ∈ s, centralizer {g}) (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Subgroup G) (⨅ (i : (↑s : Type u_1)), centralizer {(↑i : G)})
    (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})
⊢ Eq (α := Subgroup G) (center G) (⨅ (g : (↑s : Type u_1)), centralizer {(↑g : G)})

Tactic:
rw [center_eq_iInf hs, ← iInf_subtype'']

Premises used: iInf_subtype'', Subgroup.center_eq_iInf
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
k : Set G
hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x
⊢ IsMulCommutative.{u_1} ↥(closure k)

Tactic:
have := closure_le_centralizer_centralizer k
  .of_setLike_mul_comm fun _ h₁ _ h₂ ↦
    Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂)

Premises used: Set.Mem, IsMulCommutative.of_setLike_mul_comm, Subgroup.closure_le_centralizer_centralizer, Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
S : Type u_3
inst_2 : SetLike S G
inst_3 : MulMemClass S G
s : S
inst_4 : IsMulCommutative.{u_1} ↥s
⊢ IsMulCommutative.{u_1} ↥(closure (↑s : Set G))

Tactic:
isMulCommutative_closure fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂

Premises used: setLike_mul_comm, Subgroup.isMulCommutative_closure
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ LE.le (α := Subgroup G) (centralizer s) (normalizer s)

Tactic:
fun g hg h ↦ ⟨fun hh ↦ ?_, fun hh ↦ ?_⟩

Premises used: Set.Mem, setOf, Iff.intro
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
refine_1 : ∀ (g : G) (hg : Membership.mem (γ := Subgroup G) (centralizer s) g) (h : G) (hh : h ∈ s), g * h * g⁻¹ ∈ s
refine_2 : ∀ (g : G) (hg : Membership.mem (γ := Subgroup G) (centralizer s) g) (h : G) (hh : g * h * g⁻¹ ∈ s), h ∈ s
⊢ LE.le (α := Subgroup G) (centralizer s) (normalizer s)

Tactic:
refine fun g hg h ↦ ⟨fun hh ↦ ?_, fun hh ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (centralizer s) g
h : G
hh : h ∈ s
⊢ g * h * g⁻¹ ∈ s

Tactic:
simpa [← hg h hh]
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (centralizer s) g
h : G
hh : g * h * g⁻¹ ∈ s
⊢ g * h * g⁻¹ ∈ s

Tactic:
hh
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (centralizer s) g
h : G
hh : g * h * g⁻¹ ∈ s
h₁ : h = g * h * g⁻¹
⊢ h ∈ s

Tactic:
convert! hh
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (centralizer s) g
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h = g * h * g⁻¹

Tactic:
simpa using hg _ hh
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
⊢ Normal (G := ↥(normalizer s)) (subgroupOf (centralizer s) (normalizer s))

Tactic:
(Subgroup.normal_subgroupOf_iff <| centralizer_le_normalizer s).mpr fun c n hc hn ↦ ?_

Premises used: Iff.mpr, Subgroup.normal_subgroupOf_iff, Subgroup.centralizer_le_normalizer
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
refine :
  ∀ (c n : G) (hc : Membership.mem (γ := Subgroup G) (centralizer s) c)
    (hn : Membership.mem (γ := Subgroup G) (normalizer s) n),
    Membership.mem (γ := Subgroup G) (centralizer s) (n * c * n⁻¹)
⊢ Normal (G := ↥(normalizer s)) (subgroupOf (centralizer s) (normalizer s))

Tactic:
refine (Subgroup.normal_subgroupOf_iff <| centralizer_le_normalizer s).mpr fun c n hc hn ↦ ?_

Premises used: Iff.mpr, Subgroup.normal_subgroupOf_iff, Subgroup.centralizer_le_normalizer
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : Membership.mem (γ := Subgroup G) (centralizer s) c
hn : Membership.mem (γ := Subgroup G) (normalizer s) n
⊢ Membership.mem (γ := Subgroup G) (centralizer s) (n * c * n⁻¹)

Tactic:
mem_centralizer_iff_commutator_eq_one'.mpr fun g hg ↦ ?_

Premises used: Iff.mpr, Subgroup.mem_centralizer_iff_commutator_eq_one'
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : Membership.mem (γ := Subgroup G) (centralizer s) c
hn : Membership.mem (γ := Subgroup G) (normalizer s) n
refine : ∀ (g : G) (hg : g ∈ s), ⁅n * c * n⁻¹, g⁆ = 1
⊢ Membership.mem (γ := Subgroup G) (centralizer s) (n * c * n⁻¹)

Tactic:
refine mem_centralizer_iff_commutator_eq_one'.mpr fun g hg ↦ ?_

Premises used: Iff.mpr, Subgroup.mem_centralizer_iff_commutator_eq_one'
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : Membership.mem (γ := Subgroup G) (centralizer s) c
hn : Membership.mem (γ := Subgroup G) (normalizer s) n
g : G
hg : g ∈ s
this : n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1
⊢ ⁅n * c * n⁻¹, g⁆ = 1

Tactic:
simpa [commutatorElement_def, mul_assoc]

Premises used: commutatorElement_def, mul_assoc
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : Membership.mem (γ := Subgroup G) (centralizer s) c
hn : Membership.mem (γ := Subgroup G) (normalizer s) n
g : G
hg : g ∈ s
suffices : n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1
⊢ ⁅n * c * n⁻¹, g⁆ = 1

Tactic:
suffices n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1 by simpa [commutatorElement_def, mul_assoc]
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : Membership.mem (γ := Subgroup G) (centralizer s) c
hn : Membership.mem (γ := Subgroup G) (normalizer s) n
g : G
hg : g ∈ s
⊢ n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1

Tactic:
simp [← hc _ <| mem_set_normalizer_iff''.mp hn g |>.mp hg]

Premises used: Subgroup.mem_set_normalizer_iff'', Iff.mp
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Eq (α := Subgroup G) (normalizer {g}) (centralizer {g})

Tactic:
ext fun h ↦ ⟨?_, ?_⟩

Premises used: Iff.intro, Subgroup.ext
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g : G
refine_1 :
  ∀ (h : G), Membership.mem (γ := Subgroup G) (normalizer {g}) h → Membership.mem (γ := Subgroup G) (centralizer {g}) h
refine_2 :
  ∀ (h : G), Membership.mem (γ := Subgroup G) (centralizer {g}) h → Membership.mem (γ := Subgroup G) (normalizer {g}) h
⊢ Eq (α := Subgroup G) (normalizer {g}) (centralizer {g})

Tactic:
refine ext fun h ↦ ⟨?_, ?_⟩

Premises used: Iff.intro, Subgroup.ext
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
h g : G
hh : Membership.mem (γ := Subgroup G) (normalizer {g}) h
⊢ g * h = h * g

Tactic:
mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm

Premises used: mul_eq_of_eq_mul_inv, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
h g : G
hh : Membership.mem (γ := Subgroup G) (normalizer {g}) h
⊢ g * h = h * g

Tactic:
exact mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm

Premises used: mul_eq_of_eq_mul_inv, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g h : G
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) h → Membership.mem (γ := Subgroup G) (normalizer {g}) h

Tactic:
fun hh g ↦ ⟨?_, ?_⟩

Premises used: Set.Mem, setOf, Iff.intro
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
g h : G
refine_2 :
  ∀ (hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h) (g_1 : G),
    Membership.mem (γ := Set G) {g} g_1 → Membership.mem (γ := Set G) {g} (h * g_1 * h⁻¹)
refine_2₁ :
  ∀ (hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h) (g_1 : G),
    Membership.mem (γ := Set G) {g} (h * g_1 * h⁻¹) → Membership.mem (γ := Set G) {g} g_1
⊢ Membership.mem (γ := Subgroup G) (centralizer {g}) h → Membership.mem (γ := Subgroup G) (normalizer {g}) h

Tactic:
refine fun hh g ↦ ⟨?_, ?_⟩
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
h g : G
hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h
⊢ Membership.mem (γ := Set G) {g} (h * g * h⁻¹)

Tactic:
(eq_mul_inv_of_mul_eq <| hh g rfl).symm

Premises used: eq_mul_inv_of_mul_eq, Set.Mem, setOf, Set.singleton, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
h g : G
hh : Membership.mem (γ := Subgroup G) (centralizer {g}) h
⊢ Membership.mem (γ := Set G) {g} (h * g * h⁻¹)

Tactic:
exact (eq_mul_inv_of_mul_eq <| hh g rfl).symm

Premises used: eq_mul_inv_of_mul_eq, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
inst : Group G
h g : G
hh : Membership.mem (γ := Subgroup G) (centralizer {h * g * h⁻¹}) h
⊢ Membership.mem (γ := Set G) {h * g * h⁻¹} g

Tactic:
simpa using hh _ rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
⊢ ∀ (x y : ↥(normalizer (↑H : Set G))) (b : ↥H), (x * y) • b = x • y • b

Tactic:
simp [HSMul.hSMul, mul_assoc]

Premises used: mul_assoc, HSMul.hSMul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
g : ↥H
⊢ HSMul.hSMul (α := ↥(normalizer (↑H : Set G))) 1 g = g

Tactic:
simp [HSMul.hSMul]

Premises used: HSMul.hSMul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer (↑H : Set G))), HSMul.hSMul (β := ↥H) r 1 = 1

Tactic:
simp [HSMul.hSMul]

Premises used: HSMul.hSMul
-- Module: Mathlib.GroupTheory.Subgroup.Centralizer
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer (↑H : Set G))) (x y : ↥H), r • (x * y) = r • x * r • y

Tactic:
simp [HSMul.hSMul]

Premises used: HSMul.hSMul