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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map H.subtype ⊤ ≤ map H.subtype (closure ((fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)))

Tactic:
MonoidHom.map_closure,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map H.subtype ⊤ ≤ closure (⇑H.subtype '' (fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S))
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup = map H.subtype (closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆})

Tactic:
MonoidHom.map_closure,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup = closure (⇑H.subtype '' {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆})
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
⊢ (Nat.card G).minFac - 1 < (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
refine Nat.sub_one_lt_of_le (Nat.card G).minFac_pos (Nat.minFac_le_of_dvd ?_ h1)

Goal state after:
case neg.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
⊢ 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S.lowerCentralSeries (n + 1) ≤ S.lowerCentralSeries n

Tactic:
lowerCentralSeries_succ,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ ⁅S.lowerCentralSeries n, S⁆ ≤ S.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ map f (S.lowerCentralSeries (d + 1)) = (map f S).lowerCentralSeries (d + 1)

Tactic:
lowerCentralSeries_succ,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ map f ⁅S.lowerCentralSeries d, S⁆ = (map f S).lowerCentralSeries (d + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ map f ⁅S.lowerCentralSeries d, S⁆ = (map f S).lowerCentralSeries (d + 1)

Tactic:
lowerCentralSeries_succ,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ map f ⁅S.lowerCentralSeries d, S⁆ = ⁅(map f S).lowerCentralSeries d, map f S⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
⊢ Monotone fun S ↦ S.lowerCentralSeries (d + 1)

Tactic:
intro S T h; simp only [lowerCentralSeries_succ]; exact commutator_mono (hd h) h

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ S.lowerCentralSeries (n + 1) = ⊥

Tactic:
lowerCentralSeries_succ,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ ⁅S.lowerCentralSeries n, S⁆ = ⊥
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this : I'.goursatFst.Normal
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
have := normal_goursatSnd hI₂'

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case h
G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
apply CommGroup.center_eq_top

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
apply CommGroup.center_eq_top

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
S₁ : Subgroup G₁
S₂ : Subgroup G₂
n : ℕ
ih : (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
⊢ (S₁.prod S₂).lowerCentralSeries (n + 1) = (S₁.lowerCentralSeries (n + 1)).prod (S₂.lowerCentralSeries (n + 1))

Tactic:
lowerCentralSeries_succ,

Goal state after:
case succ
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
S₁ : Subgroup G₁
S₂ : Subgroup G₂
n : ℕ
ih : (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
⊢ ⁅(S₁.prod S₂).lowerCentralSeries n, S₁.prod S₂⁆ = ⁅S₁.lowerCentralSeries n, S₁⁆.prod ⁅S₂.lowerCentralSeries n, S₂⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n = pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ (pi Set.univ Ss).lowerCentralSeries (n + 1) = pi Set.univ fun i ↦ (Ss i).lowerCentralSeries (n + 1)

Tactic:
lowerCentralSeries_succ,

Goal state after:
case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n = pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ ⁅(pi Set.univ Ss).lowerCentralSeries n, pi Set.univ Ss⁆ = pi Set.univ fun i ↦ ⁅(Ss i).lowerCentralSeries n, Ss i⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ NormalizerCondition G

Tactic:
rw [normalizerCondition_iff_only_full_group_self_normalizing]
  apply @nilpotent_center_quotient_ind _ G _ _ <;> clear! G
  · intro G _ _ H _
    exact @Subsingleton.elim _ Unique.instSubsingleton _ _
  · intro G _ _ ih H hH
    have hch : center G ≤ H := Subgroup.center_le_normalizer H |>.trans (le_of_eq hH)
    have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
    have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective
    let H' := H.map (mk' (center G))
    have hH' : normalizer H' = H' := by
      apply comap_injective hsur
      rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
      exact hH
    apply map_injective_of_ker_le (mk' (center G)) hkh le_top
    exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : B ⊆ B'
g : G
hgB : g ∈ ↑⟨stabilizer G B, ⋯⟩
⊢ g • a ∈ B'

Tactic:
exact hBB' <| hgB.symm ▸ (Set.smul_mem_smul_set ha)

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
⊢ H.Normal

Tactic:
by
  by_cases hG0 : Nat.card G = 0
  · rw [hG0, minFac_zero] at hHp
    exact normal_of_index_eq_two hHp
  by_cases hG1 : Nat.card G = 1
  · rw [hG1, minFac_one] at hHp
    exact normal_of_index_eq_one hHp
  suffices H.normalCore.relIndex H = 1 by
    convert! H.normalCore_normal
    exact le_antisymm (relIndex_eq_one.mp this) (normalCore_le H)
  have : Finite G := finite_of_card_ne_zero hG0
  have index_ne_zero : H.index ≠ 0 := index_ne_zero_of_finite
  rw [← mul_left_inj' index_ne_zero, one_mul, relIndex_mul_index H.normalCore_le]
  have hp : Nat.Prime H.index := hHp ▸ minFac_prime hG1
  have h : H.normalCore.index ∣ H.index ! := by
    rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]
    exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range
  apply dvd_antisymm _ (index_dvd_of_le H.normalCore_le)
  rwa [← Coprime.dvd_mul_right, mul_factorial_pred hp.ne_zero]
  have hr1 : H.normalCore.index ≠ 1 := fun hr1 ↦ hp.ne_one <|
    Nat.eq_one_of_dvd_one (hr1 ▸ H.normalCore.index_dvd_of_le H.normalCore_le)
  rw [Nat.coprime_factorial_iff hr1]
  exact lt_of_lt_of_le (Nat.sub_one_lt hp.ne_zero) <|
    hHp ▸ minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
      (dvd_trans (minFac_dvd H.normalCore.index) (H.normalCore.index_dvd_card))

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
⊢ IsPreprimitive M α

Tactic:
have := (isPretransitive_congr hφ hf).mpr toIsPretransitive

Goal state after:
case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
⊢ IsPreprimitive G X

Tactic:
let h_bot_or_top := h.eq_bot_or_eq_top

Goal state after:
case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ IsPreprimitive G X
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ = stabilizer G s

Tactic:
refine le_antisymm (le_of_le_of_eq (this _) ?_) (this _)

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜᶜ = stabilizer G s
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite α
hs : s.ncard + n ≤ Nat.card α
⊢ ↑(s.ncard + n) ≤ ↑(Nat.card α)

Tactic:
ENat.natCast_le_natCast

Goal state after:
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite α
hs : s.ncard + n ≤ Nat.card α
⊢ s.ncard + n ≤ Nat.card α
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
hn : ↑m + ↑n ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (range ⇑x) (range ⇑y)
⊢ ∃ a, (fun x ↦ (castAddEmb n).trans x) a = x

Tactic:
use append hxy

Goal state after:
case h
α : Type u_1
m n : ℕ
hn : ↑m + ↑n ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (range ⇑x) (range ⇑y)
⊢ (fun x ↦ (castAddEmb n).trans x) (append hxy) = x
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
inst✝ : Finite α
hn : m + n ≤ Nat.card α
⊢ ↑(m + n) ≤ ↑(Nat.card α)

Tactic:
ENat.natCast_le_natCast

Goal state after:
α : Type u_1
m n : ℕ
inst✝ : Finite α
hn : m + n ≤ Nat.card α
⊢ m + n ≤ Nat.card α
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
⊢ 2 ≤ {a, g a}ᶜ.card

Tactic:
← Nat.add_le_add_iff_left,

Goal state after:
α : 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
⊢ ?m.64 + 2 ≤ ?m.64 + {a, g a}ᶜ.card

α : 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
⊢ ℕ
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ h * g * h⁻¹ ∈ stabilizer G a

Tactic:
exact hyp (normalClosure_normal.conj_mem g (le_normalClosure hg) h)

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

Goal state before:
pp: case succ.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn' : m < n + 1
⊢ ↑n ≤ ↑(n + 1)

Tactic:
ENat.natCast_le_natCast

Goal state after:
case succ.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn' : m < n + 1
⊢ n ≤ n + 1
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
⊢ G = ⊤

Tactic:
have := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card] at hmt
  let j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) :=
    (Fin.castLEEmb ((Fintype.card α).sub_le 1))
  rw [eq_top_iff]
  intro k _
  let x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq rfl).symm.toEmbedding
  let x' := j.trans x
  obtain ⟨g, hg'⟩ := exists_smul_eq G x' (k • x')
  suffices k = g by rw [this]; exact SetLike.coe_mem g
  have hx (x : Fin (Fintype.card α) ↪ α) : Function.Surjective x.toFun := by
    apply Function.Bijective.surjective
    rw [Fintype.bijective_iff_injective_and_card]
    exact ⟨EmbeddingLike.injective x, Fintype.card_fin (Fintype.card α)⟩
  have hgk' (i : Fin (Fintype.card α)) (hi : i.val < Fintype.card α - 1) :
      (g • x) i = (k • x) i :=
    Function.Embedding.ext_iff.mp hg' ⟨i.val, hi⟩
  have hgk (i : Fin (Fintype.card α)) : (g • x) i = (k • x) i := by
    rcases lt_or_eq_of_le (le_sub_one_of_lt i.prop) with hi | hi
    · exact hgk' i hi
    · obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
      rcases lt_or_eq_of_le (le_sub_one_of_lt j.prop) with hj | hj
      · suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
        apply EmbeddingLike.injective (g • x)
        rw [hgk' j hj, hxj]
      · rw [← hxj]
        apply congr_arg
        rw [Fin.ext_iff, hi, hj]
  ext a
  obtain ⟨i, rfl⟩ := (hx x) a
  specialize hgk i
  simp only [Function.Embedding.smul_apply, Equiv.Perm.smul_def] at hgk
  simp [← hgk, Subgroup.smul_def, Perm.smul_def]

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

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

Tactic:
rwa [← Set.one_lt_encard_iff_nontrivial, ← sᶜ.toFinite.cast_ncard_eq, Nat.one_lt_cast,
        ← Nat.add_lt_add_iff_left, Set.ncard_add_ncard_compl, add_comm, hsn, add_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : univ.encard = 2
⊢ Finite α

Tactic:
finite_iff_nonempty_fintype

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : univ.encard = 2
⊢ Nonempty (Fintype α)
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
⊢ B.Subsingleton

Tactic:
suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set s) by
    rcases this with hB' | hB'
    · -- trivial case
      rw [← inter_eq_self_of_subset_right hBs, ← Subtype.image_preimage_val]
      apply Set.Subsingleton.image hB'
    · -- `Subtype.val ⁻¹' B = s`
      have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)
      subst hBs'
      obtain ⟨g', hg', hg's⟩ := SetLike.exists_of_lt hG
      have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's
      suffices (g' • B).Subsingleton by
        exact subsingleton_of_image (MulAction.injective g') B this
      apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)
      exact Disjoint.subset_compl_right h

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
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)
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)ᶜ
hg' : ⟨g, hg⟩ ∈ fixingSubgroup (↥G) (↑g.support)ᶜ
⊢ ∃ k, x = k • a

Tactic:
let g' : fixingSubgroup (↥G) ((↑g.support : Set α)ᶜ) := ⟨(⟨g, hg⟩ : ↥G), hg'⟩

Goal state after:
α : 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)ᶜ
hg' : ⟨g, hg⟩ ∈ fixingSubgroup (↥G) (↑g.support)ᶜ
g' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) := ⟨⟨g, hg⟩, hg'⟩
⊢ ∃ k, x = k • a
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : 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 α ≤ 2
this : Nonempty ↥G
⊢ 2 ∣ Fintype.card ↥G

Tactic:
rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]

Goal state after:
case inl
α : 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 α ≤ 2
this : Nonempty ↥G
⊢ orderOf ⟨g, hg⟩ ∣ Fintype.card ↥G
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ H.IsSubnormal

Tactic:
by
  simp [eq_bot_of_subsingleton H]

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)
c : ↥g.cycleFactorsFinset
a✝¹ : c ∈ ↑(↑τ).support
d : ↥g.cycleFactorsFinset
a✝ : d ∈ ↑(↑τ).support
h : c ≠ d
⊢ (↑c).Disjoint ↑d

Tactic:
apply g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr h)

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β x✝ y✝ : H.LeftTransversal
h : diff (MonoidHom.id ↥H) x✝ y✝ = 1
⊢ 1⁻¹ = 1

Tactic:
inv_one

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β x✝ y✝ : H.LeftTransversal
h : diff (MonoidHom.id ↥H) x✝ y✝ = 1
⊢ 1 = 1