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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
⊢ (x : ConjClasses G) × ↑x.carrier ≃ G

Tactic:
simpa [carrier_eq_preimage_mk] using! Equiv.sigmaFiberEquiv ConjClasses.mk

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

Tactic:
rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype,
      ← Finset.sum_set_coe]
    simp

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

Goal state before:
pp: n : ℕ
i : ZMod n
k : ℤ
⊢ r i ^ k = r (i * ↑k)

Tactic:
by
  cases k <;> simp [r_pow, neg_mul_eq_mul_neg]

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r 1 ^ orderOf (r 1) = 1
⊢ False

Tactic:
r_one_pow

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r ↑(orderOf (r 1)) = 1
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
⊢ n = 1 ∨ n = 2 → IsMulCommutative (DihedralGroup n)

Tactic:
by rintro (rfl | rfl) <;> exact ⟨⟨by decide⟩⟩

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

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
have hn' : NeZero n := ⟨hn.pos.ne'⟩

Goal state after:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ ↑((n + 3) / 2) / ↑(2 * n) = (↑n + 3) / (4 * ↑n)

Tactic:
qify [show 2 ∣ n + 3 by rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]]

Goal state after:
n : ℕ
hn : Odd n
⊢ (↑n + 3) / 2 / (2 * ↑n) = (↑n + 3) / (4 * ↑n)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ toProd (inl x.1) * toProd (inr x.2) = x

Tactic:
toProd_apply_inl,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ (x.1, 1) * toProd (inr x.2) = x
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

pp: case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
· rw [if_pos h_even, ← add_assoc]
    simp only [ite_eq_right_iff, isEmpty_Prop, Nat.not_even_iff_odd, Even.add_one h_even,
      IsEmpty.forall_iff]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
subst k

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
tail : Word M
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
g : M j
h1 : tail.fstIdx ≠ some j
h2 : g ≠ 1
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (t * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w

Tactic:
cs.length_inv w

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (t * w) < cs.length w ↔ cs.length (t * w) < cs.length w
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 : ¬∃ (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:
revert h
        rw [fstIdx]
        cases w.toList
        · simp
        · simp +contextual [Sigma.ext_iff]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ (rcons
        (have __src := (equivPair i✝) w✝;
        { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ })).prod =
    of m✝ * w✝.prod

Tactic:
prod_rcons,

Goal state after:
case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of
        (have __src := (equivPair i✝) w✝;
          { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).head *
      (have __src := (equivPair i✝) w✝;
          { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.prod =
    of m✝ * w✝.prod
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
i j : ι
w' : NeWord M i j
hnot1✝ : ∀ l_1 ∈ x :: ⟨i, w'.head⟩ :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ ⟨i, w'.head⟩ :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: ⟨i, w'.head⟩ :: l)
hchain : x.fst ≠ ⟨i, w'.head⟩.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (⟨i, w'.head⟩ :: l)
h : { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
hw' : w'.toList = ⟨i, w'.head⟩ :: l
⊢ ((singleton x.snd ⋯).append ⋯ w').toWord.toList =
    { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList

Tactic:
simpa [toWord] using hw'

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s = mk m' s' ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'

Tactic:
by
  unfold mk
  rw [LocalizedModule.mk_eq, ↑ⁿ.exists_congr_left]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset a ↑H ↑K) (doubleCoset b ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K

Tactic:
rw [disjoint_comm] at h

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b ↑H ↑K) (doubleCoset a ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑⊥ ↑H) a b ↔ (QuotientGroup.leftRel H) a b

Tactic:
rel_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ (QuotientGroup.leftRel H) a b
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑H ↑⊥) a b ↔ (QuotientGroup.rightRel H) a b

Tactic:
rel_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ (QuotientGroup.rightRel H) a b
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
this✝¹ : Fintype ↥H
this✝ : HasEnoughRootsOfUnity M (Monoid.exponent ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ Nat.card ↥(domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H) * Nat.card ↥H / Nat.card ↥H

Tactic:
mul_div_cancel_right₀ _ (Fintype.card_eq_nat_card ▸ Fintype.card_ne_zero),

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
this✝¹ : Fintype ↥H
this✝ : HasEnoughRootsOfUnity M (Monoid.exponent ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ Nat.card ↥(domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_2
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⟩

Goal state after:
case refine_2
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
⊢ (fun x1 x2 ↦ x1 * x2) u r * s ∈ ↑(closure U) * R
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⟩

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
⊢ (fun x1 x2 ↦ x1 * x2) u r * s⁻¹ ∈ ↑(closure U) * R
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:
← mul_inv_rev,

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⁻¹⁻¹⁻¹)) * (↑⟨r, hr⟩ * s⁻¹)⁻¹ ∈ ↑H
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 ^ 0).totient

Tactic:
pow_zero,

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.totient 1)
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ (↑P).transferFocal.ker ⊓ ↑P = (↑P).focalSubgroup

Tactic:
← subgroupOf_map_subtype,

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ map (↑P).subtype ((↑P).transferFocal.ker.subgroupOf ↑P) = (↑P).focalSubgroup
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G

Tactic:
simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, mem_bot, mem_mk,
    Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_ofPred_eq, mem_center_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
x✝ : G
⊢ (∀ (y : G), ⁅x✝, y⁆ = 1) ↔ ∀ (g : G), g * x✝ = x✝ * g
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ map S.subtype (⊤.lowerCentralSeries n) = map S.subtype ⊥

Tactic:
map_bot,

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ map S.subtype (⊤.lowerCentralSeries n) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ map S.subtype (⊤.lowerCentralSeries n) = ⊥

Tactic:
top_subtype_lowerCentralSeries

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ S.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n

Tactic:
top_subtype_lowerCentralSeries

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = map H.subtype ⊥

Tactic:
map_bot,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = map H.subtype ⊥

Tactic:
map_bot,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = ⊥
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
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ y * z * (y⁻¹ * z⁻¹) = 1

Tactic:
← mul_inv_rev,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ y * z * (z * y)⁻¹ = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

Tactic:
have : IsNilpotent G := isNilpotent_of_ker_le_center f hf1

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ IsTrivialBlock (g • B)

Tactic:
left
    exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.comap ↑(MulAut.conj g) ⊤)) B

Tactic:
Subgroup.comap_top

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) B
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ∣ H.index

Tactic:
rwa [← Coprime.dvd_mul_right, mul_factorial_pred hp.ne_zero]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index.Coprime (H.index - 1)!
Module: Mathlib.GroupTheory.GroupAction.Blocks

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

Tactic:
by
    rintro ⟨B, ha, hB⟩; rintro ⟨B', ha', hB'⟩
    simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk]
    constructor
    · 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)
    · intro hBB' g hgB
      apply hB'.smul_eq_of_mem ha'
      exact hBB' <| hgB.symm ▸ (Set.smul_mem_smul_set ha)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Nontrivial α
this : 1 < Nat.card α
⊢ Nat.card ↥(alternatingGroup α) ∣ 3

Tactic:
nat_card_alternatingGroup

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Nontrivial α
this : 1 < Nat.card α
⊢ (Nat.card α).factorial / 2 ∣ 3
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
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B

Tactic:
· rw [is_two_pretransitive_iff] at h2
      obtain ⟨g, hga, hgb⟩ := h2 h h'
      rw [MulAction.isBlock_iff_smul_eq_of_mem] at hB
      rw [← hB (g := g) ha (by rw [hga]; exact ha), ← hgb]
      exact smul_mem_smul_set hb

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : G.index = Nat.succ 0
⊢ alternatingGroup α ≤ G

pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G

Tactic:
· exact index_eq_one.mp h ▸ le_top

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G
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:
← Subgroup.inv_mem_iff

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: case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
h : G
hinvab : h • ↑b = a
⊢ ↑b = ↑c

Tactic:
rw [eq_comm, ← inv_smul_eq_iff] at hinvab

Goal state after:
case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ ↑b = ↑c
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case e'_2
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 α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card ↥(ofStabilizer G a)

Tactic:
{

Goal state after:
case e'_2
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 α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card ↥(ofStabilizer G a)