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✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ (cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i')) ^ M.M i i' = 1

Tactic:
rw [← map_mul, ← map_pow]

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✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i') = 1
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case mul_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
i : W
mi : i ∈ Set.range cs.simple
y : W
my : y ∈ Submonoid.closure (Set.range cs.simple)
ih : p y
⊢ p (i * y)

Tactic:
| mul_left i mi y my ih =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ ⟨j, m⟩ ∈ (rcons p).toList ↔ ⟨j, m⟩ ∈ p.tail.toList ∨ m ≠ 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Tactic:
simp only [rcons, cons, ne_eq]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head
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
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length (w * cs.simple i) % 2 = (cs.length w + cs.length (cs.simple i)) % 2
⊢ False

Tactic:
eq,

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
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + cs.length (cs.simple i)) % 2
⊢ False
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ s * {a} * t = Set.image2 (fun x1 x2 ↦ x1 * a * x2) s t

Tactic:
Set.mul_singleton,

Goal state after:
α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ (fun x ↦ x * a) '' s * t = Set.image2 (fun x1 x2 ↦ x1 * a * x2) s t
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) → a⁻¹ * b ∈ H

Tactic:
rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
    rwa [one_mul, inv_mul_cancel_left]

Goal state after:
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 / Nat.card ↥H

Tactic:
H.card_eq_card_quotient_mul_card_subgroup,

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) * Nat.card ↥H / Nat.card ↥H
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : 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 : ℤ
h1n : 1 ≤ n
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

Tactic:
induction n, h1n using Int.leInduction with

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative ↥↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
replace hg := P.pow_mem hg k

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative ↥↑P
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case h₂
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))

Tactic:
· rwa [conj_conjugator_reduceCyclically]

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
exact (((QuotientGroup.mk' I.goursatFst).prodMap
    (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).exists_mulEquiv_range_eq_graph
    ((QuotientGroup.mk'_surjective _).comp hI₁) ((QuotientGroup.mk'_surjective _).comp hI₂)
    fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ mk_goursatFst_eq_iff_mk_goursatSnd_eq hI₁ hI₂ hx hy

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
this : ∀ (p : ↥ps) (P : Sylow (↑p) G), IsNilpotent ↥↑P
⊢ IsNilpotent G

Tactic:
exact nilpotent_of_mulEquiv e

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

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : {a} = univ
b : X
hb : b ≠ a
⊢ b = a

Tactic:
← Set.mem_singleton_iff,

Goal state after:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : {a} = univ
b : X
hb : b ≠ a
⊢ b ∈ {a}
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : B.ncard * 0 = Nat.card X
⊢ B = Set.univ

Tactic:
rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key

Goal state after:
case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : IsEmpty X
⊢ B = Set.univ
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
⊢ Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α

Tactic:
let := Fintype.ofFinite α

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
simpa [Nat.lt_succ_iff] using this

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G b)
⊢ ∃ a_1, (conjMap hg) a_1 = x

Tactic:
exact ⟨conjMap _ x, inv_conjMap_comp_apply _ x⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case h.inl
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
H : ∀ (i : Fin n), (Fin.Embedding.init (g • x)) i ∈ ofStabilizer G a
i : Fin n
⊢ (g • x) i.castSucc = (ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a)) (Fin.Embedding.init (g • x)) H)) i.castSucc

pp: case h.inr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
H : ∀ (i : Fin n), (Fin.Embedding.init (g • x)) i ∈ ofStabilizer G a
⊢ (g • x) (Fin.last n) =
    (ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a)) (Fin.Embedding.init (g • x)) H)) (Fin.last n)

Tactic:
· simpa [ofStabilizer.snoc] using!
      Subtype.ext_iff.mp <| Function.Embedding.codRestrict_apply _ _ H i

Goal state after:
case h.inr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
H : ∀ (i : Fin n), (Fin.Embedding.init (g • x)) i ∈ ofStabilizer G a
⊢ (g • x) (Fin.last n) =
    (ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a)) (Fin.Embedding.init (g • x)) H)) (Fin.last n)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind : ∀ (n : ℕ) (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hσ : l.prod ∈ alternatingGroup α
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ ∀ g ∈ l_1, g.IsSwap }
n : ℕ
hn : l.length = n + n
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
rw [← two_mul] at hn

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind : ∀ (n : ℕ) (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hσ : l.prod ∈ alternatingGroup α
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ ∀ g ∈ l_1, g.IsSwap }
n : ℕ
hn : l.length = 2 * n
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
suffices hg' : orderOf g' ∣ 2 by
    rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
    exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq

Goal state after:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ orderOf g' ∣ 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3

Tactic:
rw [← not_lt]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
⊢ ¬3 < Nat.card α
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ m • a = c

Tactic:
by rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
m n : ℕ
inst✝¹ : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : n ≤ Nat.card α
inst✝ : Finite α
⊢ IsMultiplyPretransitive G α m

Tactic:
by
  obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact IsPretransitive.of_surjective_map (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_natCard hα) inferInstance

Goal state after:
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 α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : ¬s ∪ g • s = Set.univ
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
← Set.compl_empty_iff,

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : ¬(s ∪ g • s)ᶜ = ∅
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ ofFixingSubgroup M s
⊢ (match ⟨m, hm⟩ • ⟨x, hx⟩ with
    | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩) =
    φ' ⟨m, hm⟩ •
      match ⟨x, hx⟩ with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩

Tactic:
rw [← SetLike.coe_eq_coe]
          exact f.map_smul' m x

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
x : α
hx : x ∈ s
⊢ k • x = x

Tactic:
Perm.smul_def,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
x : α
hx : x ∈ s
⊢ k x = x
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
have := isPretransitive_of_isCycle_mem h3g.isCycle hg

Goal state after:
case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
⊢ IsPerfect ↥f.range

Tactic:
by
  rw [MonoidHom.range_eq_map]
  exact IsPerfect.map _

Goal state after:
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
A B : AddSubgroup M
inst✝² : Module.Finite ℤ ↥B
inst✝¹ : IsTorsionFree ℤ ↥B
h : A ≤ B
inst✝ : A.IsFiniteRelIndex B
this : (A.addSubgroupOf B).FiniteIndex
⊢ finrank ℤ ↥A = finrank ℤ ↥(A.addSubgroupOf B)

Tactic:
exact (addSubgroupOfEquivOfLe h).symm.toIntLinearEquiv.finrank_eq

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
⊢ ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u → u = u'

Tactic:
hmem

Goal state after:
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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
⊢ u = u'
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hw : w.head ∈ toSubgroup A B u
x : G
h2 : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
hx : w.toList.head? = some (-u, x)
⊢ False

Tactic:
simpa using h2 (-u) rfl hw

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u)
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯)
      hcan =
    w

Tactic:
simp only [dif_neg hncan]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u)
      (cons (↑(unitsSMulGroup φ d u w.head).1) u ((↑(unitsSMulGroup φ d u w.head).2 * w.head⁻¹) • w) ⋯ ⋯) ⋯ =
    w
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ Function.Injective ⇑(f.noncommCoprod g comm) ↔
    Function.Injective ⇑f ∧ Function.Injective ⇑g ∧ Disjoint f.range g.range

Tactic:
simp only [injective_iff_map_eq_one, disjoint_iff_inf_le,
    noncommCoprod_apply, Prod.forall, Prod.mk_eq_one]
  refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
  · simpa using h x 1
  · simpa using h 1 x
  · intro x ⟨⟨y, hy⟩, z, hz⟩
    rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy
  · intro ⟨hf, hg, hp⟩ a b h
    have key := hp ⟨⟨a⁻¹, by rwa [map_inv, inv_eq_iff_mul_eq_one]⟩, b, rfl⟩
    exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
⊢ 1 • c = c

Tactic:
by
    rw [← Subtype.coe_inj]
    change ConjAct.toConjAct (1 : Perm α) • c.val = c
    simp only [map_one, one_smul]

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

Goal state before:
pp: case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : Equiv.swap z w ∈ S
hσa : Equiv.swap z w • a ∉ {x | Equiv.swap x y ∈ closure S}
this : a ≠ Equiv.swap z w • a
⊢ False

Tactic:
Perm.smul_def,

Goal state after:
case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : Equiv.swap z w ∈ S
hσa : Equiv.swap z w • a ∉ {x | Equiv.swap x y ∈ closure S}
this : a ≠ (Equiv.swap z w) a
⊢ False
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ (Equiv.swap (f a) a * f) • b = b

Tactic:
Perm.smul_def,

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ (Equiv.swap (f a) a * f) b = b
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ τ ∈ (toPermHom g).range → ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support

pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) → τ ∈ (toPermHom g).range

Tactic:
· rintro ⟨k, rfl⟩ c
    rw [coe_toPermHom, Equiv.Perm.support_conj]
    apply Finset.card_map

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) → τ ∈ (toPermHom g).range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
⊢ False

Tactic:
obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
a b : ↑(Function.fixedPoints ⇑g)
hab : a ≠ b
⊢ False