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

Goal state before:
pp: case refine_1.cons.inl
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'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inl e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

pp: case refine_1.cons.inr
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'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inr e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
· rw [hF']
            exact dif_pos (Or.inl eT)

Goal state after:
case refine_1.cons.inr
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'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inr e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Tactic:
exact upperCentralSeries_nilpotencyClass

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

Goal state before:
pp: case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x : X
⊢ ∃ x_1 ∈ range fun x ↦ orbit G x, x ∈ x_1

Tactic:
exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) → ∃ y, y • g • a = x✝

Tactic:
rintro ⟨⟨k, hk⟩, rfl⟩

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, y • g • a = g • ⟨k, hk⟩ • a
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
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = x✝

Tactic:
rintro ⟨⟨k, hk⟩, rfl⟩

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ y, g • y • a = ⟨k, hk⟩ • g • a
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index = 1
⊢ H.Normal

Tactic:
by
  rw [index_eq_one] at hH
  rw [hH]
  infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜᶜ = stabilizer G s

Tactic:
compl_compl

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G s = stabilizer G s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
ha : sign g = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
sign_of_cycleType,

Goal state after:
g : Perm (Fin 5)
ha : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
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'
⊢ (embFinTwo h') 0 = c

Tactic:
embFinTwo_apply_zero

Goal state after:
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'
⊢ c = c
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
⊢ s ∩ range Subtype.val = s \ {a}

Tactic:
simp only [Subtype.range_coe_subtype]

Goal state after:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
⊢ s ∩ {x | x ∈ ofStabilizer G a} = s \ {a}
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr.right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ ∀ {s : Set ↥(ofStabilizer M a)},
    s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)

Tactic:
intro s hs
    have : IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
      ↥(ofFixingSubgroup M (insert a (Subtype.val '' s))) := by
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup M n.succ
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]
      aesop
    exact IsPreprimitive.of_surjective ofFixingSubgroup_insert_map_bijective.surjective

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
⊢ Function.Surjective toPerm

Tactic:
classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop

Goal state after:
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
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hsgs_ne_top : s ∪ g • s ≠ ⊤
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      apply (hrec _ hmn hG htm htm').2
      exact IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
          hs_prim hsgs_ne_top

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝¹ : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card (Perm α)))
x✝ : G = ⊥ ∨ G = ⊤
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
cases G.eq_bot_or_eq_top_of_prime_card with

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

Goal state before:
pp: case pos
α : 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 : {a, b}.ncard < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
replace ht := Set.sdiff_nonempty_of_ncard_lt_ncard ht

Goal state after:
case pos
α : 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 : (t \ {a, b}).Nonempty
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
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:
compl_compl

Goal state after:
α : 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
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ sᶜᶜ.ncard < sᶜ.ncard

Tactic:
compl_compl

Goal state after:
case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ s.ncard < sᶜ.ncard
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:
compl_compl

Goal state after:
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
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr.h1
α : 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
⊢ sᶜᶜ.Nonempty

Tactic:
compl_compl

Goal state after:
case inr.h1
α : 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
⊢ s.Nonempty
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr.hs
α : 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
⊢ ¬sᶜᶜ.ncard = sᶜ.ncard

Tactic:
compl_compl

Goal state after:
case inr.hs
α : 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
⊢ ¬s.ncard = sᶜ.ncard
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr.hs'
α : 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
⊢ sᶜ.ncard < sᶜᶜ.ncard

Tactic:
compl_compl

Goal state after:
case inr.hs'
α : 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
⊢ sᶜ.ncard < s.ncard
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'
⊢ (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e' ∈ S'.inl.range

Tactic:
S'.range_inl_eq_ker_rightHom,

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'
⊢ (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e' ∈ S'.rightHom.ker
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case hf.refine_1
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : (toPermHom G ↑(powersetCard α n)) g = 1
⊢ ↑n < ENat.card α

Tactic:
·   simpa [ENat.card_eq_coe_natCard, Nat.cast_lt, Nat.finite_of_card_ne_zero (ne_zero_of_lt hn')]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
⊢ IsPerfect ↥(map f ⊤)

Tactic:
exact IsPerfect.map _

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ Monotone fun x ↦
    match x with
    | 0 => H
    | n.succ => f n

Tactic:
refine monotone_nat_of_le_succ ?_
        grind only [monotone_iff_forall_lt]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : (A.subgroupOf B).Normal
ih : (map K.subtype B).IsSubnormal
⊢ (map K.subtype A).IsSubnormal

Tactic:
refine step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (map_mono h_le)]
    exact le_trans (map_mono hN) (le_normalizer_map _)

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

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

Tactic:
conv_rhs => rw [← List.map_id a]

Goal state after:
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
a : List ℕ
ha : a ∈ c.ranges
⊢ map (⇑Fin.valEmbedding) (klift' a ⋯) = map id a
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
intro ⟨hf, hg, hp⟩ a b h
    have key := hp ⟨⟨a⁻¹, by rwa [map_inv, inv_eq_iff_mul_eq_one]⟩, b, rfl⟩
    exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
⊢ Equiv.swap x y ∈ closure S ↔ x ∈ orbit (↥(closure S)) y

Tactic:
refine ⟨fun h ↦ ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
⊢ Equiv.swap x y ∈ closure S
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
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
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
⊢ m₁.left q = m₂.left q

pp: case right
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
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b : Q
⊢ m₁.right = m₂.right

Tactic:
· have hh := fun a => (h a (m₁.right⁻¹ * q)).1
      rw [← (h a b).2] at hh
      group at hh
      exact FaithfulSMul.eq_of_smul_eq_smul hh

Goal state after:
case right
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
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b : Q
⊢ m₁.right = m₂.right
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), (∀ (i : FiniteIndexNormalSubgroup G), x ∈ i.toSubgroup) → x = 1) ↔
    ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

Tactic:
FiniteIndexNormalSubgroup.mem_toSubgroup_iff

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 : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
⊢ sign g = 1

Tactic:
sign_of_cycleType,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
⊢ (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
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 : ι
x : H
⊢ ((of i).comp (φ i)) x = (base φ) x

Tactic:
apply (Con.eq _).2

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (con φ) ((inl.comp CoprodI.of) ((φ i) x)) (inr x)