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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ g⁻¹ • y ∈ t

Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem, hg]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ y ∈ s
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
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
this : (fixingSubgroup (↥(stabilizer G a)) t).index * (Nat.card α - 1 - k)! = (Nat.card α - 1)!
⊢ (fixingSubgroup (↥(stabilizer G a)) t).index * (Nat.card α - 1 - k)! * (stabilizer G a).index = (Nat.card α)!

Tactic:
this,

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
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
this : (fixingSubgroup (↥(stabilizer G a)) t).index * (Nat.card α - 1 - k)! = (Nat.card α - 1)!
⊢ (Nat.card α - 1)! * (stabilizer G a).index = (Nat.card α)!
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 α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
⊢ Fin (s.ncard + n) ↪ α

Tactic:
have : Nonempty (Fin (s.ncard) ≃ s) :=
    Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
⊢ Fin (s.ncard + n) ↪ α
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
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

Tactic:
have hs' : f '' s = t := Set.image_preimage_eq t hf.surjective

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
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
⊢ g * Equiv.swap a b ∈ alternatingGroup α

Tactic:
simp [h, hab]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h✝ : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
i : Fin (Nat.card α - 2)
h : x i ∈ Finset.image (⇑x) Finset.univ
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i

Tactic:
← Finset.notMem_compl,

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h✝ : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
i : Fin (Nat.card α - 2)
h : x i ∉ (Finset.image (⇑x) Finset.univ)ᶜ
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left✝ : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : (fixingSubgroup (↥G) s).index * 2 = (Nat.card α)!
⊢ Nat.card (Equiv.Perm α) ≤ (fixingSubgroup (↥G) s).index * 2 * Nat.card ↥(fixingSubgroup (↥G) s)

Tactic:
this,

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Nat.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α s.ncard
left✝ : s ⊆ univ
hs : s.ncard = Nat.card α - 2
this : (fixingSubgroup (↥G) s).index * 2 = (Nat.card α)!
⊢ Nat.card (Equiv.Perm α) ≤ (Nat.card α)! * Nat.card ↥(fixingSubgroup (↥G) s)
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:
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.Perm.MaximalSubgroups

Goal state before:
pp: case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
hG : stabilizer (↥G) s = ⊤
this : G = Subgroup.map G.subtype ⊤
⊢ G ≤ stabilizer M s

Tactic:
this,

Goal state after:
case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
hG : stabilizer (↥G) s = ⊤
this : G = Subgroup.map G.subtype ⊤
⊢ Subgroup.map G.subtype ⊤ ≤ stabilizer M s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inl
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
hB' : (Subtype.val ⁻¹' B).Subsingleton
⊢ (Subtype.val '' Subtype.val ⁻¹' B).Subsingleton

Tactic:
apply Set.Subsingleton.image hB'

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

Goal state before:
pp: case hs_nonempty
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s).Nonempty

pp: case hsc_nonempty
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

pp: case hα
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ Nat.card α ≠ 2 * (↑s).ncard

Tactic:
· rwa [powersetCard.coe_nonempty_iff]

Goal state after:
case hsc_nonempty
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

case hα
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ Nat.card α ≠ 2 * (↑s).ncard
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
⊢ G = ⊤

Tactic:
by
  classical
  have := Fintype.ofFinite α
  rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
  · -- trivial case : Nat.card α ≤ 2
    rw [Nat.lt_succ_iff] at hα3
    apply Subgroup.eq_top_of_card_eq
    simp only [Nat.card_eq_fintype_card]
    apply le_antisymm (Fintype.card_subtype_le _)
    rw [← Nat.card_eq_fintype_card, Nat.card_perm]
    refine le_trans (Nat.factorial_le hα3) ?_
    rw [Nat.factorial_two]
    have : Nonempty G := One.instNonempty
    apply Nat.le_of_dvd Fintype.card_pos
    rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
    exact orderOf_dvd_card
  -- important case : Nat.card α ≥ 3
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3
  have hsc : Set.ncard ((g.support)ᶜ : Set α) = n + 1 := by
    apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      card_support_eq_two.mpr h2g, add_comm, hn]
  apply eq_top_of_isMultiplyPretransitive
  suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by
    apply IsMultiplyPreprimitive.isMultiplyPretransitive
  rw [show Nat.card α - 1 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive hsc
  · rw [hn]; apply Nat.lt_add_one
  have := isPretransitive_of_isCycle_mem h2g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_two
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]
  simp [SubMulAction.mem_ofFixingSubgroup_iff, support]

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
this : 3 = orderOf ⟨g, hg⟩
⊢ 3 ∣ Nat.card ↥G

Tactic:
this,

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
this : 3 = orderOf ⟨g, hg⟩
⊢ orderOf ⟨g, hg⟩ ∣ Nat.card ↥G
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⟩
⊢ ∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

Tactic:
let klift' (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) :
    List (Fin (Fintype.card α)) := List.pmap klift l hl

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
⊢ ∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ map length (map (map ⇑(Fintype.equivFin α).symm) l) = c

Tactic:
rw [← ranges_length c]
    simp only [l, klift', map_pmap, length_pmap,
      pmap_eq_map]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
this,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ (g ^ ↑n) (a (↑τ c)) = (g ^ m) (a (↑τ c))
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun 1 x = x

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun 1 x = x

Tactic:
· rw [ofPermHomFun_apply_of_mem_fixedPoints a _ hx]

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun 1 x = x
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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
      ← mem_support]
    rintro ⟨c, -, hc⟩
    rw [Function.mem_fixedPoints_iff] at hx
    exact mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
⊢ (↑(a.toCentralizer τ) * ↑c) x = (↑(↑τ c) * ↑(a.toCentralizer τ)) x

Tactic:
simp only [mul_apply, toCentralizer_apply]

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

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

Tactic:
this,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ g (a.ofPermHomFun τ x) = ↑(↑τ c) (a.ofPermHomFun τ x)
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
hw : ReducedWord.prod φ w ∈ of.range
⊢ w.toList = []

Tactic:
rcases hw with ⟨g, hg⟩
  let w' : ReducedWord G A B := { ReducedWord.empty G A B with head := g }
  have : w.prod φ = w'.prod φ := by simp [w', ReducedWord.prod, hg]
  simpa [w'] using (map_fst_eq_and_of_prod_eq φ this).1

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
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : IteratedWreathProduct G n →* Equiv.Perm α := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf : Function.Injective ⇑f
g : ↥f.range ≃* IteratedWreathProduct G n := (MonoidHom.ofInjective hf).symm
⊢ Nat.card ↥f.range = p ^ (Nat.card (Equiv.Perm α)).factorization p

Tactic:
Nat.card_congr g.toEquiv,

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : IteratedWreathProduct G n →* Equiv.Perm α := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf : Function.Injective ⇑f
g : ↥f.range ≃* IteratedWreathProduct G n := (MonoidHom.ofInjective hf).symm
⊢ Nat.card (IteratedWreathProduct G n) = p ^ (Nat.card (Equiv.Perm α)).factorization p
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 α
⊢ (∃ a, ∃ (_ : a ∈ alternatingGroup α), a.cycleType = m ∧ a = g) ↔ g.cycleType = m

Tactic:
mem_alternatingGroup,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ (∃ a, ∃ (_ : sign a = 1), a.cycleType = m ∧ a = g) ↔ g.cycleType = m
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:
rw [sign_of_cycleType, hg, Even.neg_one_pow hm]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : ∃ a, ∃ (_ : a ∈ alternatingGroup α), a.cycleType = m ∧ a = g
⊢ False

Tactic:
mem_alternatingGroup,

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : ∃ a, ∃ (_ : sign a = 1), a.cycleType = m ∧ a = g
⊢ False
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case H.inl.of
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
i : ι
g : G i
⊢ motive ↑(inl (CoprodI.of g))

Tactic:
| of i g =>

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ (comap K.subtype ⊥).relIndex H = N.index

Tactic:
MonoidHom.comap_bot,

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ K.subtype.ker.relIndex H = N.index
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤

Tactic:
have h5 : Nat.card (G ⧸ K) < Nat.card G := by
    rw [← index_eq_card, ← K.index_mul_card]
    refine
      lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite)
        (K.one_lt_card_iff_ne_bot.mpr h4.1)

Goal state after:
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : orderOf g ∣ 2 ^ n
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
mem_alternatingGroup,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : sign g = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}