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

Goal state before:
pp: case mpr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a

Tactic:
intro hx
    obtain ⟨k, rfl⟩ := exists_smul_eq G a x
    exact ⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩

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

Goal state before:
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'
hBB' : B ⊆ B'
⊢ ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩

Tactic:
g

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'
hBB' : B ⊆ B'
g : G
⊢ g ∈ ↑⟨stabilizer G B, ⋯⟩ → g ∈ ↑⟨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✝ : α
⊢ a✝ ∈ (k • g).support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support

Tactic:
rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]

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

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

Tactic:
exact Finset.inv_smul_mem_iff

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne

Goal state after:
case inl
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ ⇑(stabilizerEquivStabilizer hh) ∘ ⇑(stabilizerEquivStabilizer hg) = ⇑(stabilizerEquivStabilizer hk)

Tactic:
ext
    simp [stabilizerEquivStabilizer, H, MulAut.conj, ← mul_assoc]

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

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

Tactic:
apply lt_of_mul_lt_mul_right' (hf'.trans_le' _)

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

Goal state before:
pp: case succ.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * b ∈ closure {σ | σ.IsThreeCycle}

Tactic:
grind [IsSwap.mul_mem_closure_three_cycles]

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

Goal state before:
pp: case succ.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
grind [IsSwap.mul_mem_closure_three_cycles]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
a✝ : Nontrivial α
hα' : Nat.card α = 2
⊢ alternatingGroup α = ⊥

Tactic:
by
    rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G

Tactic:
rw [eq_alternatingGroup_of_index_eq_two (hG.antisymm h)]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
⊢ ∃ g, g • x = y

Tactic:
set y' := ofFixingSubgroup.append y with hy

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
⊢ ∃ g, g • x = y
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' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α 2

Tactic:
rw [hsa] at hs_prim

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' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a})
⊢ IsMultiplyPreprimitive G α 2
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
hst : g • s = t
⊢ Bijective ⇑(conjMap_ofFixingSubgroup hst)

Tactic:
constructor
  · rintro x y hxy
    simpa [← SetLike.coe_eq_coe] using hxy
  · rintro ⟨x, hx⟩
    rw [eq_comm, ← inv_smul_eq_iff] at hst
    use (SubMulAction.conjMap_ofFixingSubgroup hst) ⟨x, hx⟩
    simp [← SetLike.coe_eq_coe]

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

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
⊢ Injective ⇑(map_ofFixingSubgroupUnion M s t)

Tactic:
intro a b h

Goal state after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a b : ↥(ofFixingSubgroup M (s ∪ t))
h : (map_ofFixingSubgroupUnion M s t) a = (map_ofFixingSubgroupUnion M s t) b
⊢ a = b
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case succ.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn' : m < n + 1
⊢ ↑n ≤ ↑(n + 1)

Tactic:
rw [ENat.natCast_le_natCast]

Goal state after:
case succ.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn' : m < n + 1
⊢ n ≤ n + 1
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ b ∈ swap a b • s

Tactic:
Set.mem_smul_set

Goal state after:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b • s = s
⊢ ∃ y ∈ s, swap a b • y = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ k ∈ G

Tactic:
· -- `k ∈ G`
      apply hG
      exact MulAction.fixingSubgroup_le_stabilizer _ _ hk

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

Goal state before:
pp: case refine_1.h
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
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ (Subtype.val '' t).ncard + ?refine_1.m = n + 1 + ?refine_1.m

pp: case refine_1.m
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
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ ℕ

Tactic:
← Set.ncard_insert_of_notMem ha',

Goal state after:
case refine_1.h
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
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ (insert a (Subtype.val '' t)).ncard = n + 1 + 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.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ σ g = σ' g * S.inl n

Tactic:
by rw [hn, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
⊢ a ∈ fixedPoints K α

Tactic:
g

Goal state after:
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
⊢ g • a = a
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) sᶜ)

Tactic:
apply this h1 <;> rw [compl_compl] <;> grind

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

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
⊢ derivedSeries G 0 = ⊤
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ derivedSeries G (n + 1) = ⊤

Tactic:
| =>

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ derivedSeries G (n + 1) = ⊤
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:
| =>

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n : ℕ
⊢ H.lowerCentralSeries 0 = H
Module: Mathlib.GroupTheory.IsPerfect

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

Tactic:
| =>

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n✝ n : ℕ
⊢ H.lowerCentralSeries (n + 1) = H
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
c✝ : Localization s
c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
⊢ ↑b.2 * a.1 * (↑c.2 * c.1) ≤ ↑a.2 * b.1 * (↑c.2 * c.1)

Tactic:
exact mul_le_mul_left hab _

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

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

Tactic:
simp only [unitsSMulWithCancel, toSubgroup_one, id_eq, toSubgroup_neg_one, toSubgroupEquiv_one,
      group_smul_head, mul_inv_rev, dif_pos (this.2 hcan), dif_pos hcan]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : Cancels 1 w
⊢ consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • w) (fun g_1 a ↦ ↑g • w)
      (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
    ↑(φ g) •
      consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) w (fun g a ↦ w)
        (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
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
g g' : G
x✝¹ : g ∈ closure S
x✝ : g' ∈ closure S
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ

Tactic:
simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]

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

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
a' : g.Basis
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ : (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ } = (fun a ↦ a.toFun) a'
⊢ { toFun := toFun✝, mem_support_self' := mem_support_self'✝ } = a'

Tactic:
cases a'

Goal state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
toFun✝¹ : ↥g.cycleFactorsFinset → α
mem_support_self'✝¹ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝¹ c ∈ (↑c).support
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ :
  (fun a ↦ a.toFun) { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }
⊢ { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
w₂' : NormalWord d
hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂'.toReducedWord

Tactic:
rw [hw₁'1, hw₂'1, hprod]

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 Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
⊢ ∀ {m₁ m₂ : D ≀ᵣ Q},
    (∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right) → m₁ = m₂

Tactic:
intro m₁

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
m₁ : D ≀ᵣ Q
⊢ ∀ {m₂ : D ≀ᵣ Q},
    (∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right) → m₁ = m₂
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
g : G i
⊢ ofCoprodI (CoprodI.of g) = (of i) g

Tactic:
by
  simp [ofCoprodI]

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

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

Tactic:
if_pos hm.2,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ #{g | g.cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
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✝ * ((Word.equivPair i) w).head = 1
⊢ False

Tactic:
apply_fun (d.compl i).equiv at h

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 : ⋯.equiv ((φ i) h✝ * ((Word.equivPair i) w).head) = ⋯.equiv 1
⊢ False