awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
inl : IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
suffices IsCyclic (P.subgroupOf f.range) by
      have key := Subgroup.subgroupOfEquivOfLe h_le
      exact isCyclic_of_surjective key key.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
inl :
  ∀ (Q : Sylow p G) (hQ : Sylow.mapSurjective ⋯ Q = P.subtype h_le),
    IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
⊢ IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)

Tactic:
obtain ⟨Q, hQ⟩ := Sylow.mapSurjective_surjective f.rangeRestrict_surjective p (P.subtype h_le)

Premises used: Sylow.mapSurjective_surjective, MonoidHom.rangeRestrict_surjective, Sylow.subtype
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
Q : Sylow p G
hQ : Sylow.mapSurjective ⋯ Q = P.subtype h_le
⊢ Subgroup.map f.rangeRestrict (↑Q : Subgroup G) = (↑P : Subgroup G').subgroupOf f.range

Tactic:
rw [Sylow.ext_iff, Sylow.coe_mapSurjective, Sylow.coe_subtype] at hQ

Premises used: Sylow.ext_iff, Sylow.coe_subtype, Sylow.coe_mapSurjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
Q : Sylow p G
hQ : Subgroup.map f.rangeRestrict (↑Q : Subgroup G) = (↑P : Subgroup G').subgroupOf f.range
⊢ IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)

Tactic:
hQ ▸ isCyclic_of_surjective _ (f.rangeRestrict.subgroupMap_surjective Q)

Premises used: Sylow.toSubgroup, isCyclic_of_surjective, MonoidHom.rangeRestrict, Eq.rec, MonoidHom.subgroupMap_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
Q : Sylow p G
hQ : Subgroup.map f.rangeRestrict (↑Q : Subgroup G) = (↑P : Subgroup G').subgroupOf f.range
⊢ IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)

Tactic:
exact hQ ▸ isCyclic_of_surjective _ (f.rangeRestrict.subgroupMap_surjective Q)
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker (↑P : Subgroup G')
⊢ IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))

Tactic:
have := (P.2.map f').isCyclic_of_isZGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker (↑P : Subgroup G')
this : IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))
inr :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := ↥(↑P : Subgroup G')) (β := ↥(Subgroup.map f' (↑P : Subgroup G')))
    (⇑(f'.subgroupMap (↑P : Subgroup G')) : (a : ↥(↑P : Subgroup G')) → ↥(Subgroup.map f' (↑P : Subgroup G')))
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
apply isCyclic_of_injective (f'.subgroupMap P)

Premises used: Sylow.toSubgroup, isCyclic_of_injective, MonoidHom.subgroupMap
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker (↑P : Subgroup G')
this : IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))
inr : Eq (α := Subgroup ↥(↑P : Subgroup G')) (MonoidHom.ker (f'.subgroupMap (↑P : Subgroup G'))) ⊥
inr₁ : Eq (α := Subgroup ↥(↑P : Subgroup G')) (f'.ker.subgroupOf (↑P : Subgroup G')) ⊥
inr₂ inr₃ inr₄ inr₅ : Disjoint f'.ker (↑P : Subgroup G')
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := ↥(↑P : Subgroup G')) (β := ↥(Subgroup.map f' (↑P : Subgroup G')))
    (⇑(f'.subgroupMap (↑P : Subgroup G')) : (a : ↥(↑P : Subgroup G')) → ↥(Subgroup.map f' (↑P : Subgroup G')))

Tactic:
rwa [← MonoidHom.ker_eq_bot_iff, P.ker_subgroupMap f', Subgroup.subgroupOf_eq_bot]

Premises used: Sylow.toSubgroup, Subgroup.subgroupOf_eq_bot, Subgroup.ker_subgroupMap, MonoidHom.ker_eq_bot_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ IsZGroup G ↔
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)

Tactic:
⟨fun hG ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
refine_1 :
  ∀ (hG : IsZGroup G),
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
refine_2 :
  (∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)) →
    IsZGroup G
⊢ IsZGroup G ↔
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)

Tactic:
refine ⟨fun hG ↦ ?_, ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
refine_1 :
  ∀ (H : Subgroup G) (hH : Subgroup.IsComplement' (commutator G) H),
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)

Tactic:
obtain ⟨H, hH⟩ := Subgroup.exists_right_complement'_of_coprime hG.coprime_commutator_index

Premises used: IsZGroup.coprime_commutator_index, Subgroup.exists_right_complement'_of_coprime
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
refine_1 :
  ∀ (h1 : Abelianization G ≃* ↥H),
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)

Tactic:
have h1 : Abelianization G ≃* H := hH.symm.QuotientMulEquiv
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
h1 : Abelianization G ≃* ↥H
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)

Tactic:
⟨commutator G, H, _, (SemidirectProduct.mulEquivSubgroup hH).symm,
      isCyclic_of_surjective _ h1.surjective, hG.isCyclic_commutator, ?_⟩

Premises used: SemidirectProduct.mulEquivSubgroup, isCyclic_of_surjective, MulEquiv.surjective, commutator, And.intro, Exists.intro, IsZGroup.isCyclic_commutator, MulEquiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
h1 : Abelianization G ≃* ↥H
refine_1 : (Nat.card.{u_1} ↥(commutator G)).Coprime (Nat.card.{u_1} ↥H)
⊢ ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)

Tactic:
refine ⟨commutator G, H, _, (SemidirectProduct.mulEquivSubgroup hH).symm,
      isCyclic_of_surjective _ h1.surjective, hG.isCyclic_commutator, ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
h1 : Abelianization G ≃* ↥H
⊢ (Nat.card.{u_1} ↥(commutator G)).Coprime (Nat.card.{u_1} ↥H)

Tactic:
Nat.card_congr h1.toEquiv ▸ hG.coprime_commutator_index

Premises used: IsZGroup.coprime_commutator_index, Eq.rec, MulEquiv.toEquiv, Nat.card_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
hG : IsZGroup G
H : Subgroup G
hH : Subgroup.IsComplement' (commutator G) H
h1 : Abelianization G ≃* ↥H
⊢ (Nat.card.{u_1} ↥(commutator G)).Coprime (Nat.card.{u_1} ↥H)

Tactic:
exact Nat.card_congr h1.toEquiv ▸ hG.coprime_commutator_index
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic.{u_1} ↥H
hN : IsCyclic.{u_1} ↥N
hHN : (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
⊢ IsZGroup.{u_1} (↥N ⋊[φ] ↥H)

Tactic:
have : IsZGroup (N ⋊[φ] H) :=
      isZGroup_of_coprime SemidirectProduct.range_inl_eq_ker_rightHom.ge hHN
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic.{u_1} ↥H
hN : IsCyclic.{u_1} ↥N
hHN : (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
this : IsZGroup.{u_1} (↥N ⋊[φ] ↥H)
⊢ IsZGroup G

Tactic:
IsZGroup.of_injective (f := e.toMonoidHom) e.injective

Premises used: MulEquiv.injective, IsZGroup.of_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic.{u_1} ↥H
hN : IsCyclic.{u_1} ↥N
hHN : (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
this : IsZGroup.{u_1} (↥N ⋊[φ] ↥H)
⊢ IsZGroup G

Tactic:
exact IsZGroup.of_injective (f := e.toMonoidHom) e.injective

Premises used: MulEquiv.injective, IsZGroup.of_injective
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
⊢ (↑(center G) : Set G) = Set.center G

Tactic:
rfl

Premises used: setOf, Set.center, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Submonoid G) (toSubmonoid (center G)) (Submonoid.center G)

Tactic:
rfl

Premises used: Submonoid.center, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
⊢ IsMulCommutative.{u_1} ↥(center G)

Tactic:
⟨⟨fun a b => Subtype.ext (b.2.comm a).symm⟩⟩

Premises used: IsMulCentral.comm, Commute.symm, IsMulCommutative.mk, Std.Commutative.mk, Subtype.val, Subtype.property, Subtype.ext
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
z : G
rw : Membership.mem (γ := Subgroup G) (center G) z ↔ z ∈ Set.center G
⊢ Membership.mem (γ := Subgroup G) (center G) z ↔ ∀ (g : G), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
z : G
⊢ Membership.mem (γ := Subgroup G) (center G) z ↔ z ∈ Set.center G

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.center
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
z : G
⊢ Membership.mem (γ := Subgroup G) (center G) z ↔ z ∈ Set.center G

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
⊢ Characteristic (center G)

Tactic:
characteristic_iff_comap_le.mpr fun ϕ g hg => ?_

Premises used: Iff.mpr, Subgroup.characteristic_iff_comap_le
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
refine : ∀ (ϕ : G ≃* G) (g : G) (hg : g ∈ comap ϕ.toMonoidHom (center G)), Membership.mem (γ := Subgroup G) (center G) g
⊢ Characteristic (center G)

Tactic:
refine characteristic_iff_comap_le.mpr fun ϕ g hg => ?_

Premises used: Iff.mpr, Subgroup.characteristic_iff_comap_le
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
rw : ∀ (g_1 : G), g_1 * g = g * g_1
⊢ Membership.mem (γ := Subgroup G) (center G) g

Tactic:
rw [mem_center_iff]

Premises used: Subgroup.mem_center_iff
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : 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)
⊢ h * g = g * h

Tactic:
rw [← ϕ.injective.eq_iff, map_mul, map_mul]

Premises used: Function.Injective.eq_iff, map_mul, MulEquiv.injective
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : 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.comm (ϕ h)).symm

Premises used: SemiconjBy, Commute, IsMulCentral.comm, Commute.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : 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.comm (ϕ h)).symm

Premises used: IsMulCentral.comm, Commute.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : CommGroup G
rw : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
⊢ Eq (α := Subgroup G) (center G) ⊤

Tactic:
rw [eq_top_iff']

Premises used: Subgroup.eq_top_iff'
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : CommGroup G
x : G
rw : ∀ (g : G), g * x = x * g
⊢ Membership.mem (γ := Subgroup G) (center G) x

Tactic:
rw [Subgroup.mem_center_iff]

Premises used: Subgroup.mem_center_iff
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : CommGroup G
x y : G
⊢ y * x = x * y

Tactic:
mul_comm y x

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : CommGroup G
x y : G
⊢ y * x = x * y

Tactic:
exact mul_comm y x

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (center G) ⊤ ↔ IsMulCommutative G

Tactic:
simp [eq_top_iff', isMulCommutative_iff, mem_center_iff, eq_comm]

Premises used: Subgroup.mem_center_iff, eq_comm, Subgroup.eq_top_iff', isMulCommutative_iff
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
hG : IsMulCommutative G
⊢ Eq (α := Subgroup G) (center G) ⊤

Tactic:
center_eq_top_iff.mpr hG

Premises used: Iff.mpr, Subgroup.center_eq_top_iff
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
h : Eq (α := Subgroup G) (center G) ⊤
⊢ ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x

Tactic:
rw [eq_top_iff'] at h

Premises used: Subgroup.eq_top_iff'
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
__src : Group G := inst
x y : G
apply : Membership.mem (γ := Subgroup G) (center G) y
⊢ x * y = y * x

Tactic:
apply Subgroup.mem_center_iff.mp _ x

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
__src : Group G := inst
x y : G
⊢ Membership.mem (γ := Subgroup G) (center G) y

Tactic:
h y

Premises used: Set.Mem
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (center G) x
__src : Group G := inst
x y : G
⊢ Membership.mem (γ := Subgroup G) (center G) y

Tactic:
exact h y
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : Membership.mem (γ := Subgroup G) (center G) a
b : G
⊢ Membership.mem (γ := Subgroup G) (center G) (b * a * b⁻¹)

Tactic:
simpa [mem_center_iff.mp ha b]

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
hx : Membership.mem (γ := Subgroup G) (center G) x
y : G
⊢ y ∈ s ↔ x * y * x⁻¹ ∈ s

Tactic:
simp [← mem_center_iff.mp hx y]

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
M : Type u_2
inst : Monoid M
g h : M
H : IsConj g h
Hg : g ∈ Set.center M
rcases : ∀ (u : Mˣ) (hu : SemiconjBy (↑u : M) g h), g = h
⊢ g = h

Tactic:
rcases H with ⟨u, hu⟩
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
M : Type u_2
inst : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u : M) g h
rwa : g * (↑u : M) = h * (↑u : M)
rwa₁ rwa₂ rwa₃ rwa₄ : (↑u : M) * g = h * (↑u : M)
⊢ g = h

Tactic:
rwa [← u.mul_left_inj, Hg.comm u]

Premises used: Units.val, IsMulCentral.comm, Units.mul_left_inj
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
M : Type u_2
inst : Monoid M
g h : M
H : IsConj g h
Hh : h ∈ Set.center M
⊢ g = h

Tactic:
(H.symm.eq_of_left_mem_center Hh).symm

Premises used: IsConj.symm, IsConj.eq_of_left_mem_center, Eq.symm
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
⊢ Set.BijOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ

Tactic:
⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩

Premises used: And.intro, Set.BijOn
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
refine_1 :
  ∀ (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G)),
    Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (ConjClasses.mk g)
refine_2 :
  ∀ (x : G) (hx : x ∈ (↑(Subgroup.center G) : Set G)),
    ∀ y ∈ (↑(Subgroup.center G) : Set G), ∀ (H : Eq (α := ConjClasses G) (ConjClasses.mk x) (ConjClasses.mk y)), x = y
refine_3 : Set.SurjOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ
⊢ Set.BijOn (β := ConjClasses G) ConjClasses.mk (↑(Subgroup.center G) : Set G) (noncenter G)ᶜ

Tactic:
refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
refine_1 : (carrier (ConjClasses.mk g)).Subsingleton
⊢ Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (ConjClasses.mk g)

Tactic:
simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff]

Premises used: Set.compl_def, Set.mem_setOf, ConjClasses.mem_noncenter, Set.not_nontrivial_iff
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x : G
hx : x ∈ carrier (ConjClasses.mk g)
y : G
hy : y ∈ carrier (ConjClasses.mk g)
⊢ IsConj x g

Tactic:
simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy

Premises used: ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x : G
hx : x ∈ carrier (ConjClasses.mk g)
y : G
hy : y ∈ carrier (ConjClasses.mk g)
hx₁ : IsConj x g
⊢ IsConj y g

Tactic:
simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy

Premises used: ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G)
x y : G
hx : IsConj x g
hy : IsConj y g
refine_1 : g = y
refine_1₁ refine_1₂ : g = g
⊢ x = y

Tactic:
rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]

Premises used: IsConj.eq_of_right_mem_center
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
x : G
hx : x ∈ (↑(Subgroup.center G) : Set G)
y : G
h : y ∈ (↑(Subgroup.center G) : Set G)
H : Eq (α := ConjClasses G) (ConjClasses.mk x) (ConjClasses.mk y)
⊢ IsConj x y

Tactic:
rw [mk_eq_mk_iff_isConj] at H

Premises used: ConjClasses.mk_eq_mk_iff_isConj
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
x : G
hx : x ∈ (↑(Subgroup.center G) : Set G)
y : G
h : y ∈ (↑(Subgroup.center G) : Set G)
H : IsConj x y
⊢ x = y

Tactic:
H.eq_of_left_mem_center hx

Premises used: IsConj.eq_of_left_mem_center
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
x : G
hx : x ∈ (↑(Subgroup.center G) : Set G)
y : G
h : y ∈ (↑(Subgroup.center G) : Set G)
H : IsConj x y
⊢ x = y

Tactic:
exact H.eq_of_left_mem_center hx

Premises used: IsConj.eq_of_left_mem_center
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ Membership.mem (γ := Set (ConjClasses G)) (ConjClasses.mk '' (↑(Subgroup.center G) : Set G))
    (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)

Tactic:
⟨g, ?_, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
refine_3 : g ∈ (↑(Subgroup.center G) : Set G)
⊢ Membership.mem (γ := Set (ConjClasses G)) (ConjClasses.mk '' (↑(Subgroup.center G) : Set G))
    (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)

Tactic:
refine ⟨g, ?_, rfl⟩
-- Module: Mathlib.GroupTheory.Subgroup.Center
Goal:
G : Type u_2
inst : Group G
a : ConjClasses G
g : G
hg : Membership.mem (γ := Set (ConjClasses G)) (noncenter G)ᶜ (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)
⊢ (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton

Tactic:
simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff] at hg

Premises used: Set.compl_def, Set.mem_setOf, ConjClasses.mem_noncenter, Set.not_nontrivial_iff