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

Goal state before:
pp: case zero
⊢ Nat.card (DihedralGroup 0) = 2 * 0

Tactic:
Nat.card_eq_zero_of_infinite

Goal state after:
case zero
⊢ 0 = 2 * 0
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) = Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation)

Tactic:
apply congrArg Set.range

Goal state after:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := ⋯
⊢ uncurry M'.relation ∘ Prod.map ⇑e ⇑e = ⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
m : ι
ih : G m
⊢ of ⟨m, ih⟩.snd⁻¹ * of ih = 1

Tactic:
rw [← of.map_mul, inv_mul_cancel, of.map_one]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ (if Even (2 * k + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Tactic:
rw [if_neg this]

Goal state after:
case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Tactic:
rw [if_neg this]

Goal state after:
case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 1 ↔ ∃ i, w = cs.simple i

Tactic:
by
  constructor
  · intro h
    rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
    rcases List.length_eq_one_iff.mp (hω.symm.trans h) with ⟨i, rfl⟩
    exact ⟨i, cs.wordProd_singleton i⟩
  · rintro ⟨i, rfl⟩
    exact cs.length_simple i

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = j) →
    (m₁ = m₂ * 1 ↔ (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂)

Tactic:
rw [fstIdx]

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = j) →
    (m₁ = m₂ * 1 ↔
      (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬Option.map Sigma.fst w.toList.head? = some j ∧ m₁ = m₂)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝¹ : ℕ
hM : M.M i i' ≠ 0
m✝ : ℕ
m : (M.M i i').succ.le m✝
ih : cs.IsReduced (alternatingWord i i' m✝.succ)
⊢ cs.IsReduced (alternatingWord i i' m✝)

Tactic:
alternatingWord_succ'

Goal state after:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝¹ : ℕ
hM : M.M i i' ≠ 0
m✝ : ℕ
m : (M.M i i').succ.le m✝
ih : cs.IsReduced ((if Even m✝ then i' else i) :: alternatingWord i i' m✝)
⊢ cs.IsReduced (alternatingWord i i' m✝)
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) → a⁻¹ * b ∈ H

pp: case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2 ∈ ⊥, ∃ b_1 ∈ H, b = a_2 * a * b_1

Tactic:
· rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
    rwa [one_mul, inv_mul_cancel_left]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2 ∈ ⊥, ∃ b_1 ∈ H, b = a_2 * a * b_1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i ^ 1 • (Y i)ᶜ ⊆ X i

Tactic:
| base =>

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast • Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) q).fst)) =
    q

Tactic:
Quotient.coe_smul_out,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast • Quotient.out ((H.quotientEquivSigmaZMod g) q).fst = q
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i ^ (-1) • (X i)ᶜ ⊆ Y i

Tactic:
| base =>

Goal state after:
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 ∈ ⊤
⊢ ∀ x ∈ closure S, ∀ y ∈ S, x ∈ ↑(closure U) * R → x * y⁻¹ ∈ ↑(closure U) * R

Tactic:
· rintro - - s hs ⟨u, hu, r, hr, rfl⟩
    rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
    refine Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2
    refine subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, ?_⟩
    rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]
    apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
      (hR.mul_inv_toRightFun_mem (f (r * s⁻¹) * s))
    rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
    exact hR.toRightFun_mul_inv_mem (r * s⁻¹)

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q ↦ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩)
          Finset.univ.toList).prod =
    g ^ H.index

Tactic:
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow,
      index_eq_sum_minimalPeriod H g, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_map_toList]

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q ↦
            ⟨(Quotient.out q.out)⁻¹ * ↑⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ ↑⟨g, ⋯⟩ • x) q.out * Quotient.out q.out,
              ⋯⟩)
          Finset.univ.toList).prod =
    ↑(List.map (fun i ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out) Finset.univ.toList).prod
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
⊢ reduce (replicate (n + 1 + 1) L).flatten =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
rw [replicate_succ, flatten_cons, ← reduce_append_reduce_reduce, ih, h.reduce_eq]
    nth_rewrite 1 [← conj_conjugator_reduceCyclically L]
    have {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)} : reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) =
        reduce (L₁ ++ (L₂ ++ L₄) ++ L₅) := by
      apply reduce.sound
      repeat rw [← mul_mk]
      rw [← inv_mk]
      group
    rw [this, ← flatten_cons, ← replicate_succ, ← isReduced_iff_reduce_eq]
    apply IsReduced.append_flatten_replicate_append (hn := by simp)
    · exact isCyclicallyReduced h
    · rwa [conj_conjugator_reduceCyclically]

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ (QuotientGroup.mk' (P.prod Q).range.goursatFst) g = 1 ∧ (QuotientGroup.mk' (P.prod Q).range.goursatSnd) h = 1 ↔
    g ∈ (P.prod Q).range.goursatFst ∧ h ∈ (P.prod Q).range.goursatSnd

Tactic:
← MonoidHom.mem_ker,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ g ∈ (QuotientGroup.mk' (P.prod Q).range.goursatFst).ker ∧ h ∈ (QuotientGroup.mk' (P.prod Q).range.goursatSnd).ker ↔
    g ∈ (P.prod Q).range.goursatFst ∧ h ∈ (P.prod Q).range.goursatSnd
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) = ⊥

Tactic:
rw [top_lowerCentralSeries_pi_of_finite, pi_eq_bot_iff]

Goal state after:
case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∀ (i : η), ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) = ⊥
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mp
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'

Tactic:
rintro hBB' b hb
      obtain ⟨k, rfl⟩ := htGX.exists_smul_eq a b
      suffices k ∈ stabilizer G B' by
        exact this.symm ▸ (Set.smul_mem_smul_set ha')
      exact hBB' (hB.smul_eq_of_mem ha hb)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ k ∈ ConjAct.toConjAct g • ofSubtype.range ↔ k ∈ ofSubtype.range

Tactic:
Subgroup.mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ (ConjAct.toConjAct g)⁻¹ • k ∈ ofSubtype.range ↔ k ∈ ofSubtype.range
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α

Tactic:
exact {
      isTrivialBlock_of_isBlock {B} hB := by
        rw [← Set.preimage_image_eq B hf.injective]
        exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective)) }

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : Nontrivial X
inst✝ : IsPreprimitive G X
a : X
⊢ IsCoatom (stabilizer G a)

Tactic:
by
  rwa [isCoatom_stabilizer_iff_preprimitive]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
⊢ IsCyclic ↥(alternatingGroup α)

Tactic:
cases subsingleton_or_nontrivial α
  · infer_instance
  have : 1 < Nat.card α := Finite.one_lt_card
  apply isCyclic_of_card_dvd_prime (p := 3)
  rw [nat_card_alternatingGroup]
  interval_cases (Nat.card α) <;> simp [Nat.factorial_succ]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
i : Fin n
⊢ (Fin.Embedding.init (g • x)) i ∈ ofStabilizer G a

Tactic:
simp only [mem_ofStabilizer_iff,
      Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]
    suffices Fin.Embedding.init (g • x) i = (g • x) i.castSucc by
      simp [this]
    simp [Fin.Embedding.init, Fin.init_def]

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

Goal state before:
pp: α : 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
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ a ∉ σ.support ∧ b ∉ σ.support

Tactic:
exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: case h
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
y : Fin n ↪ ↑sᶜ
⊢ Disjoint s (range ⇑(y.trans (subtype fun x ↦ x ∈ sᶜ)))

Tactic:
rw [Set.disjoint_right]

Goal state after:
case h
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
y : Fin n ↪ ↑sᶜ
⊢ ∀ ⦃a : α⦄, a ∈ range ⇑(y.trans (subtype fun x ↦ x ∈ sᶜ)) → a ∉ s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this : ⇑(alternatingGroup α).subtype '' {x | ↑x ∈ {g | g.cycleType = {2, 2}}} = {g | g.cycleType = {2, 2}}
⊢ closure (⇑(alternatingGroup α).subtype '' {g | (↑g).cycleType = {2, 2}}) = map (alternatingGroup α).subtype ⊤

Tactic:
have := closure_cycleType_eq_two_two_eq_alternatingGroup h5

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this✝ : ⇑(alternatingGroup α).subtype '' {x | ↑x ∈ {g | g.cycleType = {2, 2}}} = {g | g.cycleType = {2, 2}}
this : closure {g | g.cycleType = {2, 2}} = alternatingGroup α
⊢ closure (⇑(alternatingGroup α).subtype '' {g | (↑g).cycleType = {2, 2}}) = map (alternatingGroup α).subtype ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
φ : Perm α ≃* Perm α
a✝ : Nontrivial α
⊢ (comap φ.toMonoidHom (alternatingGroup α)).index = 2

Tactic:
rw [index_comap_of_surjective _ (Equiv.surjective _), alternatingGroup.index_eq_two]

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 α
x✝ : ↥(fixingSubgroup M s)
x : α
c : M
hc : c ∈ fixingSubgroup M s
⊢ x ∈ sᶜ → ⟨c, hc⟩ • x ∈ sᶜ

Tactic:
rw [← Subgroup.inv_mem_iff] at hc

Goal state after:
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
⊢ x ∈ sᶜ → ⟨c, hc✝⟩ • x ∈ sᶜ
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
⊢ 1 ≤ t.ncard

Tactic:
rw [Nat.one_le_iff_ne_zero]

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
⊢ t.ncard ≠ 0
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s

Tactic:
rw [mem_stabilizer_iff]

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k • s = s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s

Tactic:
rw [mem_stabilizer_iff]

Goal state after:
α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
⊢ ofSubtype g • s = s
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right.hφ
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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
k : N
hk : k ∈ fixingSubgroup N t
⊢ ∃ a, ψ a = ⟨k, hk⟩

Tactic:
obtain ⟨k, rfl⟩ := hφ k

Goal state after:
case right.hφ
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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
k : M
hk : φ k ∈ fixingSubgroup N t
⊢ ∃ a, ψ a = ⟨φ k, hk⟩
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b ∈ stabilizer (Perm α) s

Tactic:
rw [mem_stabilizer_iff]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s = s
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
⊢ IsTrivialBlock B

Tactic:
rcases le_or_gt (Nat.card α) 2 with h2 | h2
  · exact isTrivialBlock_of_card_le_two h2 B
  rcases le_or_gt (Nat.card α) 3 with h3 | h4
  · replace h3 : Nat.card α = 3 := le_antisymm h3 h2
    have : IsPretransitive (alternatingGroup α) α := isPretransitive_of_three_le_card α h3.ge
    have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)
    exact this.isTrivialBlock_of_isBlock hB
  -- IsTrivialBlock hB, for 4 ≤ Nat.card α
  suffices IsPreprimitive (alternatingGroup α) α by
    apply IsPreprimitive.isTrivialBlock_of_isBlock hB
  apply isPreprimitive_of_is_two_pretransitive
  let := isMultiplyPretransitive α
  apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
  rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_of_lt h2)]

Goal state after:
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
n : N
⊢ S.rightHom (S.inl n) = 1

Tactic:
← MonoidHom.mem_ker,

Goal state after:
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
n : N
⊢ S.inl n ∈ S.rightHom.ker