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

Goal state before:
pp: case inl
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

pp: case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
· rw [qsmul_of_nonneg h, nnqsmul_mk, ← natCast_zsmul]
    congr
    simpa using h

Goal state after:
case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)
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
p : ℕ
i j : B
h : 0 < 2 * p
⊢ 0 < (alternatingWord i j (2 * p)).length

Tactic:
simp [h]

Goal state after:
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
p : ℕ
i j : B
h : 0 < 2 * p
⊢ 0 < 2 * p

Tactic:
simp [h]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
⊢ (lift f) w.prod ≠ 1

Tactic:
intro heq1
  have : X k ⊆ X i := by simpa [heq1] using lift_word_ping_pong f X hpp w hlast.symm
  obtain ⟨x, hx⟩ := hXnonempty k
  exact (hXdisj hhead).le_bot ⟨hx, this hx⟩

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ (↑sa * (↑sc * ↑sb)) • ma + (↑sa * (↑sc * ↑sa)) • mb < (↑sa * (↑sb * ↑sc)) • ma + (↑sa * (↑sb * ↑sa)) • mc

Tactic:
convert! this using 3

Goal state after:
case e'_3.e'_5
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sc * ↑sb) = ↑sa * ↑sb * ↑sc

case e'_3.e'_6
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sc * ↑sa) = ↑sa * ↑sa * ↑sc

case e'_4.e'_5
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sb * ↑sc) = ↑sa * ↑sb * ↑sc

case e'_4.e'_6
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sb * ↑sa) = ↑sa * ↑sa * ↑sb
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : x = ↑a * q
⊢ x = ↑a * q * 1

Tactic:
by simpa using ha

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
g g' : G
h : g = g'
⊢ ∀ (φ : G →* Mˣ), φ g = φ g'

Tactic:
simp [h]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
⊢ (fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker)
      ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ) =
    Φ

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ)) := by
      rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ (fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker)
      ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ) =
    Φ
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (H.quotientEquivSigmaZMod g).symm ⟨((H.quotientEquivSigmaZMod g) q).fst, ((H.quotientEquivSigmaZMod g) q).snd⟩ = q

Tactic:
Sigma.eta,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (H.quotientEquivSigmaZMod g).symm ((H.quotientEquivSigmaZMod g) q) = q
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ ⊤ ≤ f.range

Tactic:
← hS2,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ closure ↑S ≤ f.range
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ ⊥.IsFinitelyNormallyGenerated

Tactic:
exact .bot

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Bijective ⇑((transferSylow P hP).domRestrict ↑P)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
rw [Function.Bijective, ← range_eq_top, domRestrict_range] at hf

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).domRestrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ (transferSylow P hP).ker.IsComplement' ↑P
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₂ = []
⊢ (replicate (n + 1) L₂).flatten ≠ []

Tactic:
simp [h]

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

Goal state before:
pp: case isTrue
α : 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])

pp: case isFalse
α : 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 :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])

Tactic:
case isTrue h =>
      nth_rw 4 [← eq]
      simp [invRev, h.1.symm, h.2.symm]

Goal state after:
case isFalse
α : 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 :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
a b : G
ha : a ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
hb : b ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅a * b, y⁆ ∈ N

Tactic:
convert! Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y) using 1
    group

Goal state after:
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:
by
  rw [nilpotent_iff_finite_descending_central_series]
  refine ⟨?_, ?_⟩
  · 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]
  · rintro ⟨n, hn⟩
    refine ⟨n, lowerCentralSeries ⊤, lowerCentralSeries_isDescendingCentralSeries, ?_⟩
    rwa [← map_subtype_inj, map_bot, top_subtype_lowerCentralSeries]

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

Goal state before:
pp: case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    treeHom T b

Tactic:
· rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]
    simp only [IsIso.inv_hom_id, Category.comp_id, Category.assoc, treeHom]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

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

Tactic:
swap

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

case pos
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
h : nilpotencyClass G = n
⊢ P G

Tactic:
induction n generalizing G with

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mpr
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
g : G
h : H
⊢ ∀ (x : H) (h_1 : (g, x) ∈ I) (x_1 : G) (h_2 : (x_1, h) ∈ I) (x_2 : G) (x_3 : H) (x_4 : (x_2, x_3) ∈ I),
    P ⟨(x_2, x_3), ⋯⟩ = ⟨g, ⋯⟩ → Q ⟨(x_2, x_3), ⋯⟩ = ⟨h, ⋯⟩ → (g, h) ∈ I

Tactic:
rintro h₁ hgh₁ g₁ hg₁h g₂ h₂ hg₂h₂ hP hQ

Goal state after:
case mpr
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
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : P ⟨(g₂, h₂), ⋯⟩ = ⟨g, ⋯⟩
hQ : Q ⟨(g₂, h₂), ⋯⟩ = ⟨h, ⋯⟩
⊢ (g, h) ∈ I
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)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
⊢ ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B

Tactic:
intro B

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
B : Set X
⊢ a ∈ B → IsBlock G B → IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ ENat.card ↥(ofStabilizer G a) + 1 = ENat.card α

Tactic:
dsimp only [ENat.card]
  rw [← Cardinal.mk_sum_compl {a}, map_add, add_comm, eq_comm]
  congr
  simp

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 α
s : Set α
⊢ stabilizer G sᶜ = stabilizer G s

Tactic:
by
  have (s : Set α) : stabilizer G s ≤ stabilizer G (sᶜ) := by
    intro g h
    simp [Set.smul_set_compl, mem_stabilizer_iff.1 h]
  refine le_antisymm (le_of_le_of_eq (this _) ?_) (this _)
  rw [compl_compl]

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})

Tactic:
have : 1 < g.supportᶜ.card := by grind [Finset.card_compl, Nat.card_eq_fintype_card]

Goal state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
h : 3 ∈ g.cycleType
⊢ (g * g).IsThreeCycle

Tactic:
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h

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: 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
⊢ n ∣ 2

Tactic:
le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)

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
n : ℕ
hn : n ∈ g'.cycleType
⊢ n ∣ n

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
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
ha : Even g.cycleType.card
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

pp: g : Perm (Fin 5)
ha : (-1) ^ g.cycleType.card = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ -1 ≠ 1

Tactic:
swap

Goal state after:
g : Perm (Fin 5)
ha : (-1) ^ g.cycleType.card = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ -1 ≠ 1

g : Perm (Fin 5)
ha : Even g.cycleType.card
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
v : F
h'x : x ∈ (trivializationAt F E x).baseSet
⊢ (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
        Trivialization.symmL ℝ (trivializationAt F E x) x)
      v =
    (ContinuousLinearMap.id ℝ F) v

Tactic:
simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      mem_baseSet_trivializationAt, comp_apply, id_apply]

Goal state after:
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
v : F
h'x : x ∈ (trivializationAt F E x).baseSet
⊢ (Trivialization.linearMapAt ℝ (trivializationAt F E x) x) ((trivializationAt F E x).symm x v) = v
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : a = b
⊢ 1 • a = b

Tactic:
simp [h]

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 α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
⊢ ∀ {B : Set α}, IsBlock G B → IsTrivialBlock B

Tactic:
intro B

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
⊢ IsBlock G B → IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: 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

Tactic:
exact index_eq_one.mp h ▸ le_top

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

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Injective ⇑(ofFixingSubgroup_insert_map a s)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
    simpa only [← Subtype.coe_inj, ofFixingSubgroup_insert_map_apply] using h

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Bijective ⇑(ofFixingSubgroup_insert_map a s)

Tactic:
constructor
  · rintro ⟨x, hx⟩ ⟨y, hy⟩ h
    simpa only [← Subtype.coe_inj, ofFixingSubgroup_insert_map_apply] using h
  · rintro ⟨⟨x, hx1⟩, hx2⟩
    exact ⟨⟨x, mem_ofFixingSubgroup_insert_iff.mpr ⟨hx1, hx2⟩⟩, rfl⟩

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 α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
⊢ t.ncard ≠ 0

Tactic:
← Nat.pos_iff_ne_zero,

Goal state after:
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 α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
⊢ 0 < t.ncard
Module: Mathlib.GroupTheory.GroupAction.Period

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ BddAbove (Set.range fun a ↦ period m a)

Tactic:
by
  use Monoid.exponent M
  simpa [upperBounds] using period_le_exponent exp_pos _

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

Goal state before:
pp: case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ (k * g) • a = x

Tactic:
rw [mul_smul, hgab, hk]

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
t : Set α
ht : ∃ a b, a ∈ t ∧ b ∈ t ∧ a ≠ b
⊢ ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := ht

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
⊢ ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ ⟨Perm.ofSubtype g, ⋯⟩ ∈ stabilizer (↥(alternatingGroup α)) s

Tactic:
rw [mem_stabilizer_iff, Submonoid.mk_smul]

Goal state after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ Perm.ofSubtype g • s = s