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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(_root_.commutator G) ≤ Nat.card ↑(commutatorSet G)

Tactic:
rw [Subgroup.rank_congr (commutator_eq_closure G)]
  apply Subgroup.rank_closure_finite_le_nat_card

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) =
    Nat.card ↑(⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G))

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card
      ↥(closure (⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)))

Tactic:
←
    MonoidHom.map_closure,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card
      ↥(map (closureCommutatorRepresentatives G).subtype
          (closure (commutatorSet ↥(closureCommutatorRepresentatives G))))
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card
      ↥(map (closureCommutatorRepresentatives G).subtype (_root_.commutator ↥(closureCommutatorRepresentatives G)))

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : DihedralGroup n), a * b * c = a * (b * c)

Tactic:
by rintro (a | a) (b | b) (c | c) <;> simp only [(· * ·), mul] <;> ring_nf

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Star

Goal state before:
pp: A : Type u_1
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : A → A → Prop
hr : ∀ (a b : A), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : A
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star (w✝ + y✝)) (Star.star (x✝ + z✝))

Tactic:
rw [star_add, star_add]
    exact (h1.star hr).add (h2.star hr)

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) % n = 0
⊢ False

Tactic:
Nat.mod_eq_of_lt h

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) = 0
⊢ False
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ 2 ∣ n + 3

Tactic:
Nat.dvd_iff_mod_eq_zero,

Goal state after:
n : ℕ
hn : Odd n
⊢ (n + 3) % 2 = 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ reciprocalFactors 0 = [0]

Tactic:
unfold reciprocalFactors

Goal state after:
⊢ (if x : 0 = 0 then [0]
    else
      if x : 0 = 1 then []
      else if Even 0 then 3 :: reciprocalFactors (0 / 2) else 0 % 4 * 0 :: reciprocalFactors (0 / 4 + 1)) =
    [0]
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ reciprocalFactors 1 = []

Tactic:
unfold reciprocalFactors

Goal state after:
⊢ (if x : 1 = 0 then [0]
    else
      if x : 1 = 1 then []
      else if Even 1 then 3 :: reciprocalFactors (1 / 2) else 1 % 4 * 1 :: reciprocalFactors (1 / 4 + 1)) =
    []
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
⊢ MonoidHom.mrange (lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g

Tactic:
simp [mrange_eq]

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
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ t⁻¹ = id t

Tactic:
exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
x : DivisibleHull M
⊢ (a * b) • x = a • b • x

Tactic:
induction x with | mk m s
     =>  _ 

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

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
x : DivisibleHull M
⊢ 1 • x = x

Tactic:
induction x with | mk m s
     =>  _ 

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
m : M
s : ℕ+
⊢ 1 • mk m s = mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
x : DivisibleHull M
⊢ (a + b) • x = a • x + b • x

Tactic:
induction x with | mk m s
     =>  _ 

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a + b) • mk m s = a • mk m s + b • mk m s
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : 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
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : j = k
⊢ (lift f) w.prod ≠ 1

pp: case neg
ι : 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
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : ¬j = k
⊢ (lift f) w.prod ≠ 1

Tactic:
· subst hl
      change i ≠ j at hh
      have : lift f w.inv.prod ≠ 1 :=
        lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
      intro heq
      apply this
      simpa using heq

Goal state after:
case neg
ι : 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
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : ¬j = k
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: ι : Type u_1
G : Type u_2
inst✝ : Monoid G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i = orderOf (e.symm (Pi.mulSingle i (Multiplicative.ofAdd 1)))

Tactic:
simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
      using (ZMod.addOrderOf_one (n i)).symm

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 →* Mˣ
η : (G →* Mˣ) →* Mˣ
⊢ ((monoidHomMonoidHomEquiv G M).symm ((monoidHomMonoidHomEquiv G M) η)) φ = η φ

Tactic:
MulEquiv.symm_apply_apply

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)
φ : G →* Mˣ
η : (G →* Mˣ) →* Mˣ
⊢ η φ = η φ
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q ↦
            ⟨(Quotient.out q.out)⁻¹ * ↑⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ ↑⟨g, ⋯⟩ • x) q.out * Quotient.out q.out,
              ⋯⟩)
          Finset.univ.toList).prod =
    ↑(∏ i, ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out)

Tactic:
← Finset.prod_map_toList

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q ↦
            ⟨(Quotient.out q.out)⁻¹ * ↑⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ ↑⟨g, ⋯⟩ • x) q.out * Quotient.out q.out,
              ⋯⟩)
          Finset.univ.toList).prod =
    ↑(List.map (fun i ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out) Finset.univ.toList).prod
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
iso : G ≃* H
n : ℕ
φ : FreeGroup (Fin n) →* G
hφsurj : Function.Surjective ⇑φ
hNC : φ.ker.IsFinitelyNormallyGenerated
⊢ ((↑iso).comp φ).ker.IsFinitelyNormallyGenerated

Tactic:
φ.ker_mulEquiv_comp iso

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
iso : G ≃* H
n : ℕ
φ : FreeGroup (Fin n) →* G
hφsurj : Function.Surjective ⇑φ
hNC : φ.ker.IsFinitelyNormallyGenerated
⊢ φ.ker.IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.Focal

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

Tactic:
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₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
⊢ f x n = f y n

Tactic:
simpa [g] using congr_arg List.length heq

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
hd

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n

Tactic:
map_lowerCentralSeries,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ (map H.subtype ⊤).lowerCentralSeries n = H.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Subgroup G
inst✝ : Group.IsNilpotent ↥S
n : ℕ
hn : nilpotencyClass ↥S ≤ n
⊢ S.lowerCentralSeries n = ⊥

Tactic:
by
  rw [← top_subtype_lowerCentralSeries,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr hn, map_bot]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : Group.IsNilpotent H
n : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ map f (⊤.lowerCentralSeries n) = ⊥

Tactic:
map_lowerCentralSeries,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : Group.IsNilpotent H
n : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ (map f ⊤).lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ map f (⊤.lowerCentralSeries (nilpotencyClass H)) = ⊥

Tactic:
map_lowerCentralSeries,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ (map f ⊤).lowerCentralSeries (nilpotencyClass H) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
simp_rw [lowerCentralSeries_succ]
    grw [commutator_mono ih le_rfl, commutator_pi_pi_le]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : ↥ps
P : Sylow (↑p) G
this : Fact (Nat.Prime ↑p)
⊢ IsNilpotent ↥↑P

Tactic:
exact P.isPGroup'.isNilpotent

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g g' : Perm α
hg : g.IsSwap
hg' : g'.IsSwap
⊢ g * g' ∈ alternatingGroup α

Tactic:
simp [mem_alternatingGroup, map_mul, hg.sign_eq, hg'.sign_eq]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
this : orbit (↥N) a = {a}
⊢ n • a ∈ {a}

Tactic:
by rw [← this]; use n

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ B

Tactic:
by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h

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
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})

Tactic:
have h_support := hg3.support_eq_iff_mem_support.mpr ha

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)}
⊢ g ∈ ↑(closure {g | g.cycleType = {2, 2}})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.cycleType = {2, 2}
⊢ g ∈ ↑(alternatingGroup α)

Tactic:
simp [sign_of_cycleType, hg, ← Units.val_inj]

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 α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ y = g • k • g⁻¹ • y

Tactic:
← inv_smul_eq_iff,

Goal state after:
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 : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ g⁻¹ • y = k • g⁻¹ • y
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
⊢ k ∈ fixingSubgroup M s → ∃ x ∈ fixingSubgroup M t, (MulAut.conj g) x = k

Tactic:
· intro hk
    use MulAut.conj g⁻¹ k
    constructor
    · apply Set.conj_mem_fixingSubgroup _ hk
      rw [inv_smul_eq_iff, hg]
    · simp [MulAut.conj]; group

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 α
s✝ s t : Set α
g : M
hg : g • t = s
x✝¹ : ↥(fixingSubgroup M t)
x✝ : ↥(ofFixingSubgroup M t)
m : M
hm : m ∈ fixingSubgroup M t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ (match ⟨m, hm⟩ • ⟨x, hx⟩ with
    | ⟨x, hx⟩ => ⟨g • x, ⋯⟩) =
    (fixingSubgroupEquivFixingSubgroup hg) ⟨m, hm⟩ •
      match ⟨x, hx⟩ with
      | ⟨x, hx⟩ => ⟨g • x, ⋯⟩

Tactic:
simp only [← SetLike.coe_eq_coe, subgroup_smul_def,
      SetLike.val_smul,
      fixingSubgroupEquivFixingSubgroup_coe_apply,
      MulAut.conj_apply, mul_smul, inv_smul_smul]

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

Goal state before:
pp: case h.inr.inl
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
hn1 : 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
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
have ht : t.Finite := s.toFinite.inter_of_left (g • s)

Goal state after:
case h.inr.inl
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
hn1 : 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
ht : t.Finite
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
y : Fin s.ncard ↪ ↑s := ⋯
j : Fin s.ncard
i : Fin n
H : (y.trans (subtype fun x ↦ x ∈ s)) j = (x.trans (subtype fun x ↦ x ∈ ofFixingSubgroup M s)) i
⊢ ↑(x i) ∈ s

Tactic:
simp only [trans_apply, Function.Embedding.subtype_apply] at H

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
y : Fin s.ncard ↪ ↑s := (Classical.choice this).toEmbedding
j : Fin s.ncard
i : Fin n
H : ↑(y j) = ↑(x i)
⊢ ↑(x i) ∈ s
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
⊢ Fin (s.ncard + n) ↪ α

Tactic:
by
  have : Nonempty (Fin (s.ncard) ≃ s) :=
    Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
  let y := (Classical.choice this).toEmbedding
  apply Fin.Embedding.append (x := y.trans (subtype _)) (y := x.trans (subtype _))
  rw [Set.disjoint_iff_forall_ne]
  rintro _ ⟨j, rfl⟩ _ ⟨i, rfl⟩ H
  apply (x i).prop
  simp only [trans_apply, Function.Embedding.subtype_apply] at H
  simpa [H] using Subtype.coe_prop (y j)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
⊢ IsTrivialBlock B

Tactic:
rcases le_or_gt (Nat.card α) 3 with h3 | h4

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α ≤ 3
⊢ IsTrivialBlock B

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
k : ↥(alternatingGroup α)
hk✝ : k ∈ stabilizer (↥(alternatingGroup α)) sᶜ
hk : k ∈ stabilizer (↥(alternatingGroup α)) s
⊢ ∃ a, toPerm a = toPerm ⟨k, hk✝⟩

Tactic:
exact ⟨⟨⟨k, hG hk⟩, by aesop⟩, rfl⟩

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 : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
h : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
k : ↥(fixingSubgroup M s)
hk : ↑(k • ⟨b, hb'⟩) = ↑⟨x, hx'⟩
⊢ ∃ k, k • b = x

Tactic:
val_smul

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
h : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
k : ↥(fixingSubgroup M s)
hk : k • ↑⟨b, hb'⟩ = ↑⟨x, hx'⟩
⊢ ∃ k, k • b = x