mathlib-initiative/mathlib-tactics huggingface dataset:
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:
refine ⟨fun a b h ↦ Finset.singleton_injective congr($h.1), fun ⟨s, hs⟩ ↦ ?_⟩

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
x✝ : ↑(powersetCard α 1)
s : Finset α
hs : s ∈ powersetCard α 1
⊢ ∃ a, (mulActionHom_singleton G α) a = ⟨s, hs⟩
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : Nat.card α < n
⊢ 0 ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hP : IsPerfect G
g : G
⊢ g ∈ _root_.commutator G

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
⊢ derivedSeries G 0 = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n : ℕ
⊢ H.lowerCentralSeries 0 = H

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs

Goal state before:
pp: M : Type u_1
G : Type u_2
H : Type u_3
inst✝² : CommMonoid M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : ⊤.LocalizationMap G
g : ⊤.LocalizationMap H
s : Submonoid G
x✝ : M × M
⊢ x✝ ∈ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) ↔ x✝ ∈ divPairs f s

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ (fun x1 x2 ↦ x1 * x2) (inr (ofAdd 1)) (inl ↑a) = inr (ofAdd 1) * inl ↑a ∧
    (fun x1 x2 ↦ x1 * x2) (inl ↑(φ a)) (inr (ofAdd 1)) = inl ↑(φ a) * inr (ofAdd 1)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑b * t = of ↑(φ (φ.symm b)) * t

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑(φ a) = of ↑(φ a) * t * t⁻¹

Tactic:
simp

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
⊢ finrank ℤ ↥A = finrank ℤ ↥B

Tactic:
have : (A.addSubgroupOf B).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_addSubgroupOf
  rw [← finrank_eq_of_finiteIndex (A.addSubgroupOf B)]
  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
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * (t * of ↑(φ.symm b))

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = t⁻¹ * of ↑b * t * t⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = of ↑(φ.symm b) * t⁻¹

Tactic:
rw [equiv_symm_eq_conj]; simp

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsSimpleGroup G
⊢ ⊤.Normal

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

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

Tactic:
simp

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 : ℤˣ) (g : G), (u, g) ∈ [] → g ∈ d.set u

Tactic:
simp

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
g : G
⊢ ∀ (u : ℤˣ) (g : G), (u, g) ∈ [] → g ∈ d.set u

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
hN : ⊤.IsSubnormal
⊢ ⊤ = ⊤ ∨ ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (i : ℕ), (⊤.subgroupOf ⊤).Normal

Tactic:
simp

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
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
⊢ ((↑g'.2 * w.head⁻¹) • w).head ∈ d.set u

Tactic:
simp

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
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
⊢ ∀ u' ∈ Option.map Prod.fst ((↑g'.2 * w.head⁻¹) • w).toList.head?,
    ((↑g'.2 * w.head⁻¹) • w).head ∈ toSubgroup A B u → u = u'

Tactic:
simp only [g', group_smul_toList, Option.mem_def, Option.map_eq_some_iff, Prod.exists,
          exists_and_right, exists_eq_right, group_smul_head, inv_mul_cancel_right,
          forall_exists_index, unitsSMulGroup]

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
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
⊢ ∀ (u' : ℤˣ) (x : G), w.toList.head? = some (u', x) → ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u → u = u'
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
⊢ (comap f ⊤).IsSubnormal

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
x : M
⊢ ((f.noncommCoprod g comm).comp (inl M N)) x = f x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
x : N
⊢ ((f.noncommCoprod g comm).comp (inr M N)) x = g x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
Q : Type u_4
inst✝ : Monoid Q
h : P →* Q
x : M × N
⊢ (h.comp (f.noncommCoprod g comm)) x = ((h.comp f).noncommCoprod (h.comp g) ⋯) x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
⊢ mk (stabilizerEquiv_invFun_aux g) ∈ stabilizer (Perm α)ᵈᵐᵃ f

Tactic:
ext a
    rw [smul_apply, symm_apply_apply, Perm.smul_def]
    apply comp_stabilizerEquiv_invFun

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.left.a
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : u ∈ c.ranges
ht : klift' u ⋯ ∈ l
⊢ u.Nodup

Tactic:
exact ranges_nodup hu

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case e'_7
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
w : NormalWord d
⊢ 1 = - -1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
a : α
⊢ f a ∈ ↑(Finset.image f Finset.univ)

Tactic:
simp

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

Goal state before:
pp: case i_surj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ b ∈ Finset.image f Finset.univ, ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = b

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ (fixedBy α 1)ᶜ.Finite

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ ∀ x ∈ closure S, (fixedBy α x)ᶜ.Finite → (fixedBy α x⁻¹)ᶜ.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inv
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x y : α
⊢ {x, y}.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons.h1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).head = (cons g u w h1 h2).head

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case h2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).toList[i✝]? = some a✝ ↔ (cons g u w h1 h2).toList[i✝]? = some a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ 1 ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}

Tactic:
simp

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
w : NormalWord d
⊢ (fun g ↦ g • empty) ((fun w ↦ ReducedWord.prod φ w.toReducedWord) w) = w

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ↑(x✝⁻¹ ⟨c, hc⟩) ∈ g.cycleFactorsFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ #(↑(x✝ ⟨↑(x✝⁻¹ ⟨c, hc⟩), ⋯⟩)).support = #c.support

Tactic:
simp

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
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []
⊢ ∀ (u : ℤˣ) (g : G), (u, g) ∈ [] → g ∈ d.set u

Tactic:
simp

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
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []
⊢ ReducedWord.prod φ { head := 1, toList := [], chain := ⋯, mem_set := ⋯ }.toReducedWord =
      ReducedWord.prod φ { head := 1, toList := [], chain := chain } ∧
    List.map Prod.fst { head := 1, toList := [], chain := ⋯, mem_set := ⋯ }.toList =
        List.map Prod.fst { head := 1, toList := [], chain := chain }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := [], chain := chain }.toList.head?,
        { head := 1, toList := [], chain := ⋯, mem_set := ⋯ }.head ∈ toSubgroup A B (-u)

Tactic:
simp

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)
x : α
c : ↥g.cycleFactorsFinset
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, m, hm⟩)
  · simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx]
    suffices ∀ (d : g.cycleFactorsFinset), x ∉ (d : Perm α).support by
      simp only [this]
    intro d hx'
    rw [Function.mem_fixedPoints_iff, ← notMem_support] at hx
    apply hx
    exact mem_cycleFactorsFinset_support_le d.prop hx'
  · rw [ofPermHomFun_apply_of_cycleOf_mem a τ hd hm] --
    rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]
    by_cases h : c = d
    · simp only [h, hd, mem_support_self]
    · have H : Disjoint c.val d.val :=
        cycleFactorsFinset_pairwise_disjoint g c.prop d.prop (Subtype.coe_ne_coe.mpr h)
      have H' : Disjoint ((τ : Perm g.cycleFactorsFinset) c : Perm α)
        ((τ : Perm g.cycleFactorsFinset) d : Perm α) :=
        cycleFactorsFinset_pairwise_disjoint g ((τ : Perm g.cycleFactorsFinset) c).prop
          ((τ : Perm g.cycleFactorsFinset) d).prop (by
          intro h'; apply h
          simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h')
      rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'
      simp only [H hd, H' (mem_support_self a _)]

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:
by
  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.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (1 * a).left x✝ = a.left x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (1 * a).right = a.right

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a * 1).left x✝ = a.left x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a * 1).right = a.right

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a⁻¹ * a).left x✝ = left 1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a⁻¹ * a).right = right 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝² x✝¹ x✝ : Q
⊢ { left := 1, right := x✝² * x✝¹ }.left x✝ = ({ left := 1, right := x✝² } * { left := 1, right := x✝¹ }).left x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ }.right = ({ left := 1, right := x✝¹ } * { left := 1, right := x✝ }).right

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝ : Q
⊢ (rightHom.comp inl) x✝ = (MonoidHom.id Q) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
q : Q
⊢ rightHom (inl q) = q

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
x✝ : Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
          ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).left
      x✝ =
    x.left x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
        ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).right =
    x.right

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
x✝ : Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
          ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).left
      x✝ =
    x.left x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
        ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).right =
    x.right

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
x✝ : Q₂
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.left x✝ =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).left
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.right =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } *
        { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).right

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
Λ : Type u_3
inst✝ : MulAction D Λ
⊢ ∀ (b : Λ × Q), 1 • b = b

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite (IteratedWreathProduct G 0)

Tactic:
IteratedWreathProduct_zero

Goal state after:
case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite PUnit.{u + 1}
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Nat.card (IteratedWreathProduct G 0) = Nat.card G ^ ∑ i ∈ Finset.range 0, Nat.card G ^ i

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group (IteratedWreathProduct G 0)

Tactic:
IteratedWreathProduct_zero

Goal state after:
case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group PUnit.{u + 1}
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
constructor
  · rintro ⟨k, rfl⟩ c
    rw [coe_toPermHom, Equiv.Perm.support_conj]
    apply Finset.card_map
  · obtain ⟨a⟩ := Basis.nonempty g
    exact fun hτ ↦ ⟨toCentralizer a ⟨τ, hτ⟩, toPermHom_apply_toCentralizer a ⟨τ, hτ⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : (-1) ^ (m.sum + m.card) = 1
⊢ -1 ≠ 1

Tactic:
simp

Goal state after: