mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
⊢ a ∉ s ∪ g • s

Tactic:
simp only [Set.smul_set_compl, Set.mem_compl_iff] at hga ha

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
hga : a ∉ g • s
ha : a ∉ s
⊢ a ∉ s ∪ g • s
Module: Mathlib.GroupTheory.GroupAction.OfQuotient

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : MulAction G A
H : Subgroup G
inst✝ : H.Normal
g : G ⧸ H
a : ↑(fixedPoints (↥H) A)
⊢ Quotient.out g • a = g • a

Tactic:
by
  conv_rhs => rw [← g.out_eq]
  rfl

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

Goal state before:
pp: case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := ⋯
ha : a ∉ s ∪ g • s
⊢ s ∪ g • s ≠ Set.univ

Tactic:
· exact fun h ↦ ha (by rw [h]; trivial)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
g : Perm ↑sᶜ
⊢ sᶜᶜ.Nontrivial

Tactic:
rwa [compl_compl]

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ sᶜ.ncard < sᶜᶜ.ncard

Tactic:
rwa [compl_compl]

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

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

Tactic:
map_mul,

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

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

Tactic:
map_mul,

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

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ S.rightHom (e * (s (S.rightHom e))⁻¹) = 1

Tactic:
map_mul,

Goal state after:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ S.rightHom e * S.rightHom (s (S.rightHom e))⁻¹ = 1
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * f (↑(x (n i)).2 * ↑(∏ x_1 ∈ univ.erase i, (x (n x_1)).2)) =
    f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)

Tactic:
map_mul,

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * (f ↑(x (n i)).2 * f ↑(∏ x_1 ∈ univ.erase i, (x (n x_1)).2)) =
    f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
x : (i : ι) → N i → M i × ↥(S i)
hx : ∀ (i : ι) (z : N i), z * f i ↑(x i z).2 = f i (x i z).1
⊢ ∃ x, z * Pi.map f ↑x.2 = Pi.map f x.1

Tactic:
exact ⟨⟨fun i ↦ (x i (z i)).1, ⟨_, fun i _ ↦ (x i (z i)).2.2⟩⟩, funext fun i ↦ hx i (z i)⟩

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
⊢ Nonempty (TransversalPair G A B)

Tactic:
choose t ht using fun u ↦ (toSubgroup A B u).exists_isComplement_right 1
  exact ⟨⟨t, fun i ↦ (ht i).1⟩⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this : f m ∣ n₁ * n₂ * f ↑⟨↑s₁ * ↑s₂, ⋯⟩
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
map_mul,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this : f m ∣ n₁ * n₂ * (f ↑s₁ * f ↑s₂)
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ s * (m₁, s₁).1
this : f m ∣ f (s * (m₁, s₁).1)
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
map_mul,

Goal state after:
case inl
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ s * (m₁, s₁).1
this : f m ∣ f s * f (m₁, s₁).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case mul
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hm : Irreducible (f (i * a))
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
map_mul,

Goal state after:
case mul
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hm : Irreducible (f i * f a)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (↥(stabilizer (Perm α)ᵈᵐᵃ f))ᵐᵒᵖ
i : ι
a : α
⊢ f ((mk.symm ↑(MulOpposite.unop g)) a) = i ↔ f a = i

Tactic:
rw [← Function.comp_apply (f := f), mem_stabilizer_iff.mp g.unop.prop]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
g✝ : G
this : Cancels 1 (↑g • ofGroup g✝) ↔ Cancels 1 (ofGroup g✝)
hcan : Cancels 1 (ofGroup g✝)
⊢ consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • ofGroup g✝) (fun g_1 a ↦ ↑g • ofGroup g✝)
      (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
    ↑(φ g) •
      consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (ofGroup g✝) (fun g a ↦ ofGroup g✝)
        (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan

pp: case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
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'
this : Cancels 1 (↑g • cons g✝ u✝ w✝ h1✝ h2✝) ↔ Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
hcan : Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
      ↑(φ g) •
        consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝)
          (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
⊢ consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
      (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
    ↑(φ g) •
      consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝) (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan

Tactic:
· simp [Cancels] at hcan

Goal state after:
case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
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'
this : Cancels 1 (↑g • cons g✝ u✝ w✝ h1✝ h2✝) ↔ Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
hcan : Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
      ↑(φ g) •
        consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝)
          (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
⊢ consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
      (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
    ↑(φ g) •
      consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝) (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g✝ : G
hcan : Cancels u (ofGroup g✝)
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (ofGroup g✝) hcan).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ (ofGroup g✝).toReducedWord

pp: case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
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'
hcan : Cancels u (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g✝ u✝ w✝ h1✝ h2✝) hcan).toReducedWord =
      t ^ ↑u * ReducedWord.prod φ (cons g✝ u✝ w✝ h1✝ h2✝).toReducedWord
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g✝ u✝ w✝ h1✝ h2✝) hcan).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ (cons g✝ u✝ w✝ h1✝ h2✝).toReducedWord

Tactic:
· simp [Cancels] at hcan

Goal state after:
case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
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'
hcan : Cancels u (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g✝ u✝ w✝ h1✝ h2✝) hcan).toReducedWord =
      t ^ ↑u * ReducedWord.prod φ (cons g✝ u✝ w✝ h1✝ h2✝).toReducedWord
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g✝ u✝ w✝ h1✝ h2✝) hcan).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ (cons g✝ u✝ w✝ h1✝ h2✝).toReducedWord
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
⊢ ConjAct.toConjAct k • c ∈ g.cycleFactorsFinset

Tactic:
suffices (g.cycleFactorsFinset : Set (Perm α)) =
    (ConjAct.toConjAct k) • g.cycleFactorsFinset by
    rw [← Finset.mem_coe, this]
    simp only [Set.smul_mem_smul_set_iff, Finset.mem_coe, c_mem]
  have := cycleFactorsFinset_conj_eq (ConjAct.toConjAct (k : Perm α)) g
  rw [ConjAct.toConjAct_smul, mem_centralizer_singleton_iff.mp k_mem, mul_assoc] at this
  simp only [mul_inv_cancel, mul_one] at this
  conv_lhs => rw [this]
  simp only [Finset.coe_smul_finset]

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
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
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]

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ Function.Injective ⇑(iteratedWreathToPermHom G 0)

Tactic:
apply Function.injective_of_subsingleton

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : PushoutI φ →* K
i : ι
⊢ ((fun i ↦ f.comp (of i), f.comp (base φ)).1 i).comp (φ i) = (fun i ↦ f.comp (of i), f.comp (base φ)).2

Tactic:
rw [MonoidHom.comp_assoc, of_comp_eq_base]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff] at hx
    rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq,
      ← notMem_support]
    contrapose hx
    obtain ⟨a, -, ha⟩ := mem_support_of_mem_noncommProd_support
      (comm := fun a ha b hb h ↦ g.pairwise_commute_of_mem_zpowers h (v a) (v b) (v a).2 (v b).2) hx
    exact support_zpowers_of_mem_cycleFactorsFinset_le (v a) ha

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
⊢ K = ⊥ ∨ K = N

Tactic:
have h4 := step1 h1 h2 h3

Goal state after:
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : ∀ (K : Subgroup G), K ⊔ N = ⊤ → K = ⊤
⊢ K = ⊥ ∨ K = N
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign (ofSubtype ((k, v).1, (k, v).2).1 * (noncommPiCoprod ⋯) ((k, v).1, (k, v).2).2) = sign k * ∏ c, sign ↑(v c)

Tactic:
map_mul,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign (ofSubtype ((k, v).1, (k, v).2).1) * sign ((noncommPiCoprod ⋯) ((k, v).1, (k, v).2).2) =
    sign k * ∏ c, sign ↑(v c)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!

Tactic:
classical
    obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
    convert! card_isConj_mul_eq g
    simp_rw [Set.coe_ofPred, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
hG : Nat.card G = n
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Tactic:
revert G

Goal state after:
n : ℕ
⊢ ∀ {G : Type u} [inst : Group G] [Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ ⊤ ≤ N

Tactic:
← commutator_alternatingGroup_eq_top (by simpa using hα)

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P

Tactic:
intro p hp P

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
⊢ IsCyclic ↥↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P

Tactic:
intro p hp P

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
⊢ IsCyclic ↥↑P
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : g ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ∈ ↑(⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))

Tactic:
simp only [Set.mem_ofPred_eq] at hg

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ ↑(⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))
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)
g : PushoutI φ
w : NormalWord d
⊢ (g • w).prod = g * w.prod

Tactic:
by
  induction g using PushoutI.induction_on generalizing w with
  | of i g => rw [of_smul_eq_smul, prod_summand_smul]
  | base h => rw [base_smul_eq_smul, prod_base_smul]
  | mul x y ihx ihy => rw [mul_smul, ihx, ihy, mul_assoc]

Goal state after: