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

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
hbc : b ≤ c
ma : M
sa : ℕ+
hab : mk ma sa ≤ b
⊢ mk ma sa ≤ c

Tactic:
| mk ma sa
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
hbc : b ≤ c
ma : M
sa : ℕ+
hab : mk ma sa ≤ b
⊢ mk ma sa ≤ c
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
h : mk ma sa ≤ b
h' : b ≤ mk ma sa
⊢ mk ma sa = b

Tactic:
| mk ma sa
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
h : mk ma sa ≤ b
h' : b ≤ mk ma sa
⊢ mk ma sa = b
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
⊢ mk ma sa ≤ b ∨ b ≤ mk ma sa

Tactic:
| mk ma sa
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
⊢ mk ma sa ≤ b ∨ b ≤ mk ma sa
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
h : b < c
ma : M
sa : ℕ+
⊢ mk ma sa + b < mk ma sa + c

Tactic:
| mk ma sa
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
h : b < c
ma : M
sa : ℕ+
⊢ mk ma sa + b < mk ma sa + c
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * (s * (↑⟨r, hr⟩)⁻¹) ∈ ↑H

Tactic:
← inv_inv s,

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ ↑(f (r * s⁻¹⁻¹⁻¹)) * (s⁻¹⁻¹ * (↑⟨r, hr⟩)⁻¹) ∈ ↑H
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ (S.lowerCentralSeries (d + 1)).Characteristic

Tactic:
lowerCentralSeries_succ

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic
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:
lowerCentralSeries_succ

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑⁅S.lowerCentralSeries n, S⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ (S.lowerCentralSeries (n + 1)).Normal

Tactic:
lowerCentralSeries_succ

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n ≤ pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ (pi Set.univ Ss).lowerCentralSeries (n + 1) ≤ pi Set.univ fun i ↦ (Ss i).lowerCentralSeries (n + 1)

Tactic:
lowerCentralSeries_succ

Goal state after:
case succ
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n ≤ pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ ⁅(pi Set.univ Ss).lowerCentralSeries n, pi Set.univ Ss⁆ ≤ pi Set.univ fun i ↦ ⁅(Ss i).lowerCentralSeries n, Ss i⁆
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
b : α
⊢ b ∈ orbit (↥N) a ↔ b ∈ {a}

Tactic:
Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
b : α
⊢ b ∈ {a} ↔ b ∈ {a}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ∀ (g_1 : ↥(alternatingGroup α)), g_1 * ⟨g, hg⟩ = ⟨g, hg⟩ * g_1
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
hkga : k • g a = c
this : k ∈ alternatingGroup α
⊢ k • ⟨g, hg⟩ • a = ⟨g, hg⟩ • k • a

Tactic:
by
    simp only [← Subgroup.mk_smul k this, ← mul_smul, hg']

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

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : g • aux x = aux y
i : n
⊢ (σ g • x) i = y i

Tactic:
rw [DFunLike.ext_iff] at hg

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : ∀ (x_1 : n), (g • aux x) x_1 = (aux y) x_1
i : n
⊢ (σ g • x) i = y i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ k ∈ (ofSubtype s).range ↔ (↑k).support ⊆ s

Tactic:
by
  rw [range_ofSubtype, mem_subgroupOf, Perm.mem_range_ofSubtype_iff]
  simp

Goal state after:
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 α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
rw [Ne, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne, ← Set.nonempty_iff_ne_empty] at ha

Goal state after:
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
ha : (s ∪ g • s)ᶜ.Nonempty
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ ∀ {s : Set α}, s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
· intro s hs
    obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le hn
    apply isPreprimitive_of_is_two_pretransitive
    have hs' : s.encard = m := by
      simp only [hm, Nat.succ_eq_add_one, zero_add, add_comm 1] at hs
      exact ENat.add_left_injective_of_ne_top ENat.one_ne_top hs
    have : Finite s := Set.finite_of_encard_eq_coe hs'
    apply ofFixingSubgroup.isMultiplyPretransitive (G := M) s (n := n.succ)
    simp [Set.ncard, hs', hm, add_comm 1]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

Tactic:
· obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
      rcases lt_or_eq_of_le (le_sub_one_of_lt j.prop) with hj | hj
      · suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
        apply EmbeddingLike.injective (g • x)
        rw [hgk' j hj, hxj]
      · rw [← hxj]
        apply congr_arg
        rw [Fin.ext_iff, hi, hj]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨a, b, hab, hs⟩ := Finset.card_eq_two.mp this

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

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

Tactic:
have : ∀ (t : Set α) (_ : 1 < t.encard), ∃ (g : Perm α),
      g.IsSwap ∧ g ∈ stabilizer (Perm α) t := by
    intro t ht
    rw [Set.one_lt_encard_iff] at ht
    obtain ⟨a, b, ha, hb, h⟩ := ht
    use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb

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

Goal state before:
pp: n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)

Tactic:
isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))

Goal state after:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ IsMultiplyPreprimitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)
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 α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
this : φ g = φ 1
⊢ g • a = a

Tactic:
conv_rhs => rw [← one_smul K a]

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 α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
this : φ g = φ 1
⊢ g • a = 1 • a
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case neg
α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : ¬s.Nontrivial
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
· simp only [not_nontrivial_iff] at h0'
      apply isCoatom_stabilizer_singleton _ h0 h0'
      rw [← ncard_add_ncard_compl s]
      rw [← ncard_pos] at h0 h1
      grind

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

Goal state before:
pp: case hf.refine_1
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : (toPermHom G ↑(powersetCard α n)) g = 1
⊢ ↑n < ENat.card α

Tactic:
simpa [ENat.card_eq_coe_natCard, Nat.cast_lt, Nat.finite_of_card_ne_zero (ne_zero_of_lt hn')]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ x.length ∈ List.map List.length p

Tactic:
List.mem_map

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, a.length = x.length
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
⊢ ReducedWord.prod φ (unitsSMul φ u w).toReducedWord = t ^ ↑u * ReducedWord.prod φ w.toReducedWord

Tactic:
by
  rw [unitsSMul]
  split_ifs with hcan
  · cases w using consRecOn
    · simp [Cancels] at hcan
    · cases hcan.2
      simp only [unitsSMulWithCancel, id_eq, consRecOn_cons, prod_group_smul, prod_cons, zpow_neg]
      rcases Int.units_eq_one_or u with (rfl | rfl)
      · simp [equiv_eq_conj, mul_assoc]
      · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
        -- simp [equiv_symm_eq_conj, mul_assoc].
        simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
          Int.reduceNeg, zpow_neg, zpow_one, inv_inv]
        erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]
  · simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]
    rcases Int.units_eq_one_or u with (rfl | rfl)
    · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
      -- simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul].
      simp only [toSubgroup_neg_one, toSubgroup_one, toSubgroupEquiv_one, equiv_eq_conj, mul_assoc,
        Units.val_one, zpow_one, inv_mul_cancel_left, mul_right_inj]
      erw [(d.compl 1).equiv_snd_eq_inv_mul]
      simp [mul_assoc]
    · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
      -- simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul]
      simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
        Int.reduceNeg, zpow_neg, zpow_one, mul_assoc]
      erw [equiv_symm_eq_conj, (d.compl (-1)).equiv_snd_eq_inv_mul]
      simp [mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ ↑n ≡ m [ZMOD ↑(#(↑c).support)]

Tactic:
← IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset c.prop) (mem_support_self a c)

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ (g ^ ↑n) (a c) = (g ^ m) (a c)
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
⊢ (if f b = f a then a else if f b = a then f a else f b) ∈ orbit (↥(closure S)) b

Tactic:
split_ifs with h1 h2

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : f b = f a
⊢ a ∈ orbit (↥(closure S)) b

case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬f b = f a
h2 : f b = a
⊢ f a ∈ orbit (↥(closure S)) b

case neg
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬f b = f a
h2 : ¬f b = a
⊢ f b ∈ orbit (↥(closure S)) b
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ b ∈ fixedBy α (Equiv.swap (f a) a * f)

Tactic:
mem_fixedBy,

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ (Equiv.swap (f a) a * f) • b = b
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (of i) ((φ i) x) = (base φ) x

Tactic:
rw [← MonoidHom.comp_apply, of_comp_eq_base]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if ¬Odd (n + 1) then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
Nat.odd_add_one,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if ¬¬Odd n then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0