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

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 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
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard - 1 < n

Tactic:
rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 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
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard < s.ncard
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
hn1 : 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
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
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:
refine ⟨this, fun 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 : 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
hn1 : 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
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α 2
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
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ ofFixingSubgroup M s
⊢ (match ⟨m, hm⟩ • ⟨x, hx⟩ with
    | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩) =
    φ' ⟨m, hm⟩ •
      match ⟨x, hx⟩ with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩

Tactic:
rw [← SetLike.coe_eq_coe]

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, ⋯⟩
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ ofFixingSubgroup M s
⊢ ↑(match ⟨m, hm⟩ • ⟨x, hx⟩ with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩) =
    ↑(φ' ⟨m, hm⟩ •
        match ⟨x, hx⟩ with
        | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case refine_2
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
inst✝ : Finite α
hs : IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard

Tactic:
· rw [← Set.smul_set_compl, Set.ncard_smul_set, two_mul]

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
⊢ t.ncard - 1 < n

Tactic:
rw [Nat.lt_iff_add_one_le, ← htm, Nat.le_iff_lt_add_one, ← hsn]

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
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
⊢ t.ncard < s.ncard
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case e'_5
α : 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
this : 1 + 1 = 2
⊢ s.encard = 1

Tactic:
· apply le_antisymm
      · assumption
      rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
      aesop

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

Goal state before:
pp: case e'_6
α : 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
this : 1 + 1 = 2
⊢ sᶜ.encard = 1

Tactic:
· apply le_antisymm
      · assumption
      rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
      aesop

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ k ↑x = ↑x

Tactic:
rw [← notMem_support]

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ ↑x ∉ k.support
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:
refine ⟨this, fun 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 : 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
hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : g ∈ stabilizer (Perm α) s
hg3 : g.IsThreeCycle
⊢ IsPreprimitive (↥(Subgroup.map (alternatingGroup α).subtype G)) α

Tactic:
let φ := (alternatingGroup α).subtype.subgroupMap G
    let f : α →ₑ[φ] α := {
      toFun := id
      map_smul' _ _ := rfl }
    rwa [← isPreprimitive_congr (f := f) ((alternatingGroup α).subtype.subgroupMap_surjective G)
      Function.bijective_id]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : Nat.card α ≠ 2 * s.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
← ncard_add_ncard_compl s,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : s.ncard + sᶜ.ncard ≠ 2 * s.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)
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
⊢ False

Tactic:
apply hK

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 α := ⋯
f : α →ₑ[⇑φ] α := ⋯
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
⊢ fixedPoints K α = _root_.Set.univ
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
k : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk' : y = k' • a
⊢ (k' * k⁻¹) • ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
rw [← SetLike.coe_eq_coe]

Goal state after:
case h
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
y : α
hy : y ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
k : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ)
hk' : y = k' • a
⊢ ↑((k' * k⁻¹) • ⟨x, hx⟩) = ↑⟨y, hy⟩
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K = ⊤ ∨ ∃ K_1, K < K_1 ∧ K_1.IsSubnormal ∧ (K.subgroupOf K_1).Normal
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
obtain rfl | ⟨K', HK', hS', hN'⟩ := ih
      · obtain rfl | hH := eq_or_ne H ⊤
        · simp
        · exact Or.inr ⟨⊤, by simp [hH.lt_top , *]⟩
      right
      obtain rfl | hH := eq_or_ne H K
      · use K'
      · exact ⟨K, by simpa [*] using HK.lt_of_ne hH⟩

Goal state after:
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
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Tactic:
by
  have key0 : ¬ closure S ≤ stabilizer G T := by
    have ⟨b, hb⟩ := nonempty
    obtain ⟨σ, rfl⟩ := subset hb
    contrapose notMem with h
    exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)
  contrapose! key0
  refine (closure_le _).mpr fun σ hσ ↦ ?_
  simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, mem_smul_set_iff_inv_smul_mem]
  exact fun a ↦ ⟨fun h ↦ smul_inv_smul σ a ▸ key0 σ hσ (σ⁻¹ • a) h, key0 σ⁻¹ (hS σ hσ) a⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hd hm] --
    rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]
    by_cases h : c = d
    · simp only [h, hd, mem_support_self]
    · have H : Disjoint c.val d.val :=
        cycleFactorsFinset_pairwise_disjoint g c.prop d.prop (Subtype.coe_ne_coe.mpr h)
      have H' : Disjoint ((τ : Perm g.cycleFactorsFinset) c : Perm α)
        ((τ : Perm g.cycleFactorsFinset) d : Perm α) :=
        cycleFactorsFinset_pairwise_disjoint g ((τ : Perm g.cycleFactorsFinset) c).prop
          ((τ : Perm g.cycleFactorsFinset) d).prop (by
          intro h'; apply h
          simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h')
      rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'
      simp only [H hd, H' (mem_support_self a _)]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
d : ↥g.cycleFactorsFinset
hd : ↑τ d ≠ d
⊢ ↑d x = x

Tactic:
rw [← notMem_support]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
H : ↑τ c = c
d : ↥g.cycleFactorsFinset
hd : ↑τ d ≠ d
⊢ x ∉ (↑d).support
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ ReducedWord.prod φ w = ReducedWord.prod φ w'

Tactic:
simp [w', ReducedWord.prod, hg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := fun c ↦ #(↑c).support
hsc : sc = fun c ↦ #(↑c).support
x✝ : Perm ↥g.cycleFactorsFinset
⊢ ((fun c ↦ #(↑c).support) ∘ ⇑x✝ = fun c ↦ #(↑c).support) ↔ x✝ ∈ {k | sc ∘ ⇑k = sc}

Tactic:
Set.mem_ofPred_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := fun c ↦ #(↑c).support
hsc : sc = fun c ↦ #(↑c).support
x✝ : Perm ↥g.cycleFactorsFinset
⊢ ((fun c ↦ #(↑c).support) ∘ ⇑x✝ = fun c ↦ #(↑c).support) ↔ sc ∘ ⇑x✝ = sc
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 Even ({n}.sum + {n}.card) then {g | g.cycleType = {n}} else ∅) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
apply_ite Finset.card

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1 ∨ g ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
Set.mem_ofPred_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : g = 1 ∨ (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

Tactic:
simp_rw [hk, false_and, iff_false]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∉ Subgroup.map (ofSubtype s) (kleinFour ↥s)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n

Tactic:
← Fintype.card_eq.mpr ⟨fintypeHelper⟩,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (ZMod (2 * n) ⊕ ZMod (2 * n)) = 4 * n
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : k = 1 ∨ k ∈ {g | (↑g).cycleType = {2, 2}}
⊢ (↑k).cycleType = {2, 2}

Tactic:
Set.mem_ofPred_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : k = 1 ∨ (↑k).cycleType = {2, 2}
⊢ (↑k).cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P → ¬p ∣ Nat.card ↥(commutator G)

case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ↑P ≤ commutator G → ¬p ∣ (commutator G).index