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

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝ : Group G
b : FreeGroupBasis ι G
i : ι
⊢ b.repr (b i) = FreeGroup.of i

Tactic:
by
  change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i
  simp

Goal state after:
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
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ f.comp g₁ = (lift (f.comp g₁) (f.comp g₂)).comp inl

Tactic:
lift_comp_inl

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ f.comp g₁ = f.comp g₁
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (Units.coeHom G)
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm (PresentedGroup.of i)))) =
    ↑f i

Tactic:
← MonoidHom.toFun_eq_coe,

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (↑(Units.coeHom G)).toFun
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm (PresentedGroup.of i)))) =
    ↑f i
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case mul_simple_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ ∃ a, cs.wordProd a = cs.simple i * cs.wordProd ω

Tactic:
use i :: ω

Goal state after:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) = i :: take k (alternatingWord j i (2 * p))

Tactic:
by
  rw [listTake_alternatingWord j i p k (by lia), listTake_alternatingWord i j p (k + 1) h]
  by_cases h_even : Even k
  · simp [Nat.not_even_iff_odd.mpr (Even.add_one h_even), alternatingWord_succ', h_even]
  · simp [(by rw [Nat.not_even_iff_odd] at h_even; exact Odd.add_one h_even : Even (k + 1)),
      alternatingWord_succ', h_even]

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

Goal state before:
pp: case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)

Tactic:
if_pos (by use k; ring),

Goal state after:
case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Tactic:
rw [(by ring : ↑(M i i') * 2 - (2 * k + 1) = -1 + (-k + ↑(M i i')) * 2),
      (by ring : 2 * k + 1 = 1 + k * 2)]

Goal state after:
case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((1 + k * 2) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + ↑(M.M i i')) * 2) / 2)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ (m • empty).prod = m

Tactic:
rw [prod_smul, prod_empty, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ mk m1 s + mk m2 s = mk (m1 + m2) s

Tactic:
rw [mk_add_mk, mk_eq_mk]
  exact ⟨1, by simp [smul_smul]⟩

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset a ↑H ↑K) (doubleCoset b ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K

Tactic:
disjoint_comm

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b ↑H ↑K) (doubleCoset a ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ b = b * a⁻¹ * a * 1

Tactic:
by rw [mul_one, inv_mul_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inl
ι : 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
hcard : 3 ≤ #ι
⊢ (lift f) w.prod ≠ 1

Tactic:
obtain ⟨i, h1, h2⟩ := Cardinal.exists_ne_ne_of_three_le hcard i j

Goal state after:
case inl
ι : 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
hcard : 3 ≤ #ι
i : ι
h1 : i ≠ i✝
h2 : i ≠ j
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a✝ : Finite (Quotient ↑H ↑K)
val✝ : Fintype (Quotient ↑H ↑K)
⊢ ⋃ i ∈ Finset.univ, quotToDoubleCoset H K i = Set.univ

Tactic:
by simpa using! iUnion_quotToDoubleCoset _ _

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:
by
  rw [archimedeanClassOrderHom, ArchimedeanClass.orderHom_mk, coeOrderAddMonoidHom_apply]
  apply archimedeanClassMk_mk_eq

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
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi : e a i ≠ 1
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e

Goal state after:
case h
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := ⋯
i : ι
hi : e a i ≠ 1
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ((φi.comp (Pi.evalMonoidHom (fun i ↦ Multiplicative (ZMod (n i))) i)).comp ↑e) a ≠ 1
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ (1 + ⟨q, -1 + id k⟩.snd.cast) * Quotient.out (Quotient.out ⟨q, -1 + id k⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
id,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ (1 + ⟨q, -1 + k⟩.snd.cast) * Quotient.out (Quotient.out ⟨q, -1 + k⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)
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
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ ϕ.transfer g = diff ϕ T (g • T)

Tactic:
by
  rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff] <;> rfl

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

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

Tactic:
exact (h₁.flatten_replicate _).isReduced

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

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

Tactic:
exact (h₁.flatten_replicate _).isReduced

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑(S.lowerCentralSeries n)

Tactic:
exact S.self_le_normalizer_lowerCentralSeries n

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: 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 : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst) g, (QuotientGroup.mk' (P.prod Q).range.goursatSnd) h) = 1 ↔
    g ∈ (P.prod Q).range.goursatFst ∧ h ∈ (P.prod Q).range.goursatSnd

Tactic:
Prod.one_eq_mk,

Goal state after:
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 : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst) g, (QuotientGroup.mk' (P.prod Q).range.goursatSnd) h) = (1, 1) ↔
    g ∈ (P.prod Q).range.goursatFst ∧ h ∈ (P.prod Q).range.goursatSnd
Module: Mathlib.GroupTheory.GroupAction.Blocks

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

pp: case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x ↦ orbit G x

Tactic:
· intro x
    exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩

Goal state after:
case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x ↦ orbit G x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ a ∈ g • B

Tactic:
by rwa [← hg, smul_mem_smul_set_iff]

Goal state after:
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
⊢ g ∈ ↑⟨stabilizer G B, ⋯⟩ → g ∈ ↑⟨stabilizer G B', ⋯⟩

Tactic:
hgB

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 ∈ ↑⟨stabilizer G B', ⋯⟩
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inl
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
hB : IsBlock G ∅
⊢ IsTrivialBlock ∅

Tactic:
simp [IsTrivialBlock]

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

Goal state before:
pp: case inl
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
hB : IsBlock G ∅
⊢ IsTrivialBlock ∅

Tactic:
simp [IsTrivialBlock]

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

Goal state before:
pp: M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β

Tactic:
constructor
  · intro _
    apply IsPreprimitive.of_surjective hf.surjective
  · intro _
    have := (isPretransitive_congr hφ hf).mpr toIsPretransitive
    exact {
      isTrivialBlock_of_isBlock {B} hB := by
        rw [← Set.preimage_image_eq B hf.injective]
        exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective)) }

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

Goal state before:
pp: case inl
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B = ∅
⊢ IsTrivialBlock B

pp: case inr
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
⊢ IsTrivialBlock B

Tactic:
· simp [IsTrivialBlock, hB']

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ B

Tactic:
by rw [hga]; exact ha

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

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this✝ : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := ⋯
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := ⋯
hy : y' = append y
g : G
hg : g • x' = y'
this : g ∈ fixingSubgroup G s
i : Fin m
⊢ ↑((⟨g, this⟩ • x) i) = ↑(y i)

Tactic:
smul_apply,

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this✝ : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
this : g ∈ fixingSubgroup G s
i : Fin m
⊢ ↑(⟨g, this⟩ • x i) = ↑(y i)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • (append x) (castAdd m i) = (g • x') (castAdd m i)

Tactic:
smul_apply,

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • (append x) (castAdd m i) = g • x' (castAdd m i)
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 α
a : α
s : Set ↥(ofStabilizer M a)
m : ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
x✝ : ↑s
x : ↥(ofStabilizer M a)
hx : x ∈ s
⊢ ⟨↑m, ⋯⟩ • ↑⟨x, hx⟩ = ↑⟨x, hx⟩

Tactic:
by
        simp only [← SetLike.coe_eq_coe]
        refine (mem_fixingSubgroup_iff M).mp m.prop _ (Set.mem_insert_of_mem a ?_)
        exact ⟨⟨x, (SubMulAction.mem_ofStabilizer_iff  M a).mp x.prop⟩, hx, rfl⟩

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

Goal state before:
pp: case inr.inr
α : 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'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

Tactic:
rw [← hxj]

Goal state after:
case inr.inr
α : 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'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (k • x) j = (k • x) i
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 : 1 < t.encard
⊢ ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t

Tactic:
Set.one_lt_encard_iff

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

Goal state before:
pp: case h
α : 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
⊢ toPerm ⟨⟨Perm.ofSubtype g * k, ⋯⟩, ⋯⟩ = g

Tactic:
· ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop

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 α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
this : IsTrivialBlock (Subtype.val ⁻¹' B)
⊢ ¬{x | x ∈ s} ⊆ B

Tactic:
exact not_subset_of_ssubset hB_ss_sc

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ False

Tactic:
by
    apply compl_ne_univ.mpr h0.nonempty -- `sᶜ ≠ univ`
    apply hsc.eq_univ_of_card_lt
    grind

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

Goal state before:
pp: case pos
α : 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
hn : n ≤ 2
⊢ ↑2 ≤ ENat.card α

Tactic:
simp [← hα]

Goal state after: