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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * ↑f.range = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h (f x)
U : Subgroup G
u : G
hu : u ∈ Subgroup.map f U
⊢ u ∈ U

Tactic:
obtain ⟨u', hu₁, rfl⟩ := mem_map.mp hu
    exact U.pow_mem hu₁ n

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
⊢ (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
induction ω with

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
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω

Tactic:
← reverse_reverse ω

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 ω.reverse.reverse
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)
H : Subgroup G
this✝ : Fintype ↥H
this : HasEnoughRootsOfUnity M (Monoid.exponent ↥H)
⊢ Function.Surjective ⇑(domRestrictHom H Mˣ)

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H

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)
H : Subgroup G
this✝¹ : Fintype ↥H
this✝ : HasEnoughRootsOfUnity M (Monoid.exponent ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ Function.Surjective ⇑(domRestrictHom H Mˣ)
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)
H : Subgroup G
x : G
⊢ (∀ (φ : G →* Mˣ), (∀ y ∈ H, φ y = 1) → φ x = 1) ↔ x ∈ H

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H

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)
H : Subgroup G
x : G
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ (∀ (φ : G →* Mˣ), (∀ y ∈ H, φ y = 1) → φ x = 1) ↔ x ∈ H
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)
H : Subgroup G
⊢ Nat.card ↥(domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H

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)
H : Subgroup G
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ Nat.card ↥(domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: case refine_2
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ Nat.card G = Nat.card ((G →* Mˣ) →* Mˣ)

Tactic:
· rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity]

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ˣ)
g : G
⊢ g ∈
      { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
            invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
            left_inv := ⋯, right_inv := ⋯ }.symm
        (OrderDual.toDual Φ) ↔
    ∀ φ ∈ Φ, φ g = 1

Tactic:
Equiv.coe_fn_symm_mk,

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ˣ)
g : G
⊢ g ∈ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual (OrderDual.toDual Φ)) Mˣ).ker ↔
    ∀ φ ∈ Φ, φ g = 1
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
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))
hk : ¬k = 0
⊢ (g ^ if k = 0 then ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) else k.cast) *
      Quotient.out (Quotient.out ⟨q, k - 1⟩.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:
rw [if_neg hk, if_neg hk]

Goal state after:
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
⊢ (fun a ↦ ↑a)
      (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 =
    (fun a ↦ ↑a) ⟨g ^ H.index, ⋯⟩

Tactic:
dsimp only

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 =
    g ^ H.index
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
⊢ normalizer ↑P ≤ centralizer ↑P

Tactic:
have := (Nat.card_eq_one_iff_unique.mp hn).1

Goal state after:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ normalizer ↑P ≤ centralizer ↑P
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroupOf = closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}

Tactic:
rw [← map_subtype_inj, map_focalSubgroupOf, MonoidHom.map_closure, focalSubgroup_def]
  congr
  simp
  grind

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
have := (Nat.card_eq_one_iff_unique.mp hn).1

Goal state after:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
⊢ reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
induction n

Goal state after:
case zero
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ reduce (replicate (0 + 1) L).flatten =
    conjugator L ++ (replicate (0 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

case succ
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n✝ : ℕ
a✝ :
  reduce (replicate (n✝ + 1) L).flatten =
    conjugator L ++ (replicate (n✝ + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
⊢ reduce (replicate (n✝ + 1 + 1) L).flatten =
    conjugator L ++ (replicate (n✝ + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ = 1 ↔ y * x✝ = x✝ * y

Tactic:
mul_inv_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ x✝ * y * x✝⁻¹ = y ↔ y * x✝ = x✝ * y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
n : ℕ
⊢ comap (↑e) (upperCentralSeries G (n + 1)) = upperCentralSeries H (n + 1)

Tactic:
by
    ext
    simp [mem_upperCentralSeries_succ_iff, ← comap_upperCentralSeries e n,
      ← e.toEquiv.forall_congr_right, commutatorElement_def]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m ↦ H (n - m)) n = ⊥

Tactic:
dsimp only

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ (fun m ↦ H (n - m)) n = ⊤

Tactic:
dsimp only

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m ↦ H (n - m)) n = ⊥

Tactic:
dsimp only

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ (fun m ↦ H (n - m)) n = ⊤

Tactic:
dsimp only

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ (mk [w])⁻¹ • ⟨mk (w :: b :: l), ⋯⟩ • x ∈ MulAction.orbit (↑(startsWith b)) x

Tactic:
← List.singleton_append (l := b :: l),

Goal state after:
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ (mk [w])⁻¹ • ⟨mk ([w] ++ b :: l), ⋯⟩ • x ∈ MulAction.orbit (↑(startsWith b)) x
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ y * z * (z * y)⁻¹ = 1

Tactic:
mul_inv_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ y * z = z * y
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, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
Subgroup.mem_prod,

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 ↔
    g ∈ (P.prod Q).range.goursatFst ∧ h ∈ (P.prod Q).range.goursatSnd
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
htGX : IsPretransitive G X
a : X
⊢ ∀ {a_1 b : { B // a ∈ B ∧ IsBlock G B }},
    {
            toFun := fun x ↦
              match x with
              | ⟨B, ⋯⟩ => ⟨stabilizer G B, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨H, hH⟩ => ⟨orbit (↥H) a, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          a_1 ≤
        {
            toFun := fun x ↦
              match x with
              | ⟨B, ⋯⟩ => ⟨stabilizer G B, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨H, hH⟩ => ⟨orbit (↥H) a, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a_1 ≤ b

Tactic:
rintro ⟨B, ha, hB⟩

Goal state after:
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 : { B // a ∈ B ∧ IsBlock G B }},
    {
            toFun := fun x ↦
              match x with
              | ⟨B, ⋯⟩ => ⟨stabilizer G B, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨H, hH⟩ => ⟨orbit (↥H) a, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          ⟨B, ⋯⟩ ≤
        {
            toFun := fun x ↦
              match x with
              | ⟨B, ⋯⟩ => ⟨stabilizer G B, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨H, hH⟩ => ⟨orbit (↥H) a, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      ⟨B, ⋯⟩ ≤ b
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
a : X
⊢ ∀ (a_1 : BlockMem G a), a_1 ≤ ⟨univ, ⋯⟩

Tactic:
rintro ⟨B, ha, hB⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
⊢ ⟨B, ⋯⟩ ≤ ⟨univ, ⋯⟩
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
a : X
⊢ ∀ (a_1 : BlockMem G a), ⟨{a}, ⋯⟩ ≤ a_1

Tactic:
rintro ⟨B, ha, hB⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
⊢ ⟨{a}, ⋯⟩ ≤ ⟨B, ⋯⟩
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
rw [← hgkB', hkB']

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

Goal state before:
pp: case h.inl
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
H : ∀ (i : Fin n), (Fin.Embedding.init (g • x)) i ∈ ofStabilizer G a
i : Fin n
⊢ (g • x) i.castSucc = (ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a)) (Fin.Embedding.init (g • x)) H)) i.castSucc

Tactic:
simpa [ofStabilizer.snoc] using!
      Subtype.ext_iff.mp <| Function.Embedding.codRestrict_apply _ _ H i

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 α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : g • j 0 = j' 0
h' : g • j 1 = j' 1
i : Fin 2
hi : i = 0
⊢ (g • j) i = j' i

Tactic:
simp [hi, 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 hB

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 α
hB : IsBlock G B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case hmn
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ 1 ≤ k + 1

Tactic:
rw [Nat.succ_le_succ_iff]

Goal state after:
case hmn
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ 0 ≤ k
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 α
inst✝ : Finite α
hs : IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
have := IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs.toIsPretransitive ha

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
inst✝ : Finite α
hs : IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: 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 : ∀ (a b : α) (g : M), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : M
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x ↦ g • x) a = b
⊢ b ∈ s

Tactic:
by_contra hb

Goal state after:
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 : ∀ (a b : α) (g : M), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : M
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x ↦ g • x) a = b
hb : b ∉ s
⊢ False
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ∃ g ∈ stabilizer (Perm α) s, g • a = b

Tactic:
classical
  exact ⟨swap a b, swap_mem_stabilizer ha hb, swap_apply_left a b⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
by_cases ht : 2 < t.ncard

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : 2 < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
⊢ ∀ {B : Set α}, IsBlock (↥G) B → IsTrivialBlock B

Tactic:
intro B hB

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case right
α : 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 α}, IsBlock (↥G) B → IsTrivialBlock B

Tactic:
intro B hB

Goal state after:
case right
α : 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
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
n : ℕ
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
⊢ IsMultiplyPreprimitive G α (n + 2)

Tactic:
induction n generalizing α hα G with

Goal state after: