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

Goal state before:
pp: n : ℕ
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | Sum.inl j => r j
      | Sum.inr j => sr j)
    fun x ↦
    match x with
    | r j => Sum.inl j
    | sr j => Sum.inr j

Tactic:
rintro (x | x)

Goal state after:
case inl
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inl x)) =
    Sum.inl x

case inr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inr x)) =
    Sum.inr x
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r 1 ^ i.val) = n / n.gcd i.val

Tactic:
orderOf_pow,

Goal state after:
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r 1) / (orderOf (r 1)).gcd i.val = n / n.gcd i.val
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card { p // Commute p.1 p.2 }

Tactic:
refine Nat.card_le_card_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) ?_
    exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h

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

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
have hn' : NeZero n := ⟨hn.pos.ne'⟩
  simp_rw [Nat.card_congr (oddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]
  ring

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
by
  have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl
  rw [this, Set.range_comp, ← MonoidHom.map_closure (QuotientGroup.mk' _),
    FreeGroup.closure_range_of, ← MonoidHom.range_eq_map]
  exact MonoidHom.range_eq_top.2 (QuotientGroup.mk'_surjective _)

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ of ⟨i, p.head⟩.snd * (List.map (fun l ↦ of l.snd) p.tail.toList).prod = of p.head * p.tail.prod

Tactic:
prod

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ of ⟨i, p.head⟩.snd * (List.map (fun l ↦ of l.snd) p.tail.toList).prod =
    of p.head * (List.map (fun l ↦ of l.snd) p.tail.toList).prod
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

Tactic:
by
  simpa [add_comm] using cs.length_mul_le w₁⁻¹ (w₁ * w₂)

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
refine .inl (h.antisymm' ?_)
    simpa using cs.length_mul_le w (s i)

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ M.M i i' + 1 ≤ M.M i i' * 2

Tactic:
linarith [Nat.one_le_iff_ne_zero.mpr hM]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Tactic:
rw [this]

Goal state after:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : g * f y ∈ (↑U)ᶜ
hx₂ : ∀ a' ∈ (↑U)ᶜ, h (g * f y) ≤ h a'
⊢ g * f y ∉ S

Tactic:
exact notMem_of_notMem_closure hx₁

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)

Tactic:
obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
    rw [← List.getD_eq_getElem _ 1 hj, wordProd_mul_getD_rightInvSeq]
    rw [cs.length_rightInvSeq] at hj
    calc
      ℓ (π (ω.eraseIdx j))
      _ ≤ (ω.eraseIdx j).length := cs.length_wordProd_le _
      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
      _ = ℓ (π ω) := hω.symm

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
this : List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω

Tactic:
rw [this]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
n : ℕ
h : M → ℝ
b c₀ : ℝ
hb : 1 < b
H : ∀ (x : M), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
t : M
ht : t ∈ {x | IsOfFinOrder x}
this : Finite ↥(Submonoid.powers t)
⊢ t ∈ {a | h a ≤ c₀ / (b - 1)}

Tactic:
let C : ℝ := ⨆ g : Submonoid.powers t, h g

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
n : ℕ
h : M → ℝ
b c₀ : ℝ
hb : 1 < b
H : ∀ (x : M), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
t : M
ht : t ∈ {x | IsOfFinOrder x}
this : Finite ↥(Submonoid.powers t)
C : ℝ := ⨆ g, h ↑g
⊢ t ∈ {a | h a ≤ c₀ / (b - 1)}
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m

Tactic:
Rat.mul_num_den'

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

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ a • mk mb sb < a • mk mc sc

Tactic:
simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe]

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑⟨a.den, ⋯⟩ * ↑sc * a.num) • mb < (↑⟨a.den, ⋯⟩ * ↑sb * a.num) • mc
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.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ upperCentralSeries H n = ⊤

Tactic:
simp [← Subgroup.comap_top e.symm.toMonoidHom, ← h]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Tactic:
classical
  rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]

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:
treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩),

Goal state after:
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
⊢ homOfPath T (default.cons ⟨Sum.inr e, H⟩) ≫ of e = treeHom T b
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ ⊤.lowerCentralSeries n = ⊥

Tactic:
have : IsNilpotent G := ⟨n, h⟩
    rwa [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
      ← upperCentralSeries_eq_top_iff_nilpotencyClass_le]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : ℕ
ab : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
⊢ upperCentralSeries G a = upperCentralSeries G c

Tactic:
wlog ab : a < b

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
this :
  ∀ {G : Type u_1} [inst : Group G] {a b c : ℕ},
    a ≠ b →
      a ≤ c → upperCentralSeries G a = upperCentralSeries G b → a < b → upperCentralSeries G a = upperCentralSeries G c
ab : ¬a < b
⊢ upperCentralSeries G a = upperCentralSeries G c

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 c
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer ↑H' = H'

Tactic:
apply comap_injective hsur

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := ⋯
⊢ comap (mk' (center G)) (normalizer ↑H') = comap (mk' (center G)) H'
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f '' B)

pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ IsTrivialBlock (⇑f '' B)

Tactic:
· apply Or.intro_left; apply Set.Subsingleton.image hB

Goal state after:
case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ IsTrivialBlock (⇑f '' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ stabilizer G (orbit (↥H) a) → g ∈ H

pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ H → g ∈ stabilizer G (orbit (↥H) a)

Tactic:
· intro hg
    obtain ⟨-, ⟨b, rfl⟩, h⟩ := hg.symm ▸ mem_orbit_self a
    simp_rw [H.toSubmonoid.smul_def, ← mul_smul, ← mem_stabilizer_iff] at h
    exact (mul_mem_cancel_right b.2).mp (hH h)

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ H → g ∈ stabilizer G (orbit (↥H) a)
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✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
⊢ IsTrivialBlock B

Tactic:
obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
    · simp [IsTrivialBlock]
    · obtain ⟨g, hg⟩ := exists_smul_eq G b a
      rw [← IsTrivialBlock.smul_iff g]
      apply H _ (hB.translate g)
      rw [← hg]
      use b

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:
rw [this]

Goal state after:
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 ∉ {a}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind : ∀ (n : ℕ) (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hσ : l.prod ∈ alternatingGroup α
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ ∀ g ∈ l_1, g.IsSwap }
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
ha : (-1) ^ (g.cycleType.card * 2 + 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
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
pow_add,

Goal state after:
g : Perm (Fin 5)
ha : (-1) ^ (g.cycleType.card * 2) * (-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
⊢ IsConj (swap 0 4 * swap 1 3) g
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:
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.MultipleTransitivity

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

Tactic:
exact ⟨1, by simp [h]⟩

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

Goal state before:
pp: case right
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
⊢ False

Tactic:
have : Nontrivial (ofStabilizer G a) := by
      rw [← ENat.one_lt_card_iff_nontrivial]
      apply lt_of_add_lt_add_right
      rwa [ENat_card_ofStabilizer_add_one_eq]

Goal state after:
case right
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
this : Nontrivial ↥(ofStabilizer G a)
⊢ False
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 α
t : Set ↥(ofFixingSubgroup M s)
⊢ Disjoint s (Subtype.val '' t)

Tactic:
rw [Set.disjoint_iff]
  rintro a ⟨hbs, ⟨b, _, rfl⟩⟩; exact (b.prop hbs).elim

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

Goal state before:
pp: case mpr
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 : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := ⋯
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := ⋯
x : α
⊢ x ∈ insert a (Subtype.val '' t) → x ∈ s'

Tactic:
· rw [Set.mem_insert_iff]
          rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
          · simpa [s', ← hg]
          · simpa only using! hy

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
this : k = ↑g
⊢ k ∈ G

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
this : k = ↑g
⊢ ↑g ∈ G
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.right
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 α}, s.encard + 1 = ↑n.succ → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
intro s hs
      have : ∃ b : α, b ∈ s := by
        rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
        intro h
        apply not_lt.mpr hn
        rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
        simp only [← hs, zero_lt_one]
      obtain ⟨b, hb⟩ := this
      obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a
      rw [isPreprimitive_ofFixingSubgroup_conj_iff (g := g)]
      set s' := g • s with hs'
      let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s'
      have hst : s' = insert a (Subtype.val '' t) := by
        ext x
        constructor
        · intro hxs
          by_cases hxa : x = a
          · simp [hxa]
          · exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
        · rw [Set.mem_insert_iff]
          rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
          · simpa [s', ← hg]
          · simpa only using! hy
      rw [hst, isPreprimitive_fixingSubgroup_insert_iff]
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
      apply ENat.add_left_injective_of_ne_top ENat.one_ne_top
      simp only
      rw [← Nat.cast_one, ← Nat.cast_add, ← hs]
      apply congr_arg₂ _ _ rfl
      rw [show s = g⁻¹ • s' by simp [hs'],
        ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.natCast_one]
      exact notMem_val_image M t

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 : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ (s ∩ g • s)ᶜ

Tactic:
rw [Set.compl_inter]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case w
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
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⋯
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) := ⋯
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) := ⋯
y : β
hy : y ∈ ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ t

Tactic:
← hs'

Goal state after:
case w
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
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩,
    map_smul' := ⋯ }
y : β
hy : y ∈ ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ ⇑f '' s
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ alternatingGroup α ≤ G

Tactic:
apply Equiv.Perm.alternatingGroup_le_of_index_le_two

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ G.index ≤ 2