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 = ⊤
⊢ closure ((fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)) = ⊤

Tactic:
rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]
  exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : (center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ 0 ^ (0 + 1)

Tactic:
zero_add,

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : (center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ 0 ^ 1
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ False

Tactic:
Nat.not_odd_iff_even,

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : Even (Nat.card G)
⊢ False
Module: Mathlib.Order.Radical

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (⨅ a ∈ {H | IsCoatom H}, a) = ⨅ a ∈ {H | IsCoatom H}, a

Tactic:
simp only [OrderIso.map_iInf]

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ ⨅ i ∈ {H | IsCoatom H}, f i = ⨅ a ∈ {H | IsCoatom H}, a
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ Group.IsNilpotent ↥(frattini G)

Tactic:
q

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : ⁅x, y⁻¹⁆ ∈ N
⊢ ⁅x⁻¹, y⁆ ∈ N

Tactic:
commutatorElement_def,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : x * y⁻¹ * x⁻¹ * y⁻¹⁻¹ ∈ N
⊢ x⁻¹ * y * x⁻¹⁻¹ * y⁻¹ ∈ N
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ ⁅x✝, y⁆ = 1 ↔ y * x✝ = x✝ * y

Tactic:
commutatorElement_def,

Goal state after:
G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ = 1 ↔ y * x✝ = x✝ * y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ ⁅x, y⁆ ∈ (upperCentralSeriesAux G n).fst

Tactic:
commutatorElement_def,

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G n).fst
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, S.lowerCentralSeries n = ⊥

pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ (∃ n, S.lowerCentralSeries n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
· rintro ⟨n, H, hH, hn⟩
    refine ⟨n, ?_⟩
    have h1 := descending_central_series_ge_lower H hH n
    rw [hn, le_bot_iff] at h1
    rw [← top_subtype_lowerCentralSeries, h1, Subgroup.map_bot]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ (∃ n, S.lowerCentralSeries n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P✝ P : Generators G ι
e : ι' ≃ ι
⊢ Subgroup.closure (Set.range P.val) = ⊤

Tactic:
P.closure_eq_top

Goal state after:
G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P✝ P : Generators G ι
e : ι' ≃ ι
⊢ ⊤ = ⊤
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
⊢ ∀ (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q

Tactic:
q

Goal state after:
case refine_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
⊢ F'.map (loopOfHom T q) = F'.map q
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
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ ⁅y, z⁆ = 1

Tactic:
commutatorElement_def,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ y * z * y⁻¹ * z⁻¹ = 1
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ f' e = 1

Tactic:
exact dif_pos (Or.inr eT)

Goal state after:
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
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ I =
    map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype)
      (comap ((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd))
        (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range)

Tactic:
simp only [MonoidHom.range_comp, Subgroup.range_subtype, I']

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
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ I =
    map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype)
      (comap ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
        (map ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
          (P.prod Q).range))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Tactic:
· suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
    apply le_antisymm
    · apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
      apply comap_injective (f := (mk' (center G))) Quot.mk_surjective
      rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]
      exact upperCentralSeries_nilpotencyClass
    · apply le_of_add_le_add_right
      calc
        n + 1 = Group.nilpotencyClass G := hn.symm
        _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 :=
          nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _))

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False

Tactic:
apply false_of_nontrivial_of_subsingleton G

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G

Tactic:
rw [upperCentralSeries_one]
  exact Subgroup.center_eq_top_iff

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
⊢ IsBlock H (⇑j ⁻¹' B)

Tactic:
by
  rintro g₁ g₂ hg
  rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢
  exact (hB <| ne_of_apply_ne _ hg).preimage _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
⊢ (ConjAct.toConjAct k • g).support = k • g.support

Tactic:
by
  rw [Equiv.Perm.support_conj_eq_smul_support, ConjAct.ofConjAct_toConjAct]

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

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ g'.support.card ≤ 2

Tactic:
apply le_of_add_le_add_left

Goal state after:
case bc
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ ?a + g'.support.card ≤ ?a + 2

case a
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ ℕ
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ ((g' y) w) w ≤ r' ^ 2 * ((g' x) w) w

Tactic:
calc g' y w w
    _ = (g' y - g' x) w w + g' x w w := by simp
    _ ≤ ‖g' y - g' x‖ * ‖w‖ * ‖w‖ + g' x w w := by
      grw [← le_opNorm₂, ← Real.le_norm_self]
    _ ≤ δ * ‖w‖ ^ 2 + g' x w w := by
      rw [pow_two, mul_assoc]; gcongr
    _ ≤ δ * (‖(G : E x →L[ℝ] F)‖ * ‖G.symm w‖) ^ 2 + g' x w w := by
      grw [← le_opNorm]
      simp
    _ = δ * C * ‖G.symm w‖ ^ 2 + g' x w w := by ring
    _ = δ * C * g x (G.symm w) (G.symm w) + g' x w w := by simp [← hg]
    _ = δ * C * g' x w w + g' x w w := by
      congr
      rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
      simp only [Trivial.fiberBundle_trivializationAt', Trivial.linearMapAt_trivialization,
        LinearMap.id_coe, id_eq, w]
      rfl
    _ = (1 + δ * C) * g' x w w := by ring
    _ ≤ r' ^ 2 * g' x w w := by
      gcongr
      rw [← hgx, ← hg, real_inner_self_eq_norm_sq]
      positivity

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 α
m n : ℕ
inst✝¹ : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : n ≤ Nat.card α
inst✝ : Finite α
⊢ IsMultiplyPretransitive G α m

Tactic:
obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact IsPretransitive.of_surjective_map (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_natCard hα) inferInstance

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h : G.index > 0
⊢ alternatingGroup α ≤ G

Tactic:
rcases (Nat.succ_le_iff.mpr h).eq_or_lt' with h | h

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : G.index = Nat.succ 0
⊢ alternatingGroup α ≤ G

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α

Tactic:
by
  constructor
  · intro H1
    rw [← isPreprimitive_of_fixingSubgroup_empty_iff]
    apply H1.isPreprimitive_ofFixingSubgroup (by simp)
  · intro h
    rw [isMultiplyPreprimitive_iff]
    constructor
    · exact is_one_pretransitive_iff.mpr h.toIsPretransitive
    · simpa using isPreprimitive_of_fixingSubgroup_empty_iff.mpr h

Goal state after:
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 : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : 0 + 1 = ↑n.succ
h : s = ∅
⊢ n < 1

Tactic:
zero_add,

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : 1 = ↑n.succ
h : s = ∅
⊢ n < 1
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
this : (fixingSubgroup (↥(stabilizer G a)) t).index * (Nat.card α - 1 - k)! = (Nat.card α - 1)!
⊢ (fixingSubgroup (↥(stabilizer G a)) t).index * (stabilizer G a).index * (Nat.card α - (k + 1))! = (Nat.card α)!

Tactic:
by
      rw [add_comm k, Nat.mul_right_comm, ← Nat.sub_sub, this, mul_comm,
        index_stabilizer_of_transitive G a]
      exact Nat.mul_factorial_pred (card_ne_zero.mpr ⟨⟨a⟩, inferInstance⟩)

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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
refine ⟨stabilizer_ne_top_of_nonempty_of_nonempty_compl h0 h1, fun G hG ↦ ?_⟩

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ G = ⊤
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : sᶜ.ncard * 2 ≤ Nat.card α
⊢ False

Tactic:
rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]

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 infer_instance

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 infer_instance

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ IsPerfect ↥H ↔ ⁅H, H⁆ = H

Tactic:
by
  rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ∀ (u_1 : ℤˣ) (g : G), (u_1, g) ∈ (u, w.head) :: w.toList → g ∈ d.set u_1

Tactic:
by
      intro u' g' h'
      simp only [List.mem_cons, Prod.mk.injEq] at h'
      rcases h' with ⟨rfl, rfl⟩ | h'
      · exact h1
      · exact w.mem_set _ _ h'

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
⊢ ∀ (u' : ℤˣ) (x : G), w.toList.head? = some (u', x) → ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u → u = u'

Tactic:
simp only [Cancels, Option.map_eq_some_iff, Prod.exists, exists_and_right, exists_eq_right,
          not_and, not_exists] at h

Goal state after:
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
⊢ ∀ (u' : ℤˣ) (x : G), w.toList.head? = some (u', x) → ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u → u = u'
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

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

Tactic:
intro s
    rw [mem_map]
    rintro ⟨t, ht, rfl⟩
    apply Nodup.map (Equiv.injective _)
    obtain ⟨u, hu, rfl⟩ := mem_pmap.mp ht
    apply Nodup.of_map
    rw [hl u hu]
    exact ranges_nodup hu

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right.hf
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
a a' : ℕ
ha : a < Fintype.card α
⊢ ∀ (ha' : a' < Fintype.card α), klift a ha = klift a' ha' → a = a'

Tactic:
ha'

Goal state after:
case h.right.right.hf
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
a a' : ℕ
ha : a < Fintype.card α
ha' : a' < Fintype.card α
⊢ klift a ha = klift a' ha' → a = a'