mathlib-initiative/mathlib-tactics huggingface dataset:
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
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'
⊢ ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩ → B ⊆ B'

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:
· rintro hBB' b hb
      obtain ⟨k, rfl⟩ := htGX.exists_smul_eq a b
      suffices k ∈ stabilizer G B' by
        exact this.symm ▸ (Set.smul_mem_smul_set ha')
      exact hBB' (hB.smul_eq_of_mem ha hb)

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'
⊢ B ⊆ B' → ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ (ConjAct.ofConjAct k⁻¹) a✝ ∈ g.support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support

Tactic:
← Perm.smul_def,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ ConjAct.ofConjAct k⁻¹ • a✝ ∈ g.support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

Tactic:
← isSimpleOrder_blockMem_iff_isPreprimitive G a,

Goal state after:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom (stabilizer G a) ↔ IsSimpleOrder (BlockMem G a)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ ↑(⟨π * swap a b, ⋯⟩ * ⟨σ, hσ✝⟩ * ⟨π * swap a b, ⋯⟩⁻¹) = ↑⟨τ, hτ⟩

Tactic:
· simp only [← hπ, Subgroup.coe_mul]
      have hd : Disjoint (swap a b) σ := by
        rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
          Finset.disjoint_singleton_left]
        exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
      simp [mul_assoc, hd.commute.eq]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite α
hs : s.ncard + n ≤ Nat.card α
⊢ ∃ y, Disjoint s (range ⇑y)

Tactic:
apply exists_embedding_disjoint_range_of_add_le_ENat_card

Goal state after:
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite α
hs : s.ncard + n ≤ Nat.card α
⊢ ↑s.ncard + ↑n ≤ ENat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a.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
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap a (g a) * swap b c ∈ closure {g | g.cycleType = {2, 2}}

Tactic:
apply Subgroup.subset_closure

Goal state after:
case a.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
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap a (g a) * swap b c ∈ {g | g.cycleType = {2, 2}}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a.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
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap b c * swap (g a) (g (g a)) ∈ closure {g | g.cycleType = {2, 2}}

Tactic:
apply Subgroup.subset_closure

Goal state after:
case a.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
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap b c * swap (g a) (g (g a)) ∈ {g | g.cycleType = {2, 2}}
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:
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:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ IsMultiplyPretransitive G α 1

Tactic:
apply isMultiplyPretransitive_of_le (n := k + 1)

Goal state after:
case hmn
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ 1 ≤ k + 1

case hα
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ k + 1 ≤ Nat.card α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Bijective ⇑(ofFixingSubgroup_insert_map a s)

Tactic:
by
  constructor
  · rintro ⟨x, hx⟩ ⟨y, hy⟩ h
    simpa only [← Subtype.coe_inj, ofFixingSubgroup_insert_map_apply] using h
  · rintro ⟨⟨x, hx1⟩, hx2⟩
    exact ⟨⟨x, mem_ofFixingSubgroup_insert_iff.mpr ⟨hx1, hx2⟩⟩, rfl⟩

Goal state after:
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 α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
⊢ IsPreprimitive ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')

Tactic:
let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s'

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
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
⊢ IsPreprimitive ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')
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 ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
⊢ k = ↑g

Tactic:
have hgk (i : Fin (Fintype.card α)) : (g • x) i = (k • x) i := by
    rcases lt_or_eq_of_le (le_sub_one_of_lt i.prop) with hi | hi
    · exact hgk' i hi
    · obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
      rcases lt_or_eq_of_le (le_sub_one_of_lt j.prop) with hj | hj
      · suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
        apply EmbeddingLike.injective (g • x)
        rw [hgk' j hj, hxj]
      · rw [← hxj]
        apply congr_arg
        rw [Fin.ext_iff, hi, hj]

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
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
⊢ 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
⊢ B.Subsingleton

Tactic:
rw [← inter_eq_self_of_subset_right (subset_of_ssubset hB_ss_sc), ← Subtype.image_preimage_val]
  apply Set.Subsingleton.image
  suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set (s : Set α)) by
    apply Or.resolve_right this
    rw [preimage_eq_univ_iff, Subtype.range_coe_subtype]
    exact not_subset_of_ssubset hB_ss_sc
  suffices IsPreprimitive (stabilizer M (s : Set α)) (s : Set α) by
    apply this.isTrivialBlock_of_isBlock
    let φ' : stabilizer M (s : Set α) → M := Subtype.val
    let f' : (s : Set α) →ₑ[φ'] α := {
      toFun := Subtype.val
      map_smul' _ _ := rfl }
    exact hB.preimage f'
  exact isPreprimitive_stabilizer_of_surjective _ hG

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

Goal state before:
pp: case hn
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
⊢ 1 ≤ 1

Tactic:
· norm_num

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 α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
rw [Subsingleton.eq_singleton_of_mem h1 ha, stabilizer_singleton]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h1 : s.Subsingleton
this : Nontrivial α
a : α
ha : a ∈ s
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) a)
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
σ : S.Section
g₁ g₂ : G
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

Tactic:
obtain ⟨n, hn⟩ := mul_mul_mul_inv_mem_range_inl σ g₁ g₂
  use n⁻¹
  rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
⊢ Function.Bijective ⇑(mulActionHom_singleton G α)

Tactic:
by
  refine ⟨fun a b h ↦ Finset.singleton_injective congr($h.1), fun ⟨s, hs⟩ ↦ ?_⟩
  obtain ⟨a, rfl⟩ := card_eq_one.mp hs
  exact ⟨a, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
n : ℕ
⊢ (nsmulAddMonoidHom n).range.index = (nsmulAddMonoidHom n).range.index

Tactic:
simpa [AddEquiv.map_range_nsmulAddMonoidHom]
        using (index_map_equiv (nsmulAddMonoidHom (α := M) n).range
                (Module.finBasis ℤ M).equivFun.toAddEquiv).symm

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
obtain rfl | hH := eq_or_ne H ⊤

Goal state after:
case step.inl.inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hS : ⊤.IsSubnormal
HK : ⊤ ≤ ⊤
hN : (⊤.subgroupOf ⊤).Normal
⊢ ⊤ = ⊤ ∨ ∃ K, ⊤ < K ∧ K.IsSubnormal ∧ (⊤.subgroupOf K).Normal

case step.inl.inr
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
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
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ¬Cancels u w

Tactic:
simp only [Cancels, Option.map_eq_some_iff, Prod.exists,
    exists_and_right, exists_eq_right, not_and, not_exists]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ w',
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : ¬w.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
· rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩
      exact ⟨w.head • w', by
        simpa [ReducedWord.prod, mul_assoc] using hw'⟩

Goal state after:
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
w : ReducedWord G A B
⊢ ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ w',
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)

Tactic:
intro w hw1

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w✝ w : ReducedWord G A B
hw1 : w.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
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
⊢ ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S

Tactic:
apply fin.induction_on ..

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
⊢ ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ ∅ → f ∈ closure S

α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
⊢ ∀ {a : α} {s : Set α},
    a ∉ s →
      s.Finite →
        (∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S) →
          ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ insert a s → f ∈ closure S
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 : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
by
  have hx' : c = g.cycleOf x := cycle_is_cycleOf hx (Subtype.prop c)
  have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset := hx' ▸ c.prop
  set n := Nat.find (a.sameCycle hx'').exists_nat_pow_eq
  have hn : (g ^ (n : ℤ)) (a c) = x := by
    rw [← Nat.find_spec (a.sameCycle hx'').exists_nat_pow_eq, zpow_natCast]
    congr
    rw [← Subtype.coe_inj, hx']
  suffices ofPermHomFun a τ x = (g ^ (n : ℤ)) (a ((τ : Perm g.cycleFactorsFinset) c)) by
    rw [this, IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset ((τ : Perm g.cycleFactorsFinset) c).prop)
      (mem_support_self a ((τ : Perm g.cycleFactorsFinset) c))]
    simp only [τ.prop c]
    rw [← IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset c.prop) (mem_support_self a c)]
    rw [hn, hm]
  simp only [ofPermHomFun, dif_pos hx'']
  congr
  exact hx'.symm

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ⊔ (noncommPiCoprod ⋯).range ≤ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
sup_le_iff,

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    (noncommPiCoprod ⋯).range ≤ map (centralizer {g}).subtype (toPermHom g).ker
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range = map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
apply le_antisymm
  · rw [kerParam, MonoidHom.noncommCoprod_range, sup_le_iff, noncommPiCoprod_range, iSup_le_iff]
    simp only [zpowers_le]
    constructor
    · rintro - ⟨a, rfl⟩
      refine ⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩
      · rw [mem_centralizer_singleton_iff]
        exact Disjoint.commute (disjoint_iff_disjoint_support.mpr (ofSubtype_support_disjoint a))
      · exact Perm.ext fun x ↦ Subtype.ext (disjoint_iff_disjoint_support.mpr
          ((ofSubtype_support_disjoint a).mono_right
            (mem_cycleFactorsFinset_support_le x.2))).commute.mul_inv_cancel
    · intro i
      refine ⟨⟨i, mem_centralizer_singleton_iff.mpr (self_mem_cycle_factors_commute i.2)⟩, ?_, rfl⟩
      exact Perm.ext fun x ↦ Subtype.ext (cycleFactorsFinset_mem_commute' g i.2 x.2).mul_inv_cancel
  · rintro - ⟨p, hp, rfl⟩
    simp only [coe_subtype]
    set u : Perm (Function.fixedPoints g) :=
      subtypePerm p (fun x ↦ apply_mem_fixedPoints_iff_mem_of_mem_centralizer p.2)
    simp only [SetLike.mem_coe, mem_ker_toPermHom_iff, IsCycle.forall_commute_iff] at hp
    set v : (c : g.cycleFactorsFinset) → (Subgroup.zpowers c.val) :=
      fun c => ⟨ofSubtype
          (p.1.subtypePerm (Classical.choose (hp c.val c.prop))),
            Classical.choose_spec (hp c.val c.prop)⟩
    use (u, v)
    ext x
    rw [kerParam_apply]
    split_ifs with hx
    · rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support] at hx
      rw [ofSubtype_apply_of_mem, subtypePerm_apply]
      rwa [mem_support, cycleOf_apply_self, ne_eq]
    · rw [cycleOf_mem_cycleFactorsFinset_iff, notMem_support] at hx
      rwa [ofSubtype_apply_of_mem, subtypePerm_apply]

Goal state after:
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τ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
⊢ (↑k).cycleType.card * 2 = #(↑k).support

Tactic:
rw [← sum_cycleType, hk_cT]

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τ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
⊢ (Multiset.replicate (↑k).cycleType.card 2).card * 2 = (Multiset.replicate (↑k).cycleType.card 2).sum
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ (base φ) h • w = h • w

Tactic:
base_smul_def,

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ { toWord := w.toWord, head := h * w.head, normalized := ⋯ } = h • w
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ g ∈ Subgroup.closure (commutatorSet ↥(alternatingGroup α))

Tactic:
apply Subgroup.subset_closure

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ g ∈ commutatorSet ↥(alternatingGroup α)