mathlib-initiative/mathlib-tactics huggingface dataset:
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 →* Mˣ)

Tactic:
Nat.card_congr (domRestrictHomKerEquiv Mˣ H).toEquiv

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 (G ⧸ H →* Mˣ) = Nat.card (G ⧸ H →* Mˣ)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ (1 + ⟨q, ↑(-1) + ↑k.cast⟩.snd.cast) * Quotient.out (Quotient.out ⟨q, ↑(-1) + ↑k.cast⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
Int.cast_neg,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ (1 + ⟨q, -↑1 + ↑k.cast⟩.snd.cast) * Quotient.out (Quotient.out ⟨q, -↑1 + ↑k.cast⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ closure ↑S ≤ f.range

Tactic:
closure_le

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ ↑S ⊆ ↑f.range
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H

Tactic:
closure_le

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S) ⊆ ↑H
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
hN : N.IsFinitelyNormallyGenerated
f : G →* H
hf : Surjective ⇑f
hf' : f.ker.IsFinitelyNormallyGenerated
⊢ (comap f N).IsFinitelyNormallyGenerated

Tactic:
obtain ⟨S, hS_fin, hS⟩ := hN

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
hf' : f.ker.IsFinitelyNormallyGenerated
S : Set H
hS_fin : S.Finite
hS : normalClosure S = N
⊢ (comap f N).IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ≤ H

Tactic:
closure_le

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑H
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ≤ _root_.commutator G

Tactic:
closure_le

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑(_root_.commutator G)
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ (g⁻¹ * h * g)⁻¹ * h ∈ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}

Tactic:
exact ⟨H.mul_mem (H.inv_mem hconj) hh, _, H.inv_mem hconj, g, by group⟩

Goal state after:
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 ↥↑P).totient

Tactic:
hk,

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 ^ k).totient
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr
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 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card ↥↑P).totient

Tactic:
hk,

Goal state after:
case neg.inr
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 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac ^ k).totient
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
· rintro ⟨n, H, hH, hn⟩
    refine ⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
    dsimp only
    rw [tsub_self]
    exact hH.1

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
rcases h with ⟨n, hn⟩
  use n
  apply eq_top_iff.mpr
  calc
    ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G ≤ 1 ↔ IsMulCommutative G

Tactic:
rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : IsNilpotent G
⊢ ⊥ ≠ center G

Tactic:
simpa using mt (upperCentralSeries.eq_top zero_ne_one) <| by simp

Goal state after:
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
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ⊤.lowerCentralSeries (max (nilpotencyClass G₁) (nilpotencyClass G₂)) = ⊥

Tactic:
rw [top_lowerCentralSeries_prod,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]

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
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (g • B) (s • B)

Tactic:
rw [← iUnion_smul_set, disjoint_iUnion₂_right]

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ i ∈ s, Disjoint (g • B) (i • B)
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
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B

Tactic:
refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩
  simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢
  exact hB 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
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ g ∈ H

Tactic:
← mul_mem_cancel_left h₂⁻¹.2,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ ↑h₂⁻¹ * g ∈ H
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
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
let B := ⋂ (g : G) (_ : a ∈ g • A), g • A

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
⊢ ∃ 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 α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})

Tactic:
have h_nodup := hg3.nodup_iff_mem_support.mpr ha

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
⊢ 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 α
H : Type u_3
β : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective ⇑f
y : ι ↪ β
g : β → α
left✝ : LeftInverse g ⇑f
hfg : RightInverse g ⇑f
⊢ ∃ a, (Injective.mulActionHom_embedding ι ⋯) a = y

Tactic:
use ⟨g ∘ y, hfg.injective.comp (EmbeddingLike.injective y)⟩

Goal state after:
case h
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 : Bijective ⇑f
y : ι ↪ β
g : β → α
left✝ : LeftInverse g ⇑f
hfg : RightInverse g ⇑f
⊢ (Injective.mulActionHom_embedding ι ⋯) { toFun := g ∘ ⇑y, inj' := ⋯ } = y
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: 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 α
⊢ Nontrivial α

Tactic:
rw [← ENat.one_lt_card_iff_nontrivial]

Goal state after:
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 α
⊢ 1 < ENat.card α
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: 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
⊢ Nontrivial ↥(ofStabilizer G a)

Tactic:
rw [← ENat.one_lt_card_iff_nontrivial]

Goal state after:
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
⊢ 1 < ENat.card ↥(ofStabilizer G a)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
⊢ k ∈ G

Tactic:
let x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq rfl).symm.toEmbedding

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
⊢ k ∈ G
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : Function.Surjective toPerm
⊢ IsPreprimitive ↥(stabilizer M s) ↑s

Tactic:
by
  let φ : stabilizer M s → Perm s := toPerm
  let f : s →ₑ[φ] s := {
    toFun := id
    map_smul' _ _ := rfl }
  have hf : Function.Bijective f := Function.bijective_id
  rw [isPreprimitive_congr hs hf]
  infer_instance

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

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = Set.univ
⊢ B.Subsingleton

Tactic:
have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)
      subst hBs'
      obtain ⟨g', hg', hg's⟩ := SetLike.exists_of_lt hG
      have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's
      suffices (g' • B).Subsingleton by
        exact subsingleton_of_image (MulAction.injective g') B this
      apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)
      exact Disjoint.subset_compl_right h

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 α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this✝ : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ B = univ

Tactic:
by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ Nontrivial α

Tactic:
rw [← Finite.one_lt_card_iff_nontrivial]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ 1 < Nat.card α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g +ᵥ a = a
⊢ AddAction.toPerm g = AddAction.toPerm 0

Tactic:
AddAction.toPerm_zero,

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g +ᵥ a = a
⊢ AddAction.toPerm g = 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
k : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • x = y

Tactic:
hk,

Goal state after:
case h
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
k : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • k • a = y
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
suffices ∀ x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ),
      ∃ k : fixingSubgroup G ((↑g.support : Set α)ᶜ), x = k • a by
    rw [isPretransitive_iff]
    rintro ⟨x, hx⟩ ⟨y, hy⟩
    obtain ⟨k, hk⟩ := this x hx
    obtain ⟨k', hk'⟩ := this y hy
    use k' * k⁻¹
    rw [← SetLike.coe_eq_coe]
    simp only [SetLike.mk_smul_mk]
    rw [hk, hk', smul_smul, inv_mul_cancel_right]

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
⊢ ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
⊢ G = ⊤

Tactic:
obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3

Goal state after:
case inr
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
⊢ G = ⊤
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case nil
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
ofGroup : (g : G) → motive (NormalWord.ofGroup g)
cons :
  (g : G) →
    (u : ℤˣ) →
      (w : NormalWord d) →
        (h1 : w.head ∈ d.set u) →
          (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') →
            motive w → motive (NormalWord.cons g u w h1 h2)
g : G
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []
mem_set : ∀ (u : ℤˣ) (g_1 : G), (u, g_1) ∈ { head := g, toList := [], chain := chain }.toList → g_1 ∈ d.set u
⊢ motive { head := g, toList := [], chain := chain, mem_set := mem_set }

Tactic:
exact ofGroup _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∈ Function.fixedPoints ⇑g ∨ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
by
  rw [Classical.or_iff_not_imp_left]
  intro hx
  rw [Function.mem_fixedPoints_iff, ← ne_eq, ← mem_support,
    ← cycleOf_mem_cycleFactorsFinset_iff] at hx
  refine ⟨⟨g.cycleOf x, hx⟩, ?_, (a.sameCycle hx)⟩
  rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]
  simp [SameCycle.rfl, hx, and_self]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ #(a.ofPermHom τ).support = ∑ c ∈ (↑τ).support, #(↑c).support

Tactic:
rw [ofPermHom_support, Finset.card_biUnion]
  intro c _ d _ h
  apply Equiv.Perm.Disjoint.disjoint_support
  apply g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr h)

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op 1⁻¹ • α) T = T

Tactic:
by rw [inv_one]; apply one_smul Gᵐᵒᵖ T

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card ↑(Function.fixedPoints ⇑g))! * Fintype.card ((c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
Fintype.card_pi,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card ↑(Function.fixedPoints ⇑g))! * ∏ i, Fintype.card ↥(zpowers ↑i) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
⊢ k ^ 2 = 1

Tactic:
hk,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
⊢ a.toCentralizer ⟨τ, hτ⟩ ^ 2 = 1