mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_2
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ (F' (IsFreeGroup.of ↑⟨e, h⟩)).left (ActionCategory.back ⟨PUnit.unit, b⟩) = f ⟨e, h⟩

Tactic:
hF'

Goal state after:
case refine_2
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ (f' ↑⟨e, h⟩).left (ActionCategory.back ⟨PUnit.unit, b⟩) = f ⟨e, h⟩
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑(S.lowerCentralSeries (n + 1))

Tactic:
by
    rw [lowerCentralSeries_succ]
    apply normalizer_commutator_ge_right

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
← least_ascending_central_series_length_eq_nilpotencyClass

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inl e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
hF'

Goal state after:
case refine_1.cons.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ f' e = 1
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ F'.map (of e) = 1

Tactic:
hF'

Goal state after:
case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ f' e = 1
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • g • a = y

Tactic:
smul_smul,

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹ * g) • a = y
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ (g * k * g⁻¹) • g • a = g • k • a

Tactic:
smul_smul,

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ (g * k * g⁻¹ * g) • a = g • k • a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
⊢ {
          toFun := fun x ↦
            match x with
            | ⟨B, ⋯⟩ => ⟨stabilizer G B, ⋯⟩,
          invFun := fun x ↦
            match x with
            | ⟨H, hH⟩ => ⟨orbit (↥H) a, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨B, ⋯⟩ ≤
      {
          toFun := fun x ↦
            match x with
            | ⟨B, ⋯⟩ => ⟨stabilizer G B, ⋯⟩,
          invFun := fun x ↦
            match x with
            | ⟨H, hH⟩ => ⟨orbit (↥H) a, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨B', ⋯⟩ ↔
    ⟨B, ⋯⟩ ≤ ⟨B', ⋯⟩

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
⊢ ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩ ↔ B ⊆ B'
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
· rw [isConj_iff]
    refine ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective ?_⟩
    simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using! hπ

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x✝ : ↥(fixingSubgroup M s)
x : α
c : M
hc✝ : c ∈ fixingSubgroup M s
hc : c⁻¹ ∈ fixingSubgroup M s
hcx : ⟨c, hc✝⟩ • x ∈ s
⊢ x ∈ s

Tactic:
rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
⊢ Injective ⇑(map_ofFixingSubgroupUnion M s t)

Tactic:
intro a b h
    simpa only [← SetLike.coe_eq_coe] using! h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hkax✝ : ⟨k, hk⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
hkax : g • k • ↑⟨g⁻¹ • a, hg'a⟩ = x
⊢ ↑(⟨g * k * g⁻¹, ?w⟩ • ⟨a, ha'⟩) = x

Tactic:
smul_smul,

Goal state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hkax✝ : ⟨k, hk⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
hkax : (g * k) • ↑⟨g⁻¹ • a, hg'a⟩ = x
⊢ ↑(⟨g * k * g⁻¹, ?w⟩ • ⟨a, ha'⟩) = x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
obtain ⟨g, hg, hg3⟩ := exists_mem_stabilizer_isThreeCycle s h4
  -- By Jordan's theorem, it suffices to prove that G acts primitively
  apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem hG' hg3
  exact hG ⟨hg, IsThreeCycle.mem_alternatingGroup hg3⟩

Goal state after:
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t

Tactic:
intro t ht

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < t.encard
⊢ ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
x✝² x✝¹ : S.Equiv S'
toMulEquiv✝¹ : E ≃* E'
inl_comm✝¹ : ⇑toMulEquiv✝¹ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝¹ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝¹ = ⇑S.rightHom
toMulEquiv✝ : E ≃* E'
inl_comm✝ : ⇑toMulEquiv✝ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝ = ⇑S.rightHom
h :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.toMulEquiv =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.toMulEquiv
x✝ :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.symm =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.symm
⊢ ∀ (x : E), toMulEquiv✝¹ x = toMulEquiv✝ x

Tactic:
exact congrFun h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g • a = a
⊢ toPerm g = toPerm 1

Tactic:
toPerm_one,

Goal state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g • a = a
⊢ toPerm g = 1
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
x✝¹ x✝ : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ (match ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ with
    | ⟨n, g⟩ => S.inl n * s g) =
    (match ⟨n₁, g₁⟩ with
      | ⟨n, g⟩ => S.inl n * s g) *
      match ⟨n₂, g₂⟩ with
      | ⟨n, g⟩ => S.inl n * s g

Tactic:
simp only [conjAct, MonoidHom.comp_apply, map_mul, inl_conjAct_comm, MonoidHom.coe_coe]

Goal state after:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
x✝¹ x✝ : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ S.inl n₁ * (s g₁ * S.inl n₂ * (s g₁)⁻¹) * (s g₁ * s g₂) = S.inl n₁ * s g₁ * (S.inl n₂ * s g₂)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
k : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • k • a = k' • a

Tactic:
smul_smul,

Goal state after:
case h
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
k : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹ * k) • a = k' • a
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
this : ⁅⁅Subgroup.upperCentralSeries G 2, ⊤⁆, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, Subgroup.upperCentralSeries G 2⁆, ⊤⁆ = ⊥

Tactic:
by simpa [commutator_comm]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ ((comap f H).subgroupOf (comap f K)).Normal

Tactic:
normal_subgroupOf_iff_le_normalizer (comap_mono h_le)

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer ↑(comap f H)
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
key : g b ∈ ⊥
⊢ a = 1 ∧ b = 1

Tactic:
exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ unitsSMul φ (-u) (unitsSMul φ u w) = w

Tactic:
by
  rw [unitsSMul]
  split_ifs with hcan
  · set_option backward.isDefEq.respectTransparency false in
    have hncan : ¬ Cancels u w := (unitsSMul_cancels_iff _ _ _).1 hcan
    unfold unitsSMul
    simp only [dif_neg hncan]
    simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul,
      -SetLike.coe_sort_coe]
  · have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan)
    unfold unitsSMul at hcan ⊢
    simp only [dif_pos hcan2] at hcan ⊢
    cases w using consRecOn with
    | ofGroup => simp [Cancels] at hcan2
    | cons g u' w h1 h2 ih =>
      clear ih
      simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]
      cases hcan2.2
      have : ((d.compl (-u)).equiv w.head).1 = 1 :=
        (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1
      simpa [NormalWord.ext_iff, (d.compl (-u)).equiv_mul_left, Units.ext_iff,
        (d.compl (-u)).equiv_snd_eq_inv_mul]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ ∀ ⦃x : List ℕ⦄ (hx : ∀ a ∈ x, a < Fintype.card α) ⦃y : List ℕ⦄ (hy : ∀ a ∈ y, a < Fintype.card α),
    x.Disjoint y → (klift' x hx).Disjoint (klift' y hy)

Tactic:
intro u

Goal state after:
case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
⊢ ∀ (hx : ∀ a ∈ u, a < Fintype.card α) ⦃y : List ℕ⦄ (hy : ∀ a ∈ y, a < Fintype.card α),
    u.Disjoint y → (klift' u hx).Disjoint (klift' y hy)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (↑⟨g.cycleOf x, hx⟩).support

Tactic:
rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
⊢ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))

Tactic:
intro u

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
u : ℤˣ
⊢ u ∈ Option.map Prod.fst w₁.toList.head? → w₁.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : ResiduallyFinite G
g h : G
hgh : g ≠ h
⊢ ∃ H, ↑g ≠ ↑h

Tactic:
obtain ⟨H, hH⟩ :=
    exists_finiteIndexNormalSubgroup_notMem (g⁻¹ * h) fun h ↦ hgh <| eq_of_inv_mul_eq_one h

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : ResiduallyFinite G
g h : G
hgh : g ≠ h
H : FiniteIndexNormalSubgroup G
hH : g⁻¹ * h ∉ H
⊢ ∃ H, ↑g ≠ ↑h
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ ((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp (inl.comp CoprodI.of)) g) = (f i) g

Tactic:
simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe,
    lift_apply_inl, CoprodI.lift_of]

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
⊢ IsMulCommutative ↥N

Tactic:
have := N.bot_or_nontrivial.resolve_left (step0 h1 h3)
  have : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
  exact
    ⟨⟨fun g h => ((eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left
      (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h)).comm g).symm⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'

Tactic:
apply ih _ hG'; rfl

Goal state after: