mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ ⇑S.rightHom ∘ ⇑equiv.symm = ⇑S'.rightHom

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
by

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

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝⁴ : Group N
inst✝³ : Group E
inst✝² : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝¹ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst✝ : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
⊢ ⇑(equiv.trans equiv'.toMulEquiv) ∘ ⇑S.inl = ⇑S''.inl

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝ : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial ↥G
⊢ G = ⊤

Tactic:
by

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

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝⁴ : Group N
inst✝³ : Group E
inst✝² : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝¹ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst✝ : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
⊢ ⇑S''.rightHom ∘ ⇑(equiv.trans equiv'.toMulEquiv) = ⇑S.rightHom

Tactic:
by

Goal state after:
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 : ℕ
x✝ : Infinite α
⊢ False

Tactic:
by

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

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
x✝² x✝¹ : S.Section
toFun✝¹ : G → E
rightInverse_rightHom✝¹ : Function.RightInverse toFun✝¹ ⇑S.rightHom
toFun✝ : G → E
rightInverse_rightHom✝ : Function.RightInverse toFun✝ ⇑S.rightHom
x✝ :
  { toFun := toFun✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ }.toFun =
    { toFun := toFun✝, rightInverse_rightHom := rightInverse_rightHom✝ }.toFun
⊢ { toFun := toFun✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ } =
    { toFun := toFun✝, rightInverse_rightHom := rightInverse_rightHom✝ }

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
⊢ AddAction.toPerm g = 1 ↔ AddAction.toPerm g = 1

Tactic:
by

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

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
⊢ Function.Injective fun s ↦ (↑s.toMonoidHom).toFun

Tactic:
by

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

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
s : S.Splitting
⊢ S.rightHom.comp ↑s = MonoidHom.id G

Tactic:
by

Goal state after:
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 α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
this : IsEmpty (Fin n ↪ α)
⊢ IsMultiplyPretransitive K α n

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
⊢ FaithfulVAdd G ↑(powersetCard α n)

Tactic:
by

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
σ σ' : S.Section
g : G
⊢ σ g * (σ' g)⁻¹ ∈ S.inl.range

Tactic:
by

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
σ σ' : S.Section
g : G
⊢ (σ g)⁻¹ * σ' g ∈ S.inl.range

Tactic:
by

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
σ σ' : S.Section
g : G
n : N
hn : S.inl n = σ g * (σ' g)⁻¹
⊢ σ g = S.inl n * σ' g

Tactic:
by

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
σ σ' : S.Section
g : G
⊢ ∃ n, σ g = S.inl n * σ' g

Tactic:
by

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
σ σ' : S.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ σ g = σ' g * S.inl n

Tactic:
by

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
σ σ' : S.Section
g : G
⊢ ∃ n, σ g = σ' g * S.inl n

Tactic:
by

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
σ : S.Section
g₁ g₂ : G
⊢ σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹ ∈ S.inl.range

Tactic:
by

Goal state after:
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 α
h2 : IsMultiplyPretransitive K α 2
⊢ IsMultiplyPretransitive K α n

Tactic:
by

Goal state after:
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 α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
⊢ ∃ a, g • a ≠ a

Tactic:
by

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
σ : S.Section
g₁ g₂ : G
⊢ (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range

Tactic:
by

Goal state after:
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
this : Function.Surjective ⇑φ
⊢ IsMultiplyPretransitive K α 2

Tactic:
by

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
σ : S.Section
g₁ g₂ : G
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

Tactic:
by

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
σ : S.Section
g₁ g₂ : G
⊢ ∃ n, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n

Tactic:
by

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
σ σ' : S.Section
g✝ g₁ g₂ : G
equiv : S.Equiv S'
g : G
⊢ S'.rightHom ((⇑equiv ∘ ⇑σ) g) = g

Tactic:
by

Goal state after:
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
this : φ g = φ 1
⊢ g • a = a

Tactic:
by

Goal state after:
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 : ℕ
⊢ IsMultiplyPretransitive K α n

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ

Tactic:
by

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
⊢ (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e ∈ S.inl.range

Tactic:
by

Goal state after:
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 α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
⊢ toPerm g = 1 ↔ toPerm g = 1

Tactic:
by

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:
by

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
⊢ (fun e' ↦
        let e := Function.surjInv ⋯ (S'.rightHom e');
        e * S.inl (Function.invFun (⇑S'.inl) ((f e)⁻¹ * e')))
      ((↑f).toFun e) =
    e

Tactic:
by

Goal state after:
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 α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
⊢ FaithfulSMul G ↑(powersetCard α n)

Tactic:
by

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'
⊢ (↑f).toFun
      ((fun e' ↦
          let e := Function.surjInv ⋯ (S'.rightHom e');
          e * S.inl (Function.invFun (⇑S'.inl) ((f e)⁻¹ * e')))
        e') =
    e'

Tactic:
by

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
s : S.Splitting
x✝ : N ⋊[s.conjAct] G
n : N
g : G
⊢ (fun e ↦ ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩)
      ((fun x ↦
          match x with
          | ⟨n, g⟩ => S.inl n * s g)
        ⟨n, g⟩) =
    ⟨n, g⟩

Tactic:
by

Goal state after:
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 α (g • f) = id g • ofFinEmb n α f

Tactic:
by

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
s : S.Splitting
e : E
⊢ (fun x ↦
        match x with
        | ⟨n, g⟩ => S.inl n * s g)
      ((fun e ↦ ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩) e) =
    e

Tactic:
by

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
s : S.Splitting
x✝¹ x✝ : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ (match ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ with
    | ⟨n, g⟩ => S.inl n * s g) =
    (match ⟨n₁, g₁⟩ with
      | ⟨n, g⟩ => S.inl n * s g) *
      match ⟨n₂, g₂⟩ with
      | ⟨n, g⟩ => S.inl n * s g

Tactic:
by

Goal state after:
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 α
s : Finset α
hs : s ∈ powersetCard α n
⊢ Fintype.card ?m.29 = #?m.32

Tactic:
by

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

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
s : S.Splitting
⊢ ⇑{
          toFun := fun x ↦
            match x with
            | ⟨n, g⟩ => S.inl n * s g,
          invFun := fun e ↦ ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩, left_inv := ⋯,
          right_inv := ⋯, map_mul' := ⋯ } ∘
      ⇑(SemidirectProduct.toGroupExtension s.conjAct).inl =
    ⇑S.inl

Tactic:
by

Goal state after:
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 α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : ↑(powersetCard α n)
⊢ (compl hm) (g • s) = id g • (compl hm) s

Tactic:
by

Goal state after:
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 α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ (mulActionHom_compl G α ⋯).comp (mulActionHom_compl G α hm) = MulActionHom.id G

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
by

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
s : S.Splitting
⊢ ⇑S.rightHom ∘
      ⇑{
          toFun := fun x ↦
            match x with
            | ⟨n, g⟩ => S.inl n * s g,
          invFun := fun e ↦ ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩, left_inv := ⋯,
          right_inv := ⋯, map_mul' := ⋯ } =
    ⇑(SemidirectProduct.toGroupExtension s.conjAct).rightHom

Tactic:
by

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
s : S.Splitting
⊢ ⇑s = fun g ↦ S.inl 1 * s g * (S.inl 1)⁻¹

Tactic:
by

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

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

Tactic:
by

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
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g ↦ S.inl n * s₂ g * (S.inl n)⁻¹
⊢ ⇑s₂ = fun g ↦ S.inl n⁻¹ * s₁ g * (S.inl n⁻¹)⁻¹

Tactic:
by

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
s₁ s₂ : S.Splitting
h : S.IsConj s₁ s₂
⊢ S.IsConj s₂ s₁

Tactic:
by

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

Goal state before:
pp: α : 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)ᶜ
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
⊢ ⟨g, hg⟩ ∈ fixingSubgroup (↥G) (↑g.support)ᶜ

Tactic:
by

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
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g ↦ S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g ↦ S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ ⇑s₁ = fun g ↦ S.inl (n₁ * n₂) * s₃ g * (S.inl (n₁ * n₂))⁻¹

Tactic:
by

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
s₁ s₂ s₃ : S.Splitting
h₁ : S.IsConj s₁ s₂
h₂ : S.IsConj s₂ s₃
⊢ S.IsConj s₁ s₃

Tactic:
by

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
φ : G →* MulAut N
s : (toGroupExtension φ).Splitting
g : G
⊢ (s g).right = g

Tactic:
← rightHom_eq_right,

Goal state after:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
s : (toGroupExtension φ).Splitting
g : G
⊢ rightHom (s g) = g
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
s : (toGroupExtension φ).Splitting
g : G
⊢ (s g).right = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hgc : g.IsCycle
hg : g ∈ G
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
⊢ fixedPoints G ↑(powersetCard α n) ≠ univ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
⊢ Function.Bijective ⇑(mulActionHom_singleton G α)

Tactic:
by

Goal state after:
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
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
⊢ (↑g.support)ᶜ.ncard = n + 1

Tactic:
apply Nat.add_left_cancel

Goal state after:
case a
α : 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
⊢ ?n + (↑g.support)ᶜ.ncard = ?n + (n + 1)

case n
α : 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
⊢ ℕ
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
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
⊢ (↑g.support)ᶜ.ncard = n + 1

Tactic:
by

Goal state after:
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
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive (Perm α) ↑(powersetCard α n)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))

Tactic:
by

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

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:
by

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

Goal state before:
pp: α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝¹ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
this : Subsingleton ↑(powersetCard α n)
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
by

Goal state after: