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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
rw [tsub_eq_of_eq_add (mul_two (M i i'))] at this

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
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₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

Tactic:
by
  simpa using cs.length_mul_le (w₁ * w₂) w₂⁻¹

Goal state after:
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 : W
i : B
⊢ cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i

Tactic:
simp [IsRightInversion, IsRightDescent, cs.isReflection_simple i]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp.inr
ι : 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 : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

Tactic:
have h1n : n ≤ -1 := by
        apply Int.le_of_lt_add_one
        simpa using hgt

Goal state after:
case hpp.inr
ι : 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 : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
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:
rw [← pow_succ] at h2

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.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
⊢ g * g = 1

Tactic:
← sq,

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
⊢ g ^ 2 = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
⊢ IsDescendingCentralSeries fun m ↦ H (n - m)

Tactic:
by
  obtain ⟨h0, hH⟩ := hasc
  refine ⟨hn, fun x m hx g => ?_⟩
  dsimp at hx
  by_cases! hm : n ≤ m
  · rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx
    subst hx
    rw [commutatorElement_one_left]
    exact Subgroup.one_mem _
  · apply hH
    convert! hx using 1
    rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
by
  rw [nilpotencyClass_def]
  refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
  · intro n hn
    exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
  · rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← top_le_iff, ← hn]
    exact ascending_central_series_le_upper H hH n

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
classical apply Nat.find_mono

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
classical apply Nat.find_mono

Goal state after:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → upperCentralSeries G' n = ⊤
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
this : (functorOfMonoidHom T E).map x = F'.map x
⊢ E x = (Functor.mapEnd (root' T) F') x

Tactic:
simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using! this

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G

Tactic:
rw [upperCentralSeries_one]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case h
G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ upperCentralSeries G 1 = ⊤

Tactic:
rw [upperCentralSeries_one]

Goal state after:
case h
G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X ↔ orbit G a = Set.univ

Tactic:
by
  rw [isPretransitive_iff_base a, Set.ext_iff]
  apply forall_congr'
  intro x
  simp_rw [Set.mem_univ, iff_true, mem_orbit_iff]

Goal state after:
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
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ stabilizer G (orbit (↥H) a)
b : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) b) = a
⊢ g ∈ H

Tactic:
simp_rw [H.toSubmonoid.smul_def, ← mul_smul, ← mem_stabilizer_iff] at h

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ stabilizer G (orbit (↥H) a)
b : ↥H
h : g * ↑b ∈ stabilizer G a
⊢ g ∈ H
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
⊢ stabilizer G (orbit (↥H) a) = H

Tactic:
ext g
  constructor
  · intro hg
    obtain ⟨-, ⟨b, rfl⟩, h⟩ := hg.symm ▸ mem_orbit_self a
    simp_rw [H.toSubmonoid.smul_def, ← mul_smul, ← mem_stabilizer_iff] at h
    exact (mul_mem_cancel_right b.2).mp (hH h)
  · intro hg
    rw [mem_stabilizer_iff, ← Subgroup.coe_mk H g hg, ← Submonoid.smul_def (S := H.toSubmonoid)]
    apply smul_orbit (G := H)

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

Goal state before:
pp: case mpr
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'
⊢ B ⊆ B' → ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩

Tactic:
intro hBB' g hgB

Goal state after:
case mpr
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'
hBB' : B ⊆ B'
g : G
hgB : g ∈ ↑⟨stabilizer G B, ⋯⟩
⊢ g ∈ ↑⟨stabilizer G B', ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
hmn : m ≤ n
hn : ↑n ≤ ENat.card α
⊢ Surjective fun x ↦ (castLEEmb hmn).trans x

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact Fin.Embedding.restrictSurjective_of_add_le_ENatCard hn

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

Goal state before:
pp: case 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
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})

Tactic:
obtain ⟨b, c, hb, hc, hbc⟩ := Finset.one_lt_card_iff.mp this

Goal state after:
case 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
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
⊢ ∃ g, g • x = y

Tactic:
suffices g ∈ fixingSubgroup G s by
      use ⟨g, this⟩
      ext i
      rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]
      simp [← ofFixingSubgroup.append_right, ← smul_apply, ← hx, ← hy, hg]

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
⊢ g ∈ fixingSubgroup G s
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr.right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ ∀ {s : Set ↥(ofStabilizer M a)},
    s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)

Tactic:
intro s hs

Goal state after:
case inr.right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ ∀ {s : Set α}, s.encard + 1 = ↑n.succ → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
intro s hs

Goal state after:
case mpr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ (MulAut.conj g) ((MulAut.conj g⁻¹) k) = k

Tactic:
simp [MulAut.conj]; group

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 α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) m

Tactic:
apply ofFixingSubgroup.isMultiplyPretransitive _ s hs

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

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

Tactic:
intro s hs

Goal state after:
case inr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
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 α
inst✝ : Finite α
hs : IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
apply IsPreprimitive.of_card_lt (f := ofFixingSubgroup_of_inclusion M Set.inter_subset_left)

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
inst✝ : Finite α
hs : IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ Nat.card ↥(ofFixingSubgroup M (s ∩ g • s)) < 2 * (Set.range ⇑(ofFixingSubgroup_of_inclusion M ⋯)).ncard
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right
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 α}, s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
intro s hs

Goal state after:
case right
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
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x

Tactic:
· rw [← Set.mem_compl_iff] at hx
      obtain ⟨k, hk⟩ := hs' b hb x hx
      use k * g
      rw [mul_smul, hgab, hk]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ sᶜ.Nontrivial

Tactic:
rw [← one_lt_ncard_iff_nontrivial]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ 1 < sᶜ.ncard
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ S.inl n * σ (g₁ * g₂) = σ g₁ * σ g₂

Tactic:
← eq_mul_inv_iff_mul_eq,

Goal state after:
case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ (S.rightHom (Function.surjInv ⋯ (S'.rightHom (f e))))⁻¹ * S.rightHom e = 1

Tactic:
← MonoidHom.comp_apply,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ (S.rightHom (Function.surjInv ⋯ ((S'.rightHom.comp f) e)))⁻¹ * S.rightHom e = 1
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
n : N
hn : S.inl n = (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e
⊢ S.inl (Function.invFun (⇑S'.inl) (f (S.inl n))) = S.inl n

Tactic:
← MonoidHom.comp_apply,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
n : N
hn : S.inl n = (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e
⊢ S.inl (Function.invFun (⇑S'.inl) ((f.comp S.inl) n)) = S.inl n
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ f (S.inl (Function.invFun (⇑S'.inl) ((f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e'))) =
    (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e'

Tactic:
← MonoidHom.comp_apply,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (f.comp S.inl) (Function.invFun (⇑S'.inl) ((f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e')) =
    (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e'
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (S'.rightHom (f (Function.surjInv ⋯ (S'.rightHom e'))))⁻¹ * S'.rightHom e' = 1

Tactic:
← MonoidHom.comp_apply,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ ((S'.rightHom.comp f) (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * S'.rightHom e' = 1
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
⊢ (unitsSMulGroup φ d u g).2 = (⋯.equiv g).2

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl <;> rfl

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ (f.noncommCoprod g comm) mn = f mn.1 * g mn.2

Tactic:
noncommCoprod_apply

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ f mn.1 * g mn.2 = f mn.1 * g mn.2
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ (g ^ j) x ∈ (↑c).support

Tactic:
exact zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff.mpr hc

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑(σ * τ) c)) = a.ofPermHomFun σ ((g ^ m) (a (↑τ c)))

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a _ _ rfl]

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑(σ * τ) c)) = (g ^ m) (a (↑σ (↑τ c)))

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑τ c)) ∈ (↑(↑τ c)).support