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

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ∀ l ∈ (singleton x✝ a✝).toList, l.snd ≠ 1

Tactic:
simpa only [toList, List.mem_singleton, ne_eq, forall_eq]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
⊢ ∀ x ∈ _w₁✝.toList.getLast?, ∀ y ∈ _w₂✝.toList.head?, x.fst ≠ y.fst

Tactic:
intro x

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
⊢ x ∈ _w₁✝.toList.getLast? → ∀ y ∈ _w₂✝.toList.head?, x.fst ≠ y.fst
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_2
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ ↑1 • ↑(⟨a.den, ⋯⟩ * (⟨b.den, ⋯⟩ * s)) • (a * b).num • m = ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m

Tactic:
simp [← natCast_zsmul, smul_smul]

Goal state after:
case e'_2
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ (↑a.den * (↑b.den * ↑↑s) * (a * b).num) • m = ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_3
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ ↑1 • ↑(⟨(a * b).den, ⋯⟩ * s) • a.num • b.num • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m

Tactic:
simp [← natCast_zsmul, smul_smul]

Goal state after:
case e'_3
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ (↑(a * b).den * ↑↑s * (a.num * b.num)) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b : DivisibleHull M
h : a ≤ b
h' : b ≤ a
⊢ a = b

Tactic:
by
    induction a with | mk ma sa
    induction b with | mk mb sb
    rw [mk_le_mk] at h h'
    rw [mk_eq_mk_iff_smul_eq_smul]
    exact le_antisymm h h'

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(leftRel K)), ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
x : Quot ⇑(leftRel K)
⊢ ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(rightRel H)), ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
x : Quot ⇑(rightRel H)
⊢ ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: case refine_1
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝¹ x✝ : G
h : { toFun := fun φ ↦ φ x✝¹, map_one' := ⋯ } = { toFun := fun φ ↦ φ x✝, map_one' := ⋯ }
⊢ x✝¹ = x✝

Tactic:
OneHom.mk.injEq,

Goal state after:
case refine_1
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝¹ x✝ : G
h : (fun φ ↦ φ x✝¹) = fun φ ↦ φ x✝
⊢ x✝¹ = x✝
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1 → (f i) (FreeGroup.freeGroupUnitEquivInt.symm n) • X' j ⊆ X' i

Tactic:
hne1

Goal state after:
case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ (f i) (FreeGroup.freeGroupUnitEquivInt.symm n) • X' j ⊆ X' i
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
rw [smul_apply_eq_smul_apply_inv_smul, transferTransversal_apply, transferFunction_apply, ←
    mul_smul, ← zpow_neg_one, ← zpow_add, quotientEquivSigmaZMod_apply, smul_eq_mul, ← mul_assoc,
    ← zpow_one_add, Int.cast_add, Int.cast_neg, Int.cast_one, intCast_cast, cast_id', id, ←
    sub_eq_neg_add, cast_sub_one, add_sub_cancel]
  by_cases hk : k = 0
  · rw [if_pos hk, if_pos hk, zpow_natCast]
  · rw [if_neg hk, if_neg hk]

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ Surjective ⇑(↑P).transferFocal

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
x : ↥↑P ⧸ (↑P).focalSubgroupOf
⊢ ∃ a, (↑P).transferFocal a = x
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ _root_.commutator G ⊓ ↑P = (↑P).focalSubgroup

Tactic:
apply le_antisymm
  · apply le_trans ?_ (ker_transferFocal_inf_eq_focalSubgroup P).le
    exact inf_le_inf_right _ (Abelianization.commutator_subset_ker P.transferFocal)
  · exact le_inf P.focalSubgroup_le_commutator P.focalSubgroup_le

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]

Goal state after:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
⊢ H (n + 1) ≤ upperCentralSeries G (n + 1)

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
⊢ x ∈ H (n + 1) → x ∈ upperCentralSeries G (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)

Tactic:
intro x

Goal state after:
case right
G : Type u_1
inst✝ : Group G
x : G
⊢ ∀ (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ⊤.lowerCentralSeries n = ⊥

pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
· rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← le_bot_iff, ← hn]
    exact descending_central_series_ge_lower H hH n

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, Nonempty (Generators G (Fin n))) → FG G

Tactic:
rintro ⟨n, ⟨P⟩⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
P : Generators G (Fin n)
⊢ FG G
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:
intro x

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 : G
⊢ ∀ {y : G} (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (∃ g, g • a = a_1) ↔ (a_1 ∈ orbit G a ↔ a_1 ∈ Set.univ)

Tactic:
intro x

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ x ∈ Set.univ)
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ ∀ (x y : β), ∃ g, g • x = y

Tactic:
intro x

Goal state after:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x : β
⊢ ∀ (y : β), ∃ g, g • x = y
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
⊢ ∀ (x y : α), ∃ g, g • x = y

Tactic:
intro x

Goal state after:
case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x : α
⊢ ∀ (y : α), ∃ g, g • x = y
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ (range fun x ↦ orbit G x).PairwiseDisjoint id

Tactic:
rintro s ⟨x, rfl⟩ t ⟨y, rfl⟩ h

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x y : X
h : (fun x ↦ orbit G x) x ≠ (fun x ↦ orbit G x) y
⊢ Function.onFun Disjoint id ((fun x ↦ orbit G x) x) ((fun x ↦ orbit G x) y)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃ x ∈ range fun x ↦ orbit G x, a ∈ x

Tactic:
intro x

Goal state after:
case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x : X
⊢ ∃ x_1 ∈ range fun x ↦ orbit G x, x ∈ x_1
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ (g • B).Subsingleton

Tactic:
exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
⊢ IsBlock G ↑s

Tactic:
simp only [IsBlock, disjoint_left]
  rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
  refine hab ?_
  rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]

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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a

Tactic:
intro x

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

Goal state before:
pp: case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a

Tactic:
intro x

Goal state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : ⊥ = ⊤
⊢ False

Tactic:
← Subtype.coe_inj

Goal state after:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False
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:
rw [Equiv.Perm.support_conj_eq_smul_support, ConjAct.ofConjAct_toConjAct]

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

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
⊢ ∀ (x : X), ∃ g, g • a = x

Tactic:
intro x

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ ∃ g, g • a = x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ Function.Surjective ⇑(conjMap hg)

Tactic:
intro x

Goal state after:
case right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G b)
⊢ ∃ a_1, (conjMap hg) a_1 = x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G ∅ = ⊤

Tactic:
by
  aesop

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G univ = ⊤

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
hn : ↑m + ↑n ≤ ENat.card α
⊢ Surjective fun x ↦ (castAddEmb n).trans x

Tactic:
intro x

Goal state after:
α : Type u_1
m n : ℕ
hn : ↑m + ↑n ≤ ENat.card α
x : Fin m ↪ α
⊢ ∃ a, (fun x ↦ (castAddEmb n).trans x) a = x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : Perm α
⊢ k ∈ map Perm.ofSubtype (alternatingGroup ↥s) ↔ k ∈ Perm.ofSubtype.range ⊓ alternatingGroup α

Tactic:
Subgroup.mem_map,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : Perm α
⊢ (∃ x ∈ alternatingGroup ↥s, Perm.ofSubtype x = k) ↔ k ∈ Perm.ofSubtype.range ⊓ alternatingGroup α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
this : G = ⊤
⊢ False

Tactic:
rw [this, Subgroup.index_top] at hG

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : 1 = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
this : G = ⊤
⊢ False
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case hmn
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
⊢ 1 ≤ k + 1

Tactic:
Nat.succ_le_succ_iff

Goal state after:
case hmn
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
⊢ 0 ≤ k
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: 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 α
⊢ 1 < ENat.card α

Tactic:
exact lt_trans (by norm_num) hsn'

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

Goal state before:
pp: 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
⊢ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1

Tactic:
← ofStabilizer.isMultiplyPretransitive

Goal state after:
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
⊢ IsMultiplyPretransitive G α (Nat.succ 1)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

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

Tactic:
← ofStabilizer.isMultiplyPretransitive

Goal state after:
case inr.left
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPretransitive M α n.succ
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 : s.encard + 1 = ↑n.succ
⊢ ∃ b, b ∈ s

Tactic:
← Set.nonempty_def,

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 : s.encard + 1 = ↑n.succ
⊢ s.Nonempty
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 α

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