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

Goal state before:
pp: case inr.refine_2
α : 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
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ ↑(⟨π * swap a b, ⋯⟩ * ⟨σ, hσ✝⟩ * ⟨π * swap a b, ⋯⟩⁻¹) = ↑⟨τ, hτ⟩

Tactic:
simp only [← hπ, Subgroup.coe_mul]

Goal state after:
case inr.refine_2
α : 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
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ π * swap a b * σ * ↑⟨π * swap a b, ⋯⟩⁻¹ = π * σ * π⁻¹
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
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ _root_.Disjoint {a, b} σ.support

Tactic:
Finset.disjoint_insert_left,

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
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ a ∉ σ.support ∧ _root_.Disjoint {b} σ.support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a
α : 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)))
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})

Tactic:
H

Goal state after:
case a
α : 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)))
⊢ swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a))) ∈ ↑(closure {g | g.cycleType = {2, 2}})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ {g | g.cycleType = {2, 2}} ⊆ ↑(alternatingGroup α)

Tactic:
by
  intro g hg
  rw [Set.mem_ofPred_eq] at hg
  simp [sign_of_cycleType, hg, ← Units.val_inj]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
⊢ (swap (g a) d) c = c

Tactic:
rw [swap_apply_of_ne_of_ne hc.2 hcd]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
⊢ ∃ g, g • x = y

Tactic:
let aux (x : n ↪ β) : (n ↪ α) :=
      x.trans (Function.Embedding.ofSurjective (⇑f) hf)
    have aux_apply (x : n ↪ β) (i : n) : f.toFun (aux x i) = x i := by
      simp only [trans_apply, aux]
      apply Function.surjInv_eq
    obtain ⟨g, hg⟩ := exists_smul_eq (M := G) (aux x) (aux y)
    use σ g
    ext i
    rw [DFunLike.ext_iff] at hg
    rw [smul_apply]
    simp [← aux_apply, ← hg, MulActionHom.map_smul']

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ B

Tactic:
rw [hga]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ a ∈ B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ k ∈ MulAut.conj g • (ofSubtype s).range ↔ k ∈ (ofSubtype (g • s)).range

Tactic:
simp_rw [mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff, ← map_inv,
    MulAut.smul_def, ← ConjAct.toConjAct_smul_eq_mulAut_conj, ConjAct.coe_smul]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ (ConjAct.toConjAct ↑g⁻¹ • ↑k).support ⊆ s ↔ (↑k).support ⊆ g • s
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
by
  rcases Nat.lt_or_ge n 1 with h0 | h1
  · rw [Nat.lt_one_iff] at h0
    rw [h0]
    apply is_zero_preprimitive
  rw [isMultiplyPreprimitive_iff]
  constructor
  · rw [← ofStabilizer.isMultiplyPretransitive]
    exact IsMultiplyPreprimitive.isMultiplyPretransitive M α n.succ
  · 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.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
y : α
hy : y ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))
h : (ofFixingSubgroup_insert_map a s) ⟨x, hx⟩ = (ofFixingSubgroup_insert_map a s) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simpa only [← Subtype.coe_inj, ofFixingSubgroup_insert_map_apply] using h

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

Goal state before:
pp: case h.inl
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
suffices IsPretransitive (fixingSubgroup G s) (ofFixingSubgroup G s) →
      IsMultiplyPretransitive G α 2 by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      rw [hsa] at hs_prim
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]
      exact IsPreprimitive.of_surjective
          ofFixingSubgroup_of_singleton_bijective.surjective

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

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
⊢ ofSubtype g • s = s

Tactic:
ext g'

Goal state after:
α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
g' : α
⊢ g' ∈ ofSubtype g • s ↔ g' ∈ s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_2
s : Set α
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s

pp: case h
α : Type u_2
s : Set α
g : Perm ↑s
⊢ toPerm ⟨ofSubtype g, ?property⟩ = g

Tactic:
· apply ofSubtype_mem_stabilizer

Goal state after:
case h
α : Type u_2
s : Set α
g : Perm ↑s
⊢ toPerm ⟨ofSubtype g, ⋯⟩ = g
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 α
⊢ IsMultiplyPretransitive K α n

Tactic:
suffices h2 : IsMultiplyPretransitive K α 2 by
    by_cases hn : n ≤ 2
    · apply MulAction.isMultiplyPretransitive_of_le' hn
      simp [← hα]
    · suffices (IsEmpty (Fin n ↪ α)) by infer_instance
      rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]

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 α
⊢ IsMultiplyPretransitive K α 2
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
a : α
a✝ : a ∈ _root_.Set.univ
g : K
⊢ φ g = φ 1

Tactic:
simpa [← Subtype.coe_inj] using H.elim ⟨_, ⟨g, rfl⟩⟩ ⟨_, ⟨1, rfl⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
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
n : N
hn : S.inl n = (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e
⊢ S.inl (Function.invFun (⇑S'.inl) (f ((Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e))) =
    (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e

Tactic:
← hn,

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
n : N
hn : S.inl n = (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e
⊢ S.inl (Function.invFun (⇑S'.inl) (f (S.inl n))) = S.inl n
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'
⊢ S'.inl (Function.invFun (⇑S'.inl) ((f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e')) =
    (f (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * e'

Tactic:
apply Function.invFun_eq

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ ↑(ofFinEmb n α (f.trans (Equiv.toEmbedding (toPerm g)))) = id g • ↑(ofFinEmb n α f)

Tactic:
val_ofFinEmb,

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ Finset.map (f.trans (Equiv.toEmbedding (toPerm g))) Finset.univ = id g • ↑(ofFinEmb n α f)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ Finset.map (f.trans (Equiv.toEmbedding (toPerm g))) Finset.univ = id g • ↑(ofFinEmb n α f)

Tactic:
val_ofFinEmb,

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ Finset.map (f.trans (Equiv.toEmbedding (toPerm g))) Finset.univ = id g • Finset.map f Finset.univ
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ S.inl (Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹)) = e * (s (S.rightHom e))⁻¹

Tactic:
apply Function.invFun_eq

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
s : S.Splitting
e : E
⊢ ∃ a, S.inl a = e * (s (S.rightHom e))⁻¹
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
⊢ Function.Surjective ⇑(mulActionHom_of_embedding G α n)

Tactic:
by
  intro ⟨s, hs⟩
  obtain ⟨f : Fin n ↪ α, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])
  exact ⟨f, Subtype.ext hf⟩

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

Goal state before:
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

Tactic:
rw [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq]

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)
⊢ ¬n = Nat.card α
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hsn'
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
⊢ n + 2 < Nat.card α

pp: case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
· rw [hn]; apply Nat.lt_add_one

Goal state after:
case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hsn'
α : 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 α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ n + 2 < Nat.card α

pp: case inr.hprim
α : 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 α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
· grind

Goal state after:
case inr.hprim
α : 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 α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
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
⊢ alternatingGroup α ≤ G

Tactic:
classical
  rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
  · -- trivial case : Fintype.card α ≤ 3
    rw [Nat.lt_succ_iff] at hα4
    apply alternatingGroup_le_of_index_le_two
    rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos),
      Subgroup.index_mul_card, Nat.card_perm]
    apply le_trans (Nat.factorial_le hα4)
    rw [show Nat.factorial 3 = 2 * 3 by simp [Nat.factorial]]
    simp only [mul_le_mul_iff_right₀, Nat.succ_pos]
    apply Nat.le_of_dvd Nat.card_pos
    suffices 3 = orderOf (⟨g, hg⟩ : G) by
      rw [this, Nat.card_eq_fintype_card]
      exact orderOf_dvd_card
    simp only [orderOf_mk, h3g.orderOf]
    -- important case : Nat.card α ≥ 4
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4
  apply IsMultiplyPretransitive.alternatingGroup_le
  suffices IsMultiplyPreprimitive G α (Nat.card α - 2) from
    IsMultiplyPreprimitive.isMultiplyPretransitive ..
  rw [show Nat.card α - 2 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
  · apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      h3g.card_support, add_comm, hn]
  · grind
  have := isPretransitive_of_isCycle_mem h3g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_three
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]
  apply congr_arg
  ext x
  simp [SubMulAction.mem_ofFixingSubgroup_iff]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
⊢ Subgroup.upperCentralSeries (G ⧸ center G) 1 = ⊥

Tactic:
← comap_eq_ker_of_surjective <| QuotientGroup.mk'_surjective _,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
⊢ comap (QuotientGroup.mk' (center G)) (Subgroup.upperCentralSeries (G ⧸ center G) 1) =
    (QuotientGroup.mk' (center G)).ker
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊥
hSubn : ⊥.IsSubnormal
hN : (H.subgroupOf ⊥).Normal
Knorm : ⊥.Normal
⊢ H.Normal

pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
Knorm : ⊤.Normal
⊢ H.Normal

Tactic:
· grind

Goal state after:
case step.inr
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
Knorm : ⊤.Normal
⊢ H.Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
exact step _ _ HK.le Ksn h

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
· grind

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case right
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 = ⊤
⊢ (match 0 with
      | 0 => H
      | n.succ => f n) =
      H ∧
    (match n + 1 with
      | 0 => H
      | n.succ => f n) =
      ⊤

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

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 = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal

Tactic:
· grind

Goal state after:
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

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 = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal
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 = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal

Tactic:
· grind

Goal state after: