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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)

Tactic:
intro ht

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of
        (have __src := (equivPair i✝) w✝;
          { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).head *
      (have __src := (equivPair i✝) w✝;
          { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.prod =
    of m✝ * w✝.prod

Tactic:
of.map_mul,

Goal state after:
case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * of ((equivPair i✝) w✝).head *
      (have __src := (equivPair i✝) w✝;
          { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.prod =
    of m✝ * w✝.prod
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : _w₁✝.toList ≠ []
_w₂_ih✝ : _w₂✝.toList ≠ []
⊢ (_w₁✝.append _hne✝ _w₂✝).toList ≠ []

Tactic:
apply List.append_ne_nil_of_left_ne_nil

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : _w₁✝.toList ≠ []
_w₂_ih✝ : _w₂✝.toList ≠ []
⊢ _w₁✝.toList ≠ []
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✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
⊢ ∀ l ∈ (_w₁✝.append _hne✝ _w₂✝).toList, l.snd ≠ 1

Tactic:
intro l

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✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
⊢ l ∈ (_w₁✝.append _hne✝ _w₂✝).toList → l.snd ≠ 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ drop j (cs.rightInvSeq ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))

Tactic:
rightInvSeq,

Goal state after:
case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ drop j (cs.rightInvSeq ω) = drop (j + 1) ((cs.wordProd ω)⁻¹ * cs.simple k * cs.wordProd ω :: cs.rightInvSeq ω)
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 c : DivisibleHull M
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
by
    induction a with | mk ma sa
    induction b with | mk mb sb
    induction c with | mk mc sc
    rw [mk_le_mk] at ⊢ hab hbc
    rw [← nsmul_le_nsmul_iff_right (show sb.val ≠ 0 by simp), smul_comm _ _ ma, smul_comm _ _ mc]
    rw [← nsmul_le_nsmul_iff_right (show sc.val ≠ 0 by simp), smul_comm _ _ mb] at hab
    rw [← nsmul_le_nsmul_iff_right (show sa.val ≠ 0 by simp)] at hbc
    exact hab.trans hbc

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ArchimedeanClass.mk (mk m s) = (archimedeanClassOrderHom M) (ArchimedeanClass.mk m)

Tactic:
rw [archimedeanClassOrderHom, ArchimedeanClass.orderHom_mk, coeOrderAddMonoidHom_apply]
  apply archimedeanClassMk_mk_eq

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relIndex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ Group.rank ↥((center G).subgroupOf (_root_.commutator G))

Tactic:
apply card_dvd_exponent_pow_rank'

Goal state after:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relIndex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : ↥((center G).subgroupOf (_root_.commutator G))), g ^ (center G).index = 1
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
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)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
exact MonoidHom.ker_transferSylow_isComplement' P (hP.normalizer_le_centralizer rfl)

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : b.1 = a.1 ∧ (!b.2) = a.2
⊢ a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) = a :: (l ++ [b])

Tactic:
nth_rw 4 [← eq]

Goal state after:
α : Type u
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h : b.1 = a.1 ∧ (!b.2) = a.2
⊢ a :: conjugator l ++ reduceCyclically l ++ invRev (a :: conjugator l) =
    a :: (conjugator l ++ reduceCyclically l ++ invRev (conjugator l) ++ [b])
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ Group.IsNilpotent ↥S ↔ ∃ n, S.lowerCentralSeries n = ⊥

Tactic:
nilpotent_iff_finite_descending_central_series

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

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1

Tactic:
zero_tsub,

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = 0
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hH : ¬IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

Tactic:
rw [nilpotencyClass_of_not_nilpotent hH, zero_tsub, nilpotencyClass_of_not_nilpotent]
    exact mt of_quotient_center_nilpotent hH

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ center G = ⊤

Tactic:
rw [← upperCentralSeries_one]
    exact upperCentralSeries_eq_top_iff_nilpotencyClass_le.mpr h

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G a ≤ upperCentralSeries G (a + 1)

pp: case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a

Tactic:
· exact upperCentralSeries_mono _ <| Nat.le_succ ..

Goal state after:
case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (g • B) (s • B)

Tactic:
← iUnion_smul_set,

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (g • B) (⋃ a ∈ s, a • B)
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 ∈ ↑⟨stabilizer G B', ⋯⟩

Tactic:
apply hB'.smul_eq_of_mem ha'

Goal state after:
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'
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * 0 → l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
intro l

Goal state after:
case zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
⊢ (∀ g ∈ l, g.IsSwap) → l.length = 2 * 0 → l.prod ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
⊢ ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * (n + 1) → l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
intro l

Goal state after:
case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
l : List (Perm α)
⊢ (∀ g ∈ l, g.IsSwap) → l.length = 2 * (n + 1) → l.prod ∈ closure {σ | σ.IsThreeCycle}
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
⊢ (c * g' * (c * g')).IsThreeCycle

Tactic:
simp only [mul_assoc]

Goal state after:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * (c * g'))).IsThreeCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
Subgroup.mem_inf,

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 ∧ k ∈ alternatingGroup α
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

Tactic:
by
  constructor
  · intro _ a b c d h h'
    obtain ⟨m, e⟩ := exists_smul_eq (M := G) (embFinTwo h) (embFinTwo h')
    exact ⟨m,
      by rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero],
      by rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]⟩
  · intro H
    constructor
    intro j j'
    obtain ⟨g, h, h'⟩ :=
      H (j.injective.ne_iff.mpr Fin.zero_ne_one) (j'.injective.ne_iff.mpr Fin.zero_ne_one)
    use g
    ext i
    by_cases hi : i = 0
    · simp [hi, h]
    · simp [eq_one_of_ne_zero i hi, h']

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

Goal state before:
pp: case h.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ (MulAut.conj g⁻¹) k ∈ fixingSubgroup M t

pp: case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ (MulAut.conj g) ((MulAut.conj g⁻¹) k) = k

Tactic:
· apply Set.conj_mem_fixingSubgroup _ hk
      rw [inv_smul_eq_iff, hg]

Goal state after:
case h.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ (MulAut.conj g) ((MulAut.conj g⁻¹) k) = k
Module: Mathlib.GroupTheory.GroupAction.Period

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ period g⁻¹ a = period g a

Tactic:
by
  simp only [period_eq_minimalPeriod, Function.minimalPeriod_eq_minimalPeriod_iff,
    isPeriodicPt_smul_iff]
  intro n
  rw [smul_eq_iff_eq_inv_smul, eq_comm, ← zpow_natCast, inv_zpow, inv_inv, zpow_natCast]

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

Goal state before:
pp: case right.hf.left
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⋯
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) := ⋯
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := ⋯
⊢ Function.Injective ⇑g

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
        suffices f x = f y by
          simpa [← Subtype.coe_inj, hf.injective.eq_iff] using! this
        simpa only [g, ← Subtype.coe_inj] using! h

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.ncard = 2
x✝ : Finite α
⊢ Nat.card α = 2

Tactic:
ncard_univ

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α : ↑(Nat.card α) = 2
x✝ : Finite α
⊢ Nat.card α = 2
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 α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
this : IsPreprimitive ↥(stabilizer M s) ↑s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)

Tactic:
apply this.isTrivialBlock_of_isBlock

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
this : IsPreprimitive ↥(stabilizer M s) ↑s
⊢ IsBlock (↥(stabilizer M s)) (Subtype.val ⁻¹' B)
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
this : IsTrivialBlock (Subtype.val ⁻¹' B)
⊢ B.Subsingleton

Tactic:
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:
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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)

Tactic:
apply this.isTrivialBlock_of_isBlock

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
this : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
⊢ IsBlock (↥(stabilizer (↥G) s)) (Subtype.val ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.Support

Goal state before:
pp: case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
⊢ g' • a = a

Tactic:
have := Set.forall_mem_image.1 hg' ha

Goal state after:
case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
this : g' • g • a = g • a
⊢ g' • a = a
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
    by_cases hn : n ≤ 2
    · apply MulAction.isMultiplyPretransitive_of_le' hn
      simp [← hα]
    · suffices (IsEmpty (Fin n ↪ α)) by infer_instance
      rwa [← not_nonempty_iff, Function.Embedding.nonempty_iff_card_le, Fintype.card_fin,
        ← Nat.card_eq_fintype_card, hα]

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

Goal state before:
pp: 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
⊢ Nat.card α = g.support.card + (n + 1)

Tactic:
card_support_eq_two.mpr h2g,

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
⊢ Nat.card α = 2 + (n + 1)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n✝ n : ℕ
⊢ H.lowerCentralSeries (n + 1) = H

Tactic:
Subgroup.lowerCentralSeries_succ,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n✝ n : ℕ
⊢ ⁅H.lowerCentralSeries n, H⁆ = H
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e : ↥s
he : ↑e * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑e * (↑(a₁, a₂).2 * (b₁, b₂).1)
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
obtain ⟨f, hf⟩ := r_iff_exists.1 hcd

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e : ↥s
he : ↑e * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑e * (↑(a₁, a₂).2 * (b₁, b₂).1)
f : ↥s
hf : ↑f * (↑(d₁, d₂).2 * (c₁, c₂).1) = ↑f * (↑(c₁, c₂).2 * (d₁, d₂).1)
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e : ↥s
he : ↑e * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑e * (↑(a₁, a₂).2 * (b₁, b₂).1)
⊢ ↑c₂ * a₁ < ↑a₂ * c₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁

Tactic:
obtain ⟨f, hf⟩ := r_iff_exists.1 hcd

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e : ↥s
he : ↑e * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑e * (↑(a₁, a₂).2 * (b₁, b₂).1)
f : ↥s
hf : ↑f * (↑(d₁, d₂).2 * (c₁, c₂).1) = ↑f * (↑(c₁, c₂).2 * (d₁, d₂).1)
⊢ ↑c₂ * a₁ < ↑a₂ * c₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : (A.subgroupOf B).Normal
ih : (map K.subtype B).IsSubnormal
⊢ (map K.subtype A).IsSubnormal

Tactic:
| step A B h_le hSubn hN ih =>

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

Goal state before:
pp: α : 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
⊢ ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α

Tactic:
intro l

Goal state after:
α : 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
l : List ℕ
⊢ l ∈ c.ranges → ∀ n ∈ l, n < Fintype.card α