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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ ↑(⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ *
        ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩) =
    (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)

Tactic:
coe_mul,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q) * ((↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)) =
    (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))

Tactic:
refine (Nat.le_of_dvd ?_ h2).trans (Nat.pow_le_pow_left h1 _)

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  (center ↥(closureCommutatorRepresentatives G)).index ≤ Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card ↥(_root_.commutator G) ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ 0 <
    (center ↥(closureCommutatorRepresentatives G)).index ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
Module: Mathlib.GroupTheory.Focal

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

Tactic:
by
  rw [← map_subtype_inj, map_focalSubgroupOf, MonoidHom.map_closure, focalSubgroup_def]
  congr
  simp
  grind

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ IsCyclicallyReduced (replicate (n + 1) (head :: tail)).flatten

Tactic:
rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ ((∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, x.1 = y.1 → x.2 = y.2)
        (replicate (n + 1) (head :: tail))) ∧
    ∀ a ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?,
      ∀ b ∈ (replicate (n + 1) (head :: tail)).flatten.head?, a.1 = b.1 → a.2 = b.2
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α × Bool
h : startsWith a = startsWith b
⊢ a = b

Tactic:
simp only [startsWith, Set.ext_iff, Set.mem_ofPred_eq] at h
  simpa using h (mk [a])

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_3.h_obj
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
this : curry E = F'
⊢ ∀ (X_1 : ActionCategory G A), E.obj X_1 = (uncurry F' ⋯).obj X_1

pp: case h_map
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
this : curry E = F'
⊢ ∀ (X_1 Y : ActionCategory G A) (f : X_1 ⟶ Y), E.map f ≍ (uncurry F' ⋯).map f

Tactic:
· intro
        apply Unit.ext

Goal state after:
case h_map
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
this : curry E = F'
⊢ ∀ (X_1 Y : ActionCategory G A) (f : X_1 ⟶ Y), E.map f ≍ (uncurry F' ⋯).map f
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: case mp
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
⊢ (mk [w])⁻¹ • (fun m ↦ m • x) ⟨g, hg⟩ ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
set l := g.toWord with hl

Goal state after:
case mp
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ (mk [w])⁻¹ • (fun m ↦ m • x) ⟨g, hg⟩ ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨mk g.toWord, ⋯⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
← hl,

Goal state after:
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨mk [a], ⋯⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n

Tactic:
exact upperCentralSeries_mono _ h

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ (mk [w])⁻¹ • ⟨mk g.toWord, ⋯⟩ • x ∈ MulAction.orbit (↑(startsWith b)) x

Tactic:
← hl,

Goal state after:
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ (mk [w])⁻¹ • ⟨mk (a :: b :: l), ⋯⟩ • x ∈ MulAction.orbit (↑(startsWith b)) x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case left
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ Setoid.IsPartition (range fun a ↦ orbit (↥N) a)

pp: case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ ∀ ⦃B : Set X⦄, (B ∈ range fun a ↦ orbit (↥N) a) → IsBlock G B

Tactic:
· apply IsPartition.of_orbits

Goal state after:
case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ ∀ ⦃B : Set X⦄, (B ∈ range fun a ↦ orbit (↥N) a) → IsBlock G B
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
this : Fintype α
⊢ ConjAct.toConjAct g • ofSubtype.range = ofSubtype.range

Tactic:
ext k

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ k ∈ ConjAct.toConjAct g • ofSubtype.range ↔ k ∈ ofSubtype.range
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a = a

Tactic:
rw [← Set.mem_singleton_iff]

Goal state after:
case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ {a}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g g' : Perm α
hg : g.IsSwap
hg' : g'.IsSwap
⊢ g * g' ∈ alternatingGroup α

Tactic:
by
  simp [mem_alternatingGroup, map_mul, hg.sign_eq, hg'.sign_eq]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
⊢ n • a = a

Tactic:
rw [← Set.mem_singleton_iff]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
⊢ n • a ∈ {a}
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
⊢ ⇑(AddAction.stabilizerEquivStabilizer hh) ∘ ⇑(AddAction.stabilizerEquivStabilizer hg) =
    ⇑(AddAction.stabilizerEquivStabilizer hk)

Tactic:
ext
    simp [AddAction.stabilizerEquivStabilizer, H, AddAut.addConj, ← add_assoc]

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 α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ m • b = d

Tactic:
rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ map Perm.ofSubtype (alternatingGroup ↥s) = Perm.ofSubtype.range ⊓ alternatingGroup α

Tactic:
ext k

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : Perm α
⊢ k ∈ map Perm.ofSubtype (alternatingGroup ↥s) ↔ k ∈ Perm.ofSubtype.range ⊓ alternatingGroup α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g : ↥(alternatingGroup α)
⊢ MulAut.conj g • (ofSubtype s).range = (ofSubtype (g • s)).range

Tactic:
ext k

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ k ∈ MulAut.conj g • (ofSubtype s).range ↔ k ∈ (ofSubtype (g • s)).range
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M t) = fixingSubgroup M s

Tactic:
ext k

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
⊢ k ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M t) ↔ k ∈ fixingSubgroup M s
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
β : Type u_3
x y : ι ↪ β
⊢ ∃ σ, σ • x = y

Tactic:
obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair x y x.injective y.injective
  exact ⟨σ, Function.Embedding.ext fun i => by simp [Function.Embedding.smul_apply, hσ]⟩

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ ⟨swap a b * swap c d, ⋯⟩ • a = b

Tactic:
simp only [Subgroup.smul_def, Perm.smul_def, Perm.coe_mul]
      grind

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
σ : S.Section
g₁ g₂ : G
⊢ (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
    mul_assoc, inv_mul_cancel]

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:
| top =>

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:
| top =>

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝ : Group G
H : Subgroup G
ne_top : ⊤ ≠ ⊤
⊢ ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

Tactic:
| top =>

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∃ n f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = ⊤ ∧ f n = ⊤

Tactic:
| top =>

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
⊢ (map K.subtype ⊤).IsSubnormal

Tactic:
| top =>

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

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

Tactic:
| top =>

Goal state after:
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:
| top =>

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

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

Tactic:
by
  induction h with
  | top => simp
  | step H K h_le hSubn hN ih =>
    apply step _ (comap f K) (comap_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]
    exact (comap_mono hN).trans (le_normalizer_comap f)

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ : Localization s
a b : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
c✝ : Localization s
c : α × ↥s
⊢ mk a.1 a.2 * mk c.1 c.2 ≤ mk b.1 b.2 * mk c.1 c.2

Tactic:
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ (c.2 : α)] at hab ⊢
        exact mul_le_mul_left hab _

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a c) = a c

Tactic:
conv_rhs => rw [h]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a d) = a d
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ ((g ^ 1) x) = (g ^ 1) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
simp only [zpow_one] at this

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (g x) = ↑(↑τ c) (a.ofPermHomFun τ x)
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q) =
    ↑(⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h)

Tactic:
coe_mul,

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q) = (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q) * ↑h
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
hn : Nonempty ι
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
⊢ f.comp (base φ) = g.comp (base φ)

Tactic:
by
    cases hn with
    | intro i =>
      ext
      rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(kerParam g)

Tactic:
by
  rw [kerParam, MonoidHom.noncommCoprod_injective]
  refine ⟨ofSubtype_injective, ?_, ?_⟩
  · apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
    · intro a
      simp only [range_subtype, ne_eq]
      simp only [zpowers_eq_closure, ← closure_iUnion]
      apply disjoint_closure_of_disjoint_support
      rintro - ⟨-⟩ - ⟨-, ⟨b, rfl⟩, -, ⟨h, rfl⟩, ⟨-⟩⟩
      rw [← disjoint_iff_disjoint_support]
      apply cycleFactorsFinset_pairwise_disjoint g a.2 b.2
      simp only [ne_eq, ← Subtype.ext_iff]
      exact ne_comm.mp h
    · exact fun i ↦ subtype_injective _
  · rw [noncommPiCoprod_range, ← ofSubtype.range.closure_eq]
    simp only [zpowers_eq_closure, ← closure_iUnion]
    apply disjoint_closure_of_disjoint_support
    rintro - ⟨a, rfl⟩ - ⟨-, ⟨b, rfl⟩, ⟨-⟩⟩
    exact (ofSubtype_support_disjoint a).mono_right (mem_cycleFactorsFinset_support_le b.2)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if ¬¬Odd n then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
not_not,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Odd n then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_1.left
ι : 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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
h₁ : ↑(⟨(φ i) h, ⋯⟩ * (⋯.equiv 1).1) = 1
h₂ : ((Word.equivPair i) w).head = 1
⊢ False

Tactic:
coe_mul,

Goal state after:
case refine_1.left
ι : 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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
h₁ : ↑⟨(φ i) h, ⋯⟩ * ↑(⋯.equiv 1).1 = 1
h₂ : ((Word.equivPair i) w).head = 1
⊢ False
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:
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.Perm.Centralizer

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

Tactic:
card_of_cycleType_mul_eq,

Goal state after:
case pos.H2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Fintype.card α)! = if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
this : IsPreprimitive (Perm α) ↑(Set.powersetCard α 2)
⊢ _root_.commutator (Perm α) ≤ N

Tactic:
apply iwasawaStructure_two.commutator_le

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
this : IsPreprimitive (Perm α) ↑(Set.powersetCard α 2)
⊢ fixedPoints ↥N ↑(Set.powersetCard α 2) ≠ _root_.Set.univ
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
⊢ Injective prod

Tactic:
by
  let := Classical.decEq ι
  let := fun i => Classical.decEq (G i)
  exact equiv.symm.injective

Goal state after: