mathlib-initiative/mathlib-tactics huggingface dataset:
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
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⟩

Tactic:
by_cases hij : j = i

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
hij : j = i
⊢ ⟨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⟩

case neg
ι : 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
hij : ¬j = i
⊢ ⟨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
t : W
ht : cs.IsReflection t
⊢ Odd (cs.length t)

Tactic:
suffices cs.lengthParity t = Multiplicative.ofAdd 1 by
    simpa [lengthParity_eq_ofAdd_length, ZMod.natCast_eq_one_iff_odd]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ cs.lengthParity t = Multiplicative.ofAdd 1
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₂ : W
⊢ cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2

Tactic:
rw [← ZMod.natCast_eq_natCast_iff', Nat.cast_add]
  simpa only [lengthParity_eq_ofAdd_length, ofAdd_add] using! map_mul cs.lengthParity w₁ w₂

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

Goal state before:
pp: case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ 1 ≤ cs.length (cs.simple i)

Tactic:
by_contra! length_lt_one
    have : cs.lengthParity (s i) = Multiplicative.ofAdd 0 := by
      rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
    have : Multiplicative.ofAdd (0 : ZMod 2) = Multiplicative.ofAdd 1 :=
      this.symm.trans (cs.lengthParity_simple i)
    contradiction

Goal state after:
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
i : B
⊢ cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Tactic:
nth_rw 1 [← length_inv]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD j 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
j : ℕ
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD j 1 =
    (cs.wordProd (drop (j + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))

Tactic:
rcases j with _ | j'

Goal state after:
case cons.zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD j 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD 0 1 =
    (cs.wordProd (drop (0 + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[0]?).getD 1 *
      cs.wordProd (drop (0 + 1) (i :: ω))

case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD j 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
j' : ℕ
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD (j' + 1) 1 =
    (cs.wordProd (drop (j' + 1 + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) * (Option.map cs.simple (i :: ω)[j]?).getD 1 * (cs.wordProd (take j (i :: ω)))⁻¹

Tactic:
rcases j with _ | j'

Goal state after:
case cons.zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD 0 1 =
    cs.wordProd (take 0 (i :: ω)) * (Option.map cs.simple (i :: ω)[0]?).getD 1 * (cs.wordProd (take 0 (i :: ω)))⁻¹

case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD (j' + 1) 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).last⟩ ∈ (singleton x✝ a✝).toList.getLast?

Tactic:
rw [Option.mem_def]
    rfl

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c

Tactic:
qsmul_of_nonneg ha.le

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ ⟨a, ⋯⟩ • b < ⟨a, ⋯⟩ • c
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
T : H.LeftTransversal := default
⊢ diff ϕ T (1 • T) = 1

Tactic:
by rw [one_smul, diff_self]

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ_surj : Function.Surjective ⇑φ
hφ_ker : φ.ker.IsFinitelyNormallyGenerated
⊢ (f.comp φ).ker.IsFinitelyNormallyGenerated

Tactic:
rw [← MonoidHom.comap_ker]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ_surj : Function.Surjective ⇑φ
hφ_ker : φ.ker.IsFinitelyNormallyGenerated
⊢ (Subgroup.comap φ f.ker).IsFinitelyNormallyGenerated
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
T : H.LeftTransversal
inst✝ : (center G).FiniteIndex
a b : G
⊢ ⟨(a * b) ^ (center G).index, ⋯⟩ = ⟨a ^ (center G).index, ⋯⟩ * ⟨b ^ (center G).index, ⋯⟩

Tactic:
by simp_rw [← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow, map_mul]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G)) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))

Tactic:
← pow_succ

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_2
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ (fun F ↦ ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g) (uncurry F' ⋯)

pp: case refine_3
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ ∀ (y : ActionCategory G A ⥤ CategoryTheory.SingleObj X),
    (fun F ↦ ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g) y →
      y = uncurry F' ⋯

Tactic:
· rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b⟩ ⟨e, h : IsFreeGroup.of e • a = b⟩
      change (F' (IsFreeGroup.of _)).left _ = _
      rw [hF']
      cases inv_smul_eq_iff.mpr h.symm
      rfl

Goal state after:
case refine_3
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ ∀ (y : ActionCategory G A ⥤ CategoryTheory.SingleObj X),
    (fun F ↦ ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g) y →
      y = uncurry F' ⋯
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w w' : α × Bool
⊢ (∀ (x : FreeGroup α), x.toWord[0]? = some w → ¬w = w') ↔ ¬w = w'

Tactic:
exact Iff.intro (fun h ↦ h (mk [w]) (by simp)) (by grind)

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a : α × Bool
hl : [a] = g.toWord
⊢ a = w

Tactic:
simpa [← hl, startsWith] using hg

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
⊢ a = w

Tactic:
simpa [← hl, startsWith] using hg

Goal state after:
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P : Generators G ι
f : G →* H
hf : Function.Surjective ⇑f
⊢ Subgroup.map f (Subgroup.closure (Set.range P.val)) = ⊤

Tactic:
P.closure_eq_top,

Goal state after:
G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P : Generators G ι
f : G →* H
hf : Function.Surjective ⇑f
⊢ Subgroup.map f ⊤ = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = comap (mk' (center G)) ⊤

Tactic:
rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]

Goal state after:
case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ Group.IsNilpotent G

Tactic:
use 1
  rw [upperCentralSeries_one]
  apply CommGroup.center_eq_top

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

Goal state before:
pp: M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
y : β
x' : α
⊢ ∃ g, g • f x' = y

Tactic:
obtain ⟨y', rfl⟩ := hf y

Goal state after:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x' y' : α
⊢ ∃ g, g • f x' = f y'
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ (range fun x ↦ orbit G x).PairwiseDisjoint id

Tactic:
by
  rintro s ⟨x, rfl⟩ t ⟨y, rfl⟩ h
  contrapose! h
  exact (orbit.eq_or_disjoint x y).resolve_right h

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

Goal state before:
pp: M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : IsTrivialBlock B
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
obtain hB | hB := hB
  · apply Or.intro_left; exact Set.Subsingleton.preimage hB hf
  · apply Or.intro_right; simp only [hB]; apply Set.preimage_univ

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B

Tactic:
by
  simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ Group.IsNilpotent G

Tactic:
have hcq : Nat.card (G ⧸ center G) < Nat.card G := by
      rw [card_eq_card_quotient_mul_card_subgroup (center G)]
      apply lt_mul_of_one_lt_right Nat.card_pos
      exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
    have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
    exact of_quotient_center_nilpotent hnq

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
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : ¬(g₂⁻¹ * g₁) • B = B
⊢ Disjoint ((g₂⁻¹ * g₁) • B) B

Tactic:
exact hB h

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 α
g : G
a b : α
hg : b = g • a
x✝ : ↥(stabilizer G a)
k : G
hk : k ∈ stabilizer G a
⊢ ∀ (x : ↥(ofStabilizer G a)), ⟨g • ↑(⟨k, hk⟩ • x), ⋯⟩ = (stabilizerEquivStabilizer hg) ⟨k, hk⟩ • ⟨g • ↑x, ⋯⟩

Tactic:
by
    simp [← SetLike.coe_eq_coe, subgroup_smul_def, stabilizerEquivStabilizer, ← smul_assoc]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
rw [Set.mem_iInter] at this

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : G), b ∈ ⋂ (_ : a ∈ i • A), i • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ alternatingGroup α ≤ closure {g | g.cycleType = {2, 2}}

Tactic:
· rw [← Equiv.Perm.closure_three_cycles_eq_alternating, Subgroup.closure_le]
    intro g hg3
    obtain ⟨a, ha⟩ := hg3.isCycle.nonempty_support
    have h_support := hg3.support_eq_iff_mem_support.mpr ha
    have h_nodup := hg3.nodup_iff_mem_support.mpr ha
    have : 1 < g.supportᶜ.card := by grind [Finset.card_compl, Nat.card_eq_fintype_card]
    obtain ⟨b, c, hb, hc, hbc⟩ := Finset.one_lt_card_iff.mp this
    have H : g = (swap a (g a) * (swap b c)) * (swap b c * (swap (g a) (g (g a)))) := by
      simp [mul_assoc, ← hg3.eq_swap_mul_swap_iff_mem_support.mpr ha]
    rw [H]
    apply mul_mem <;>
    · apply Subgroup.subset_closure
      exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ {g | g.cycleType = {2, 2}} ⊆ ↑(alternatingGroup α)

Tactic:
intro g hg
  rw [Set.mem_ofPred_eq] at hg
  simp [sign_of_cycleType, hg, ← Units.val_inj]

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

Goal state before:
pp: g : Perm (Fin 5)
ha : Even g.cycleType.card
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
isConj_iff_cycleType_eq,

Goal state after:
g : Perm (Fin 5)
ha : Even g.cycleType.card
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = g.cycleType
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: 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 : α →ₑ[σ] β
ι : Type u_5
hf : Injective ⇑f
⊢ Injective ⇑(mulActionHom_embedding ι hf)

Tactic:
intro _ _ hxy

Goal state after:
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 : α →ₑ[σ] β
ι : Type u_5
hf : Injective ⇑f
a₁✝ a₂✝ : ι ↪ α
hxy : (mulActionHom_embedding ι hf) a₁✝ = (mulActionHom_embedding ι hf) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: 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 • x = y

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq (M := G) (aux x) (aux y)

Goal state after:
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
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
⊢ G = alternatingGroup α

Tactic:
by
  nontriviality α
  obtain ⟨_, ⟨a, b, hab, rfl⟩, habG⟩ : ∃ g : Perm α, g.IsSwap ∧ g ∉ G := by
    by_contra! h
    suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
    rwa [eq_top_iff, ← closure_isSwap, G.closure_le]
  ext g
  refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_
  rw [mul_mem_iff_of_index_two hG, mul_mem_iff_of_index_two alternatingGroup.index_eq_two, ih]
  refine iff_congr (iff_of_false ?_ (by cases (sign_swap hxy).symm.trans ·)) Iff.rfl
  contrapose habG
  rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec]
  exact (normal_of_index_eq_two hG).conj_mem _ habG _

Goal state after: