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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ S.lowerCentralSeries (n + 1) = ⊥

Tactic:
rw [lowerCentralSeries_succ, commutator_def, closure_eq_bot_iff, Set.subset_singleton_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ ∀ y ∈ {g | ∃ g₁ ∈ S.lowerCentralSeries n, ∃ g₂ ∈ S, ⁅g₁, g₂⁆ = g}, y = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
by
  classical
  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
⊢ commutator M ≤ N

Tactic:
have ntα : Nontrivial α := nontrivial_of_fixedPoints_ne_univ hNX

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
rw [hG0, minFac_zero] at hHp
    exact normal_of_index_eq_two hHp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : ¬a = b
⊢ ∃ g, g • a = b

Tactic:
· rw [is_two_pretransitive_iff] at h2
      obtain ⟨g, h, _⟩ := h2 h (Ne.symm h)
      exact ⟨g, h⟩

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ (swap x y ∈ G ↔ g ∈ alternatingGroup α) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)

Tactic:
refine iff_congr (iff_of_false ?_ (by cases (sign_swap hxy).symm.trans ·)) Iff.rfl

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ swap x y ∉ G
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
k : ℕ
Hk : IsMultiplyPretransitive G α k
s : Set α
hs : s.ncard = k
⊢ (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!

Tactic:
by
  induction k generalizing G α with
  | zero =>
    rw [Set.ncard_eq_zero] at hs
    simp [hs]
  | succ k hrec =>
    have hGX : IsPretransitive G α := by
      rw [← is_one_pretransitive_iff]
      apply isMultiplyPretransitive_of_le (n := k + 1)
      · rw [Nat.succ_le_succ_iff]; apply Nat.zero_le
      · rw [← hs, ← Set.ncard_univ]
        exact ncard_le_ncard s.subset_univ finite_univ
    have : s.Nonempty := by
      rw [← Set.ncard_pos, hs]
      exact succ_pos k
    obtain ⟨a, has⟩ := this
    let t : Set (SubMulAction.ofStabilizer G a) := Subtype.val ⁻¹' s
    have hat : Subtype.val '' t = s \ {a} := by
      rw [Set.image_preimage_eq_inter_range]
      simp only [Subtype.range_coe_subtype]
      rw [Set.sdiff_eq_compl_inter, Set.inter_comm]
      congr
    have hat' : s = insert a (Subtype.val '' t) := by
      rw [hat, Set.insert_sdiff_singleton, Set.insert_eq_of_mem has]
    have hfs := SubMulAction.fixingSubgroup_of_insert a t
    rw [← hat'] at hfs
    rw [hfs, Subgroup.index_map,
      MonoidHom.ker_eq_bot (stabilizer G a).subtype
        (by simp only [Subgroup.coe_subtype, Subtype.coe_injective])]
    simp only [sup_bot_eq, Subgroup.range_subtype]
    have htcard : t.ncard = k := by
      rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]
      suffices ¬ a ∈ (Subtype.val '' t) by
        convert! Set.ncard_insert_of_notMem this ?_
        · rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
        apply Set.toFinite
      intro h
      obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
      apply hb
      simp only [← hb', Set.mem_singleton_iff]
    suffices (fixingSubgroup (stabilizer G a) t).index *
      (Nat.card α - 1 - k).factorial =
        (Nat.card α - 1).factorial by
      rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm,
        index_stabilizer_of_transitive G a]
      exact Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)
    convert! hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard
    all_goals { rw [nat_card_ofStabilizer_eq G a] }

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := ⋯
ht : t.Finite
⊢ a ∈ t

Tactic:
exact ⟨ha, hga⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard - 1 + 1 ≤ n

Tactic:
← htm,

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard ≤ n
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩,
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ s.encard + 1 = ↑n

Tactic:
rw [← ht, ← hs', hf.injective.encard_image]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard - 1 + 1 ≤ n

Tactic:
← htm,

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard ≤ n
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
⊢ Perm.ofSubtype g • s = s

Tactic:
ofSubtype_mem_stabilizer

Goal state after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
⊢ s = s
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
⊢ IsMultiplyPretransitive K α 2

Tactic:
let φ := MulAction.toPermHom K α

Goal state after:
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
⊢ IsMultiplyPretransitive K α 2
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.Section
g₁ g₂ : G
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

Tactic:
obtain ⟨n, hn⟩ := mul_mul_mul_inv_mem_range_inl σ g₁ g₂

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.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂
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 α
s : Finset α
hs : s ∈ powersetCard α n
⊢ Fintype.card ?m.29 = #?m.32

Tactic:
rw [hs, Fintype.card_fin]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 1 = Subgroup.upperCentralSeries G n

Tactic:
apply Subgroup.upperCentralSeries.eq_ge_of_eq_succ <| by lia

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 1 = Subgroup.upperCentralSeries G (1 + 1)
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * f ↑(∏ i, (x (n i)).2) = f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)

Tactic:
rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
· rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN
      exact ⟨H, hN, le_rfl, ne_top.lt_top⟩

Goal state after:
case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
hbc : mk b.1 b.2 ≤ mk c.1 c.2
⊢ mk a.1 a.2 ≤ mk c.1 c.2

Tactic:
simp only [mk_le_mk] at hab hbc ⊢
      apply le_of_mul_le_mul_left' _
      · exact ↑b.2
      grw [mul_left_comm, hab]
      rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case zero
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
hm : Irreducible (f 0)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ 0 = u * m'

Tactic:
exact (hm.ne_zero f.map_zero).elim

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
a✝ : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
⊢ Cancels u' w

Tactic:
simp only [Cancels, cons_head, cons_toList, List.head?_cons,
        Option.map_some, Option.some.injEq] at h

Goal state after:
case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
a✝ : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h✝ : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
h : g ∈ toSubgroup A B u ∧ u' = -u
⊢ Cancels u' w
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
i : ι
a : { x // f x = i }
⊢ ↑(((fun g i ↦ (mk.symm ↑(MulOpposite.unop g)).subtypePerm ⋯)
          ((fun g ↦ { unop' := ⟨mk (stabilizerEquiv_invFun_aux g), ⋯⟩ }) g) i)
        a) =
    ↑((g i) a)

Tactic:
apply stabilizerEquiv_invFun_eq

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
⊢ {g | f ∘ ⇑g = f}.ncard = ∏ i, {a | f a = i}.ncard !

Tactic:
by
  classical
  cases nonempty_fintype α
  simp only [← Nat.card_coe_set_eq, Set.coe_ofPred, card_eq_fintype_card]
  exact stabilizer_card f

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
⊢ t ^ ↑u • w = unitsSMul φ u w

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl)

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t ^ ↑1 • w = unitsSMul φ 1 w

case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t ^ ↑(-1) • w = unitsSMul φ (-1) w
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ of ↑((toSubgroupEquiv φ u) (⋯.equiv w.head).1) *
      (t ^ ↑u * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl)

Goal state after:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑((toSubgroupEquiv φ 1) (⋯.equiv w.head).1) *
      (t ^ ↑1 * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑1 * ReducedWord.prod φ w.toReducedWord

case neg.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels (-1) w
⊢ of ↑((toSubgroupEquiv φ (-1)) (⋯.equiv w.head).1) *
      (t ^ ↑(-1) * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑(-1) * ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ Equiv.swap a c ∈ M

Tactic:
Equiv.swap_comm,

Goal state after:
case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ Equiv.swap c a ∈ M
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝ : Finite Q
⊢ Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q

Tactic:
rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ Function.Injective ⇑(iteratedWreathToPermHom G 0)

Tactic:
simp only [IteratedWreathProduct_zero]
      apply Function.injective_of_subsingleton

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

Goal state before:
pp: case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ (i : ↥g.cycleFactorsFinset), ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
intro i
      refine ⟨⟨i, mem_centralizer_singleton_iff.mpr (self_mem_cycle_factors_commute i.2)⟩, ?_, rfl⟩
      exact Perm.ext fun x ↦ Subtype.ext (cycleFactorsFinset_mem_commute' g i.2 x.2).mul_inv_cancel

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ #{g | g.cycleType = m} = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
by
  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff,
    ← exists_with_cycleType_iff, not_exists]
  simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
H : ⟨c, hc⟩ ≠ ⟨d, hd⟩
⊢ #d.support + #(↑⟨d, hd⟩).support = #d.support * 2

Tactic:
mul_two

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
H : ⟨c, hc⟩ ≠ ⟨d, hd⟩
⊢ #d.support + #(↑⟨d, hd⟩).support = #d.support + #d.support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ σ ∈ ↑(kleinFour ↥s) ↔ ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}

Tactic:
coe_kleinFour_of_card_eq_four hs

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ σ ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}} ↔ ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.PowSaturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

Tactic:
refine ⟨fun h n g hgn ↦ ?_, fun h n g hgn ↦ by simpa using h n g (by simpa using hgn)⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
rcases eq_or_ne H ⊥ with rfl | h

Goal state after:
case ind.inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⁅⊥, ⊥⁆

case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
h : H ≠ ⊥
⊢ IsCyclic ↥⁅H, H⁆