mathlib-initiative/mathlib-tactics huggingface dataset:
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.den, ⋯⟩ * ↑sc * a.num) • mb < (↑⟨a.den, ⋯⟩ * ↑sb * a.num) • mc

Tactic:
[

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.DivisibleHull

Goal state before:
pp: 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, ⋯⟩ * a.num ≠ 0

Tactic:
simpa using ha.ne.symm

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ b • mk m s < c • mk m s

Tactic:
[

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ b • mk m s < c • 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
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c

Tactic:
[

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < (c - b) • a

Tactic:
[

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < (c - b) • a
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
⊢ ↑↑s • mk m s = ↑↑s' • mk m s'

Tactic:
[

Goal state after:
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
⊢ ↑↑s • mk m s = ↑↑s' • mk m s'
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
num✝¹ : M
den✝¹ : ℕ+
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝¹ den✝¹) ≤ ArchimedeanClass.mk (mk num✝ den✝)
⊢ (mk num✝¹ den✝¹).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤
    (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
[

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
num✝¹ : M
den✝¹ : ℕ+
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝¹ den✝¹) ≤ ArchimedeanClass.mk (mk num✝ den✝)
⊢ (mk num✝¹ den✝¹).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤
    (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s)

Tactic:
[

Goal state after:
case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s)
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
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ *
      ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩

Tactic:
[

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ *
      ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩
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₁ H₂ : Subgroup 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 := ⋯ }
        H₁ ≤
      { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
          invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
          left_inv := ⋯, right_inv := ⋯ }
        H₂ ↔
    H₁ ≤ H₂

Tactic:
[

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

Tactic:
[

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 ∈ (subgroupOrderIsoSubgroupMonoidHom G M).symm (OrderDual.toDual Φ) ↔ ∀ φ ∈ Φ, φ g = 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pred
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ n : ℤ
hle : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ (n - 1) • (X i)ᶜ ⊆ Y i

Tactic:
| pred n hle hi =>

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : (center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
[

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : (center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)
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✝ : (center G).FiniteIndex
a b : G
⊢ ⟨(a * b) ^ (center G).index, ⋯⟩ = ⟨a ^ (center G).index, ⋯⟩ * ⟨b ^ (center G).index, ⋯⟩

Tactic:
[

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : (center G).FiniteIndex
a b : G
⊢ ⟨(a * b) ^ (center G).index, ⋯⟩ = ⟨a ^ (center G).index, ⋯⟩ * ⟨b ^ (center G).index, ⋯⟩
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative ↥↑P
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ normalizer ↑P
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroupOf.Normal

Tactic:
rw [focalSubgroupOf_def, normal_subgroupOf_iff (focalSubgroup_le H)]
  intro n g hn hg
  induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH

Goal state after:
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ frattini G ≤ comap φ (frattini H)

Tactic:
[

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ frattini G ≤ comap φ (frattini H)
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ ⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ (⨅ a ∈ {H_1 | IsCoatom H_1}, a)

Tactic:
comap_iInf,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ ⨅ a ∈ {H | IsCoatom H}, a ≤ ⨅ i ∈ {H_1 | IsCoatom H_1}, comap φ i
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ N ↔ x✝ * y * (x✝⁻¹ * y⁻¹) ∈ N

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ N ↔ x✝ * y * (x✝⁻¹ * y⁻¹) ∈ N
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ IsNilpotent G ↔ IsNilpotent H

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ IsNilpotent G ↔ IsNilpotent H
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case h₂
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))

Tactic:
conj_conjugator_reduceCyclically

Goal state after:
case h₂
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsReduced L
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
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))
⊢ x ^ (2 * n) = y ^ (2 * n)

Tactic:
[

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
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))
⊢ x ^ (2 * n) = y ^ (2 * 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 : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨g, hg⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
[

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 : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨g, hg⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}
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])⁻¹ • ⟨g, hg⟩ • x ∈ MulAction.orbit (↑(startsWith b)) x

Tactic:
[

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])⁻¹ • ⟨g, hg⟩ • 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 : ℕ
⊢ S.lowerCentralSeries n ≤ S

Tactic:
by
  simpa using S.lowerCentralSeries_antitone (Nat.zero_le n)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊥

Tactic:
← hG

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊥

Tactic:
← hG

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n ≤ ⊤.lowerCentralSeries n
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)
⊢ I.goursatFst.prod I.goursatSnd ≤ I

Tactic:
rintro ⟨g, h⟩ ⟨hg, hh⟩
  simpa using mul_mem (mem_goursatFst.1 hg) (mem_goursatSnd.1 hh)

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✝ : IsNilpotent H
this : IsNilpotent G
⊢ ⊤.lowerCentralSeries (nilpotencyClass H + 1) = ⊥

Tactic:
refine lowerCentralSeries_succ_eq_bot ⊤
    (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

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: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ upperCentralSeries G 0 = ⊤ ↔ Subsingleton G

Tactic:
upperCentralSeries_zero,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ ⊥ = ⊤ ↔ Subsingleton G
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
have := nilpotencyClass_zero_iff_subsingleton.mp h
    exact hbase _

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)
⊢ (g, h) ∈
      ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
[

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)
⊢ (g, h) ∈
      ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
S₁ : Subgroup G₁
S₂ : Subgroup G₂
n : ℕ
ih : (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
⊢ (S₁.prod S₂).lowerCentralSeries (n + 1) = (S₁.lowerCentralSeries (n + 1)).prod (S₂.lowerCentralSeries (n + 1))

Tactic:
[

Goal state after:
case succ
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
S₁ : Subgroup G₁
S₂ : Subgroup G₂
n : ℕ
ih : (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
⊢ (S₁.prod S₂).lowerCentralSeries (n + 1) = (S₁.lowerCentralSeries (n + 1)).prod (S₂.lowerCentralSeries (n + 1))
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:
[

Goal state after:
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)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
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:
[

Goal state after:
case succ
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
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)
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ x ∈ Set.univ)

Tactic:
[

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ x ∈ Set.univ)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B

Tactic:
[

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
⊢ g₁ • B = g₂ • B

Tactic:
by_contra! hg'

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ False
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
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • 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
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
g₁ g₂ : G
a : X
ha₁ : a ∈ ⋂ i, g₁ • B i
ha₂ : a ∈ ⋂ i, g₂ • B i
⊢ ⋂ i, g₁ • B i = ⋂ i, g₂ • B i

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι) ⦃g₁ g₂ : G⦄, (g₁ • B i ∩ g₂ • B i).Nonempty → g₁ • B i = g₂ • B i
g₁ g₂ : G
a : X
ha₁ : a ∈ ⋂ i, g₁ • B i
ha₂ : a ∈ ⋂ i, g₂ • B i
⊢ ⋂ i, g₁ • B i = ⋂ i, g₂ • B i
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ¬g₁ • B = g₂ • B → Disjoint (⇑C.inclusion '' (g₁ • B)) (⇑C.inclusion '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
disjoint_image_iff C.inclusion_injective

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ¬g₁ • B = g₂ • B → Disjoint (g₁ • B) (g₂ • B) ↔ g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)