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

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ↑P

Tactic:
Subsingleton.elim P.1 ⊤

Goal state after:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑⁅S.lowerCentralSeries n, S⁆

Tactic:
apply normalizer_commutator_ge_right

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ ⊤.lowerCentralSeries n = ⊥

Tactic:
← map_subtype_inj,

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
hn : S.lowerCentralSeries n = ⊥
⊢ map S.subtype (⊤.lowerCentralSeries n) = map S.subtype ⊥
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
this : ∀ {x y : G} (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q
⊢ (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
    (Functor.mapEnd (root' T) F')

Tactic:
rintro ⟨⟨a, b, e⟩, h⟩
          simp only [Functor.mapEnd, DFunLike.coe, this, hF']
          exact dif_neg h

Goal state after:
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, Nonempty (Generators G (Fin n))) → FG G

Tactic:
rintro ⟨n, ⟨P⟩⟩
    exact P.fg

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ ⊤.lowerCentralSeries n = ⊥

Tactic:
← map_subtype_inj,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = map H.subtype ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ ⊤.lowerCentralSeries n = ⊥

Tactic:
← map_subtype_inj,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = map H.subtype ⊥
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
h : H
hg : (g, h).1 ∈ ↑I.goursatFst.toSubmonoid
hh : (g, h).2 ∈ ↑I.goursatSnd.toSubmonoid
⊢ (g, h) ∈ I

Tactic:
simpa using mul_mem (mem_goursatFst.1 hg) (mem_goursatSnd.1 hh)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : Group.IsNilpotent H
⊢ Group.IsNilpotent G

Tactic:
rw [nilpotent_iff_lowerCentralSeries]
  rcases nilpotent_iff_lowerCentralSeries.mp ‹_› with ⟨n, hn⟩
  refine ⟨n + 1, lowerCentralSeries_succ_eq_bot ⊤
    (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)⟩
  rw [map_lowerCentralSeries, ← le_bot_iff]
  exact hn ▸ Subgroup.lowerCentralSeries_mono n le_top

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
hn : nilpotencyClass (G ⧸ center G) = n
⊢ P G

Tactic:
exact hstep _ (ih _ hn)

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y

Tactic:
exact ⟨h * g⁻¹, by rw [← hx, smul_smul, inv_mul_cancel_right, hy]⟩

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

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

Tactic:
exact eq_inv_iff_eq.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (ConjAct.toConjAct k • g).cycleFactorsFinset ↔ c ∈ Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset

Tactic:
ConjAct.smul_def,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (ConjAct.ofConjAct (ConjAct.toConjAct k) * g * (ConjAct.ofConjAct (ConjAct.toConjAct k))⁻¹).cycleFactorsFinset ↔
    c ∈ Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X

Tactic:
have := B.ncard_le_card

Goal state after:
X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
this : B.ncard ≤ Nat.card X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X
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
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G b a

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
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
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G b a

Goal state after:
case inr
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
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β

Tactic:
by
  constructor
  · intro _
    apply IsPreprimitive.of_surjective hf.surjective
  · intro _
    have := (isPretransitive_congr hφ hf).mpr toIsPretransitive
    exact {
      isTrivialBlock_of_isBlock {B} hB := by
        rw [← Set.preimage_image_eq B hf.injective]
        exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective)) }

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ closure {g | (↑g).IsThreeCycle} = ⊤

Tactic:
← map_subtype_inj,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ map (alternatingGroup α).subtype (closure {g | (↑g).IsThreeCycle}) = map (alternatingGroup α).subtype ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ closure {g | (↑g).IsThreeCycle} = ⊤

Tactic:
rw [← map_subtype_inj, MonoidHom.map_closure]
  have : (alternatingGroup α).subtype '' _ = {g : Perm α | IsThreeCycle g} :=
    Subtype.coe_image_of_subset isThreeCycle_subset_alternatingGroup
  aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {g | (↑g).cycleType = {2, 2}} = ⊤

Tactic:
← map_subtype_inj,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ map (alternatingGroup α).subtype (closure {g | (↑g).cycleType = {2, 2}}) = map (alternatingGroup α).subtype ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * (g' * g' * c)).IsThreeCycle

Tactic:
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]

Goal state after:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * c).IsThreeCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
← map_subtype_inj,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ map (alternatingGroup α).subtype (ofSubtype s).range =
    map (alternatingGroup α).subtype (Perm.ofSubtype.range.subgroupOf (alternatingGroup α))
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h.inl
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}
⊢ IsPretransitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a}) →
    IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1

Tactic:
rw [is_one_pretransitive_iff]

Goal state after:
case h.inl
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}
⊢ IsPretransitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a}) →
    IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
⊢ IsMultiplyPreprimitive M α n

