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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
⊢ commutator M ≤ N

Tactic:
have is_transN := IsQuasiPreprimitive.isPretransitive_of_normal hNX

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
⊢ commutator M ≤ N
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
⊢ commutator M ≤ N

Tactic:
have is_transN := IsQuasiPreprimitive.isPretransitive_of_normal hNX
  have ntα : Nontrivial α := nontrivial_of_fixedPoints_ne_univ hNX
  obtain a : α := Nontrivial.to_nonempty.some
  apply nN.commutator_le_of_self_sup_commutative_eq_top ?_ (IwaS.is_comm a)
  -- We have to prove that N ⊔ IwaS.T x = ⊤
  rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]
  intro x
  obtain ⟨g, rfl⟩ := MulAction.exists_smul_eq N a x
  rw [Subgroup.smul_def, IwaS.is_conj g a]
  rintro _ ⟨k, hk, rfl⟩
  have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)
  have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk
  exact (N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')

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

Goal state before:
pp: M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
⊢ IsSimpleGroup M

Tactic:
by
  apply IsSimpleGroup.mk
  intro N nN
  cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with
  | inl h =>
    refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
    apply is_faithful.eq_of_smul_eq_smul
    intro x
    rw [one_smul]
    exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
  | inr h => exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ (toPermHom G (G ⧸ H)).ker.index ∣ H.index !

Tactic:
index_ker,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ H.index !
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ sign.ker.index = 2

Tactic:
index_ker,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥sign.range = 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ 2 ≤ σ.supportᶜ.card

Tactic:
Finset.card_compl,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ 2 ≤ card α - σ.support.card
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ 2 ≤ σ.supportᶜ.card

Tactic:
rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
⊢ σ.support.card + 2 ≤ card α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ [a, g a, b, c].Nodup

Tactic:
grind [Finset.mem_compl]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ [b, c, g a, g (g a)].Nodup

Tactic:
grind [Finset.mem_compl]

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

Goal state before:
pp: g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
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:
rw [mem_alternatingGroup, sign_of_cycleType, h2, Multiset.sum_replicate, Multiset.card_replicate,
    smul_eq_mul, pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha

Goal state after:
g : Perm (Fin 5)
ha : Even g.cycleType.card
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

g : Perm (Fin 5)
ha : (-1) ^ 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
⊢ -1 ≠ 1
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr.left
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
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

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:
· rw [← ofStabilizer.isMultiplyPretransitive]
    exact IsMultiplyPreprimitive.isMultiplyPretransitive M α n.succ

Goal state after:
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)
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)
this : a ∉ Subtype.val '' t
⊢ (insert a (Subtype.val '' t)).ncard = t.ncard + 1

Tactic:
convert! Set.ncard_insert_of_notMem this ?_
        · rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
        apply Set.toFinite

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

Goal state before:
pp: case h
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 : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hkax✝ : ⟨k, hk⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
hkax : ⟨k, hk⟩ • ↑⟨g⁻¹ • a, hg'a⟩ = g⁻¹ • x
⊢ ↑(⟨g * k * g⁻¹, ?w⟩ • ⟨a, ha'⟩) = x

Tactic:
Subgroup.mk_smul,

Goal state after:
case h
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 : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hkax✝ : ⟨k, hk⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
hkax : k • ↑⟨g⁻¹ • a, hg'a⟩ = g⁻¹ • x
⊢ ↑(⟨g * k * g⁻¹, ?w⟩ • ⟨a, ha'⟩) = x
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
⊢ (Finset.image (⇑x) Finset.univ)ᶜ.card = 2

Tactic:
Finset.card_compl,

Goal state after:
α : 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
⊢ Fintype.card α - (Finset.image (⇑x) Finset.univ).card = 2
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 ∉ {a, b}
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i

Tactic:
Finset.mem_insert,

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 = a ∨ x i ∈ {b})
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle

Tactic:
obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := hs

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ¬∀ (b_1 : α), ⟨swap a b * swap a c, ⋯⟩ • b_1 ∈ s ↔ b_1 ∈ s

Tactic:
Subgroup.mk_smul,

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ¬∀ (b_1 : α), (swap a b * swap a c) • b_1 ∈ s ↔ b_1 ∈ s
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
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)

Tactic:
let φ' : stabilizer G s → G := Subtype.val

Goal state after:
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
φ' : ↥(stabilizer (↥G) s) → ↥G := Subtype.val
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

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

Tactic:
rcases eq_or_ne n 1 with rfl | hn1

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
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1

case inr.inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : (∃ a ∈ factors m, f a = x) ∧ ¬IsUnit x
⊢ Prime x

Tactic:
obtain ⟨p, hp, rfl⟩ := hx.1

Goal state after:
case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
p : M
hp : p ∈ factors m
hx : (∃ a ∈ factors m, f a = f p) ∧ ¬IsUnit (f p)
⊢ Prime (f p)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ k ∈ (toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

Tactic:
simp only [toPermHom, MonoidHom.mem_ker, DFunLike.ext_iff, Subtype.forall]
  refine forall₂_congr (fun _ _ ↦ ?_)
  simp [← Subtype.coe_inj, commute_iff_eq, mul_inv_eq_iff_eq_mul]

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
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (id c)) = x

Tactic:
id_eq,

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
⊢ (g ^ m) (a c) = x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) ↔
    ∀ (x : ↥g.cycleFactorsFinset), ((fun c ↦ #(↑c).support) ∘ ⇑τ) x = #(↑x).support

Tactic:
simp only [Subtype.forall, Function.comp_apply]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k✝ : ℤ
hk✝ : ↑a ^ k✝ = ↑(v a)
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉ (g.cycleOf x).support
k : ℤ
hk : ↑⟨g.cycleOf x, hx⟩ ^ k = ↑(v ⟨g.cycleOf x, hx⟩)
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
← hk,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k✝ : ℤ
hk✝ : ↑a ^ k✝ = ↑(v a)
k : ℤ
ha2 : (↑⟨g.cycleOf x, hx⟩ ^ k) x ∉ (g.cycleOf x).support
hk : ↑⟨g.cycleOf x, hx⟩ ^ k = ↑(v ⟨g.cycleOf x, hx⟩)
⊢ x ∈ Function.fixedPoints ⇑g
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
⊢ Nonempty (Transversal φ)

Tactic:
by
  choose t ht using fun i => (φ i).range.exists_isComplement_right 1
  apply Nonempty.intro
  exact
    { injective := hφ
      set := t
      one_mem := fun i => (ht i).2
      compl := fun i => (ht i).1 }

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_2
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
this : ((Word.equivPair i) w).head = (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1

Tactic:
simpa [((injective_iff_map_eq_one' _).1 (d.injective i))] using this

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(OnCycleFactors.toPermHom g).ker * (OnCycleFactors.toPermHom g).ker.index =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
index_ker,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(OnCycleFactors.toPermHom g).ker * Nat.card ↥(OnCycleFactors.toPermHom g).range =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Nat.card ↑{h | IsConj g h}

Tactic:
Set.coe_ofPred,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Nat.card { h // IsConj g h }
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑?m.351 ^ x) k = ↑(uv ?m.351)
⊢ sign ↑(uv ⟨c, hc⟩) = 1

Tactic:
← hk,

Goal state after:
case e'_2.e'_6
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ sign ((fun x ↦ ↑⟨c, hc⟩ ^ x) k) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    (↑((MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩)).support ⊆ s ∧
      (↑((MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩) = 1 ∨ (↑((MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩)).cycleType = {2, 2})

Tactic:
Subgroup.mk_smul,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)) ↔
    (↑((MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩)).support ⊆ s ∧
      (↑((MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩) = 1 ∨ (↑((MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩)).cycleType = {2, 2})
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
refine Or.inr fun p ↦ zpow_one p ▸ ⟨k, p ^ (v.cast : ℤ), ?_⟩

Goal state after:
case neg.inr
G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
p : G
⊢ k • p ^ v.cast * (p ^ v.cast)⁻¹ = p ^ 1