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

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ H.index ∈ H

Tactic:
classical
    replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
      (congr_arg (· ∈ H) (key k g₀ hk)).mp hk
    replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod (g • ·) q ∈ H := fun q =>
      key (Function.minimalPeriod (g • ·) q) q.out
        (QuotientGroup.out_conj_pow_minimalPeriod_mem H g q)
    let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
      (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod (g • ·) q.out
    have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out
    replace key :=
      Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
    simpa only [f, Finset.prod_pow_eq_pow_sum, index_eq_sum_minimalPeriod H g] using! key

Goal state after:
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
⊢ g * φ g = 1

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
⊢ g * φ g = 1
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case mul
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x✝ y✝ : G
hx✝ : x✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
hy✝ : y✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
IHa : g * x✝ * g⁻¹ ∈ H.focalSubgroup
IHb : g * y✝ * g⁻¹ ∈ H.focalSubgroup
⊢ g * (x✝ * y✝) * g⁻¹ ∈ H.focalSubgroup

Tactic:
simpa using

Goal state after:
case mul
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x✝ y✝ : G
hx✝ : x✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
hy✝ : y✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
IHa : g * x✝ * g⁻¹ ∈ H.focalSubgroup
IHb : g * y✝ * g⁻¹ ∈ H.focalSubgroup
⊢ g * (x✝ * y✝) * g⁻¹ ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case inv
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x✝ : G
hx✝ : x✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
IH : g * x✝ * g⁻¹ ∈ H.focalSubgroup
⊢ g * x✝⁻¹ * g⁻¹ ∈ H.focalSubgroup

Tactic:
simpa using

Goal state after:
case inv
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x✝ : G
hx✝ : x✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
IH : g * x✝ * g⁻¹ ∈ H.focalSubgroup
⊢ g * (x✝⁻¹ * g⁻¹) ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
g : ↥P
hQ : IsPGroup p (↥↑P ⧸ (↑P).focalSubgroupOf)
⊢ ↑g ^ (↑P).index = 1 ↔ g ∈ (↑P).focalSubgroupOf

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
g : ↥P
hQ : IsPGroup p (↥↑P ⧸ (↑P).focalSubgroupOf)
⊢ ↑g ^ (↑P).index = 1 ↔ g ∈ (↑P).focalSubgroupOf
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ ∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) l

Tactic:
simpa using

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) (head :: tail)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : IsReduced l → IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h' : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ b.1 = a.1 → b.2 = a.2

Tactic:
simpa using

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : IsReduced l → IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h' : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ b.1 = a.1 → b.2 = a.2
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
⊢ comap (↑e) (upperCentralSeries G 0) = upperCentralSeries H 0

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
⊢ Function.Injective ⇑e
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))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ g x n = g y n

Tactic:
simpa using

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))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ g x n = g y n
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
heq : g x n = g y n
⊢ g x (2 * n) = g y (2 * n)

Tactic:
simpa using

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
heq : g x n = g y n
⊢ g x (2 * n) = g y (2 * n)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
⊢ f x n = f y n

Tactic:
simpa using

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
⊢ f x n = f y n
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
leq : f x n = f y n
⊢ f x (2 * n) = f y (2 * n)

Tactic:
simpa using

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
leq : f x n = f y n
⊢ f x (2 * n) = f y (2 * n)
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α × Bool
h : ∀ (x : FreeGroup α), x.toWord[0]? = some a ↔ x.toWord[0]? = some b
⊢ a = b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a b : α × Bool
h : ∀ (x : FreeGroup α), x.toWord[0]? = some a ↔ x.toWord[0]? = some b
⊢ a = b
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ treeHom T a = homOfPath T p

Tactic:
rw [treeHom, Unique.default_eq]

Goal state after:
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
⊢ a = w

Tactic:
simpa using

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
⊢ a = w
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
⊢ a = w

Tactic:
simpa using

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
⊢ a = w
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S.lowerCentralSeries n ≤ S
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
⊢ ∀ {a : WideSubquiver.toType (Symmetrify (Generators G)) T}
    (p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a), F'.map (homOfPath T p) = 1

Tactic:
intro a p

Goal state after:
case refine_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ F'.map (homOfPath T p) = 1
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (y.1 / x.1, 1) ∈ I
⊢ (1, x.2 / y.2) ∈ I

Tactic:
simpa using

Goal state after:
case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (y.1 / x.1, 1) ∈ I
⊢ (1, x.2 / y.2) ∈ I
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I

Tactic:
simpa using

Goal state after:
case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I
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 : G
h : H
hg : (g, h).1 ∈ ↑I.goursatFst.toSubmonoid
hh : (g, h).2 ∈ ↑I.goursatSnd.toSubmonoid
⊢ (g, h) ∈ I

Tactic:
simpa using

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
h : H
hg : (g, h).1 ∈ ↑I.goursatFst.toSubmonoid
hh : (g, h).2 ∈ ↑I.goursatSnd.toSubmonoid
⊢ (g, h) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:

Tactic:
⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
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 : G
h : H
hgh : (g, h) ∈ I
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range

Tactic:
simpa using

Goal state after:
case mp
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 : G
h : H
hgh : (g, h) ∈ I
⊢ ∃ (x : ∃ x, (g, x) ∈ I) (x_1 : ∃ a, (a, h) ∈ I),
    ∃ a b, ∃ (h_1 : (a, b) ∈ I), P ⟨(a, b), ⋯⟩ = ⟨g, ⋯⟩ ∧ Q ⟨(a, b), ⋯⟩ = ⟨h, ⋯⟩
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⊤.lowerCentralSeries 1 = ⊥ ↔ IsMulCommutative G

Tactic:
rw [lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_top]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = ⊤ ↔ IsMulCommutative G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : IsNilpotent G
⊢ ⊥ ≠ center G

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : IsNilpotent G
⊢ ¬⊥ = center G
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
⊢ (mk' (center G)).ker ≤ H

Tactic:
simpa using

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
⊢ center G ≤ H
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
hg' : g₁ • B ≠ g₂ • B
⊢ B = ∅

Tactic:
simpa using

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
⊢ B = ∅
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ Disjoint B (s • B)

Tactic:
simpa using

Goal state after:
M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ Disjoint B (s • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ ¬1 • B ⊆ s • B

Tactic:
simpa using

Goal state after:
M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ ¬B ⊆ s • 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
hB : IsBlock G B
g : G
⊢ g • B ≠ B → Disjoint (g • B) B

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
g : G
⊢ ¬g • B = B → Disjoint (g • B) B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ B = ∅

Tactic:
simpa using

Goal state after:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ B = ∅
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.Normal

Tactic:
· rw [hG1, minFac_one] at hHp
    exact normal_of_index_eq_one hHp

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.Normal
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X

Tactic:
simp only [Set.top_eq_univ, Set.ne_univ_iff_exists_notMem] at Hnt

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Hnt : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
α✝ : Type u_2
inst✝² : MulAction G✝ α✝
G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(SubAddAction.ofStabilizer G a)
hy : g +ᵥ ↑x ∈ {b}
⊢ ↑x ∈ {a}

Tactic:
simpa using

Goal state after:
G✝ : Type u_1
inst✝³ : Group G✝
α✝ : Type u_2
inst✝² : MulAction G✝ α✝
G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(SubAddAction.ofStabilizer G a)
hy : g +ᵥ ↑x ∈ {b}
⊢ ↑x = a
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
hy : g • ↑x ∈ {b}
⊢ ↑x ∈ {a}

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
hy : g • ↑x ∈ {b}
⊢ ↑x = 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
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
hB_ne_top : ¬B = Set.univ
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
simpa using

Goal state after:
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
hB_ne_top : ¬B = Set.univ
this : B.ncard < 2
⊢ B.Subsingleton
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(ofStabilizer G a)
⊢ ↑(((conjMap hh).comp (conjMap hg)) x) = ↑((conjMap hk) x)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(ofStabilizer G a)
⊢ (conjMap hh) ((conjMap hg) x) = (conjMap hk) x