Tactic:
by
  rcases Nat.eq_zero_or_pos n with hn | hn
  · rw [hn]
    exact is_zero_preprimitive M α
  rw [isMultiplyPreprimitive_iff]
  constructor
  · exact isMultiplyPretransitive_of_le' (Nat.le_succ n) hα
  · intro s hs
    obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le hn
    apply isPreprimitive_of_is_two_pretransitive
    have hs' : s.encard = m := by
      simp only [hm, Nat.succ_eq_add_one, zero_add, add_comm 1] at hs
      exact ENat.add_left_injective_of_ne_top ENat.one_ne_top hs
    have : Finite s := Set.finite_of_encard_eq_coe hs'
    apply ofFixingSubgroup.isMultiplyPretransitive (G := M) s (n := n.succ)
    simp [Set.ncard, hs', hm, add_comm 1]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
MulAction.isPretransitive_iff_base (⟨a, ha'⟩ : ofFixingSubgroup M (s ∩ g • s))

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ ∀ (x : ↥(ofFixingSubgroup M (s ∩ g • s))), ∃ g_1, g_1 • ⟨a, ha'⟩ = x
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

Tactic:
let φ' : fixingSubgroup M s → fixingSubgroup N t := fun ⟨m, hm⟩ ↦
      ⟨φ m, fun ⟨y, hy⟩ => by
        rw [← hs', Set.mem_image] at hy
        obtain ⟨x, hx, hx'⟩ := hy
        simp only
        rw [← hx', ← map_smulₛₗ]
        apply congr_arg
        rw [mem_fixingSubgroup_iff] at hm
        exact hm x hx⟩

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
Module: Mathlib.GroupTheory.GroupAction.Period

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a

Tactic:
rw [smul_eq_iff_eq_inv_smul, eq_comm, ← zpow_natCast, inv_zpow, inv_inv, zpow_natCast]

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

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock (↥G) B
inst✝ : IsPreprimitive ↥(stabilizer (↥G) B) ↑B
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Subtype.val ⁻¹' B = Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
⊢ B.Subsingleton

Tactic:
have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock (↥G) B
inst✝ : IsPreprimitive ↥(stabilizer (↥G) B) ↑B
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Subtype.val ⁻¹' B = Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (⟨g', hg'⟩ • B) B
⊢ B.Subsingleton
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)

Tactic:
by
    apply this.isTrivialBlock_of_isBlock
    -- `IsBlock (Subtype.val ⁻¹' B : Set s)`
    let φ' : stabilizer G s → G := Subtype.val
    let f' : s →ₑ[φ'] α := {
      toFun := Subtype.val
      map_smul' _ _ := rfl }
    apply MulAction.IsBlock.preimage f' hB

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₁ s₂ : S.Splitting
h : S.IsConj s₁ s₂
⊢ S.IsConj s₂ s₁

Tactic:
by
  obtain ⟨n, hn⟩ := h
  exact ⟨n⁻¹, by simp only [hn, map_inv]; group⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive (Perm α) ↑(powersetCard α n)

Tactic:
by
  -- The finiteness of `α` follows from the assumptions of the theorem.
  have : Finite α := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt hn)
  have : Fintype α := Fintype.ofFinite α
  -- The action is pretransitive.
  have : IsPretransitive (Perm α) (powersetCard α n) := powersetCard.isPretransitive
  -- The type on which the group acts is nontrivial.
  have : Nontrivial (powersetCard α n) := powersetCard.nontrivial' h_one_le hn
  obtain ⟨s⟩ := this.to_nonempty
  -- It remains to prove that stabilizer of some point is maximal.
  rw [← isCoatom_stabilizer_iff_preprimitive _ s]
  -- The stabilizer of a combination is the stabilizer of the underlying set.
  rw [stabilizer_coe]
  -- We conclude by `Equiv.Perm.isCoatom_stabilizer`
  apply isCoatom_stabilizer
  -- `s` is nonempty because `n ≠ 0`.
  · rwa [powersetCard.coe_nonempty_iff]
  -- `sᶜ` is nonempty because `n < Nat.card α`.
  · rw [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq]
    exact hn.ne
  -- `Nat.card α ≠ 2 * s.ncard` because `Nat.card α ≠ 2 * s`.
  · rwa [ncard_eq]

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

Goal state before:
pp: case inr.inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 1 ≤ Nat.card α
hn0 : 1 ≠ 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1

Tactic:
rw [is_one_pretransitive_iff]

Goal state after:
case inr.inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 1 ≤ Nat.card α
hn0 : 1 ≠ 0
⊢ IsPretransitive (↥(alternatingGroup α)) α
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.commutator ↥H = ⊤ ↔ ⁅H, H⁆ = H

Tactic:
← map_subtype_inj,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ _root_.commutator ↥⊤ = ⊤ ↔ _root_.commutator G = ⊤

Tactic:
← map_subtype_inj,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ map ⊤.subtype (_root_.commutator ↥⊤) = map ⊤.subtype ⊤ ↔ _root_.commutator G = ⊤
Module: Mathlib.GroupTheory.IsPerfect

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

Tactic:
derivedSeries_eq_top,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ ⁅⊤, ⊤⁆ = ⊤
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case mul.inr
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'
hai : Irreducible (f a) ∧ IsUnit (f i)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
obtain ⟨u, m', hu, hm', rfl⟩ := ha hai.1

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ Equiv.swap a c ∈ M

Tactic:
rw [Equiv.swap_comm, ← swap_mul_swap_mul_swap hab' hac]

Goal state after:
case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ Equiv.swap b c * Equiv.swap a b * Equiv.swap b c ∈ M
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Tactic:
rw [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ofPermHomFun_apply_of_mem_fixedPoints]

Goal state after:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ (g ^ j) x ∈ Function.fixedPoints ⇑g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c.IsCycle ∧ ∀ a ∈ c.support, c a = g a
this : sign c = 1
⊢ c.IsCycle

Tactic:
exact hc.left

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))
hm' : Even (m.sum + m.card)
⊢ #{g | g.cycleType = m} = 0

Tactic:
rw [Equiv.Perm.card_of_cycleType, if_neg]

Goal state after:
case pos.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos.hnc.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm✝ : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
exact hm

Goal state after: