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

Goal state before:
pp: case neg.inl
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac ^ k).totient

Tactic:
h0,

Goal state after:
case neg.inl
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac ^ 0).totient
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : x✝¹ ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2

Tactic:
rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₁ ++ (L₂ :: replicate n L₂).flatten)

Tactic:
flatten_cons,

Goal state after:
case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₁ ++ (L₂ ++ (replicate n L₂).flatten))
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 (L :: replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
flatten_cons,

Goal state after:
α : 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 (L ++ (replicate (n + 1) L).flatten) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ⁅upperCentralSeries G (n + 1), ⊤⁆ ≤ upperCentralSeries G n

Tactic:
apply closure_le _ |>.mpr
  rintro _ ⟨h, hh, g, _, rfl⟩
  exact mem_upperCentralSeries_succ_iff.mp hh g

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H 0
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
h0,

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ ⊥
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
⊢ reduceCyclically x.toWord = reduceCyclically y.toWord

Tactic:
simp only [replicate_succ, flatten_cons, append_assoc] at heq'

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  reduceCyclically x.toWord ++ ((replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord)) =
    reduceCyclically y.toWord ++ ((replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord))
⊢ reduceCyclically x.toWord = reduceCyclically y.toWord
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ (y.1 / x.1, 1) ∈ I → (1, x.2 / y.2) ∈ I

pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ (1, x.2 / y.2) ∈ I → (y.1 / x.1, 1) ∈ I

Tactic:
<;>

Goal state after:
case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ (y.1 / x.1, 1) ∈ I → (1, x.2 / y.2) ∈ I

case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ (1, x.2 / y.2) ∈ I → (y.1 / x.1, 1) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_3.refine_1
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ i ∈ Set.Iic (nilpotencyClass G)

pp: case refine_3.refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ j ∈ Set.Iic (nilpotencyClass G)

Tactic:
<;>

Goal state after:
case refine_3.refine_1
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ i ∈ Set.Iic (nilpotencyClass G)

case refine_3.refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ j ∈ Set.Iic (nilpotencyClass G)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hbase
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer ↑H = H → H = ⊤

pp: case hstep
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
<;>

Goal state after:
case hbase
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer ↑H = H → H = ⊤

case hstep
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g ↦ g • B) ∧ a ∈ b

Tactic:
· intro a
    obtain ⟨b : X, hb : b ∈ B⟩ := hBe
    obtain ⟨g, rfl⟩ := exists_smul_eq G b a
    use g • B
    simp only [Set.smul_mem_smul_set_iff, hb, Set.mem_range,
      exists_apply_eq_apply, and_imp, forall_exists_index,
      forall_apply_eq_imp_iff, true_and]
    exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • d • ↑s = b • ↑s

Tactic:
smul_coe_set hd

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • ↑s = b • ↑s
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y

Tactic:
use Classical.arbitrary G

Goal state after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.Subsingleton ∨ B = Set.univ

Tactic:
← B.ncard_le_one_iff_subsingleton,

Goal state after:
X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B = Set.univ
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mp.inl
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : ⟨B, ⋯⟩ = ⊥
⊢ IsTrivialBlock B

pp: case mp.inr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : ⟨B, ⋯⟩ = ⊤
⊢ IsTrivialBlock B

Tactic:
<;>

Goal state after:
case mp.inl
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : ⟨B, ⋯⟩ = ⊥
⊢ IsTrivialBlock B

case mp.inr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : ⟨B, ⋯⟩ = ⊤
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥sign.range = 2

Tactic:
MonoidHom.range_eq_top.mpr (sign_surjective α)

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥⊤ = 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * Nat.card ↥(alternatingGroup α) = Nat.card (Perm α)

Tactic:
by
  simp only [← alternatingGroup.index_eq_two (α := α), index_mul_card]

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✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥

Tactic:
← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a),

Goal state after:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ((block_stabilizerOrderIso G a) ⊥)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inr.«2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h✝ : Nontrivial α
hα : 2 ≤ 3
this : 1 < 2
⊢ Nat.factorial 2 / 2 ∣ 3

pp: case inr.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h✝ : Nontrivial α
hα : 3 ≤ 3
this : 1 < 3
⊢ Nat.factorial 3 / 2 ∣ 3

Tactic:
<;>

Goal state after:
case inr.«2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h✝ : Nontrivial α
hα : 2 ≤ 3
this : 1 < 2
⊢ Nat.factorial 2 / 2 ∣ 3

case inr.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h✝ : Nontrivial α
hα : 3 ≤ 3
this : 1 < 3
⊢ Nat.factorial 3 / 2 ∣ 3
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case succ.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * b ∈ closure {σ | σ.IsThreeCycle}

pp: case succ.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
<;>

Goal state after:
case succ.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * b ∈ closure {σ | σ.IsThreeCycle}

case succ.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap a (g a) * swap b c ∈ closure {g | g.cycleType = {2, 2}}

pp: case a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap b c * swap (g a) (g (g a)) ∈ closure {g | g.cycleType = {2, 2}}

Tactic:
<;>

Goal state after:
case a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap a (g a) * swap b c ∈ closure {g | g.cycleType = {2, 2}}

case a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap b c * swap (g a) (g (g a)) ∈ closure {g | g.cycleType = {2, 2}}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ _root_.Disjoint (swap 0 4).support (swap 1 3).support

Tactic:
support_swap h04,

Goal state after:
case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ _root_.Disjoint {0, 4} (swap 1 3).support
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, hg⟩ ∈ center ↥(alternatingGroup α)
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
⊢ k • ⟨g, hg⟩ • a = ⟨g, hg⟩ • k • a

Tactic:
rw [Subgroup.mem_center_iff] at hg'

Goal state after:
α : 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
⊢ k • ⟨g, hg⟩ • a = ⟨g, hg⟩ • k • a
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case succ
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
⊢ (fixingSubgroup G s).index * (Nat.card α - (k + 1))! = (Nat.card α)!

Tactic:
have : s.Nonempty := by
      rw [← Set.ncard_pos, hs]
      exact succ_pos k

Goal state after:
case succ
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
this : s.Nonempty
⊢ (fixingSubgroup G s).index * (Nat.card α - (k + 1))! = (Nat.card α)!
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 α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Injective ⇑(ofFixingSubgroup_insert_map a s)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h

Goal state after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h : (ofFixingSubgroup_insert_map a s) ⟨x, hx⟩ = (ofFixingSubgroup_insert_map a s) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
β : Type u_3
x y : ι ↪ β
⊢ ∃ σ, σ • x = y

Tactic:
by
  obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair x y x.injective y.injective
  exact ⟨σ, Function.Embedding.ext fun i => by simp [Function.Embedding.smul_apply, hσ]⟩

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
by
  constructor
  · apply isMultiplyPreprimitive_ofStabilizer
  · intro H
    rw [isMultiplyPreprimitive_iff]
    constructor
    · exact ofStabilizer.isMultiplyPretransitive.mpr H.isMultiplyPretransitive
    · intro s hs
      have : ∃ b : α, b ∈ s := by
        rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
        intro h
        apply not_lt.mpr hn
        rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
        simp only [← hs, zero_lt_one]
      obtain ⟨b, hb⟩ := this
      obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a
      rw [isPreprimitive_ofFixingSubgroup_conj_iff (g := g)]
      set s' := g • s with hs'
      let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s'
      have hst : s' = insert a (Subtype.val '' t) := by
        ext x
        constructor
        · intro hxs
          by_cases hxa : x = a
          · simp [hxa]
          · exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
        · rw [Set.mem_insert_iff]
          rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
          · simpa [s', ← hg]
          · simpa only using! hy
      rw [hst, isPreprimitive_fixingSubgroup_insert_iff]
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
      apply ENat.add_left_injective_of_ne_top ENat.one_ne_top
      simp only
      rw [← Nat.cast_one, ← Nat.cast_add, ← hs]
      apply congr_arg₂ _ _ rfl
      rw [show s = g⁻¹ • s' by simp [hs'],
        ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.natCast_one]
      exact notMem_val_image M t

Goal state after:
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 α := ⋯
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x

Tactic:
mem_fixingSubgroup_iff

Goal state after:
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
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x