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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : FiniteIndexNormalSubgroup G
h : (fun H ↦ H.toSubgroup) A = (fun H ↦ H.toSubgroup) B
⊢ A = B

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
A B : FiniteIndexNormalSubgroup G
h : (fun H ↦ H.toSubgroup) A = (fun H ↦ H.toSubgroup) B
x✝ : G
⊢ x✝ ∈ A.carrier ↔ x✝ ∈ B.carrier
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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝¹ x✝ : G
⊢ (Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) (x✝¹ * x✝) =
    (Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝¹ *
      (Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝

Tactic:
ext

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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝² x✝¹ : G
x✝ : G →* Mˣ
⊢ ↑(((Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) (x✝² * x✝¹)) x✝) =
    ↑(((Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝² *
          (Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝¹)
        x✝)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
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:
if_pos hk,

Goal state after:
case pos
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 ^ ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) * 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)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
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 ^ ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) * 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:
if_pos hk,

Goal state after:
case pos
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 ^ ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) * Quotient.out (Quotient.out ⟨q, k - 1⟩.fst) =
    g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
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)

pp: case neg
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:
· simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero]

Goal state after:
case neg
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.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
key : g * φ g = 1
⊢ φ g = g⁻¹

Tactic:
rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key

Goal state after:
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
⊢ (↑P).Normal

Tactic:
have frattini_argument := Sylow.normalizer_sup_eq_top P

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : normalizer ↑(map (frattini G).subtype ↑P) ⊔ frattini G = ⊤
⊢ (↑P).Normal
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : normalizer ↑(map (frattini G).subtype ↑P) ⊔ frattini G = ⊤
⊢ (↑P).Normal

Tactic:
have normalizer_P := frattini_nongenerating frattini_argument

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : normalizer ↑(map (frattini G).subtype ↑P) ⊔ frattini G = ⊤
normalizer_P : normalizer ↑(map (frattini G).subtype ↑P) = ⊤
⊢ (↑P).Normal
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)
x✝¹ : α × Bool
ha : (replicate (n + 1) (head :: tail)).flatten.getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2

Tactic:
List.getLast?_flatten_replicate (h := by simp +arith)

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ N.upperCentralSeriesStep = comap (mk' N) (center (G ⧸ N))

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ : G
⊢ x✝ ∈ N.upperCentralSeriesStep ↔ x✝ ∈ comap (mk' N) (center (G ⧸ N))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = center G

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = center G

Tactic:
ext
  simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, mem_bot, mem_mk,
    Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_ofPred_eq, mem_center_iff]
  exact forall_congr' fun y => by
    rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
⊢ AddSubgroup.upperCentralSeries G 1 = AddSubgroup.center G

Tactic:
ext

Goal state after:
G : Type u_2
inst✝ : AddGroup G
x✝ : G
⊢ x✝ ∈ AddSubgroup.upperCentralSeries G 1 ↔ x✝ ∈ AddSubgroup.center G
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:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
n : ℕ
x✝ : H
⊢ x✝ ∈ comap (↑e) (upperCentralSeries G (n + 1)) ↔ x✝ ∈ upperCentralSeries H (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Group.IsNilpotent G ↔ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
⊢ Group.IsNilpotent G → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
n : ℕ
nH : upperCentralSeries G n = ⊤
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
exact ⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩

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

Goal state before:
pp: G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
e : IsFreeGroup.Generators G
⊢ (curry E) (IsFreeGroup.of e) = f' e

Tactic:
ext

Goal state after:
case left
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
e : IsFreeGroup.Generators G
x✝ : A
⊢ ((curry E) (IsFreeGroup.of e)).left x✝ = (f' e).left x✝

case right
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
e : IsFreeGroup.Generators G
⊢ ((curry E) (IsFreeGroup.of e)).right = (f' e).right
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n H, IsAscendingCentralSeries H ∧ H 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
i : X
⊢ i ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1} ↔
    i ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
i : X
⊢ i ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1} →
    i ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

case mpr
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
i : X
⊢ i ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x} →
    i ∈ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1}
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsDescendingCentralSeries ⊤.lowerCentralSeries

Tactic:
constructor

Goal state after:
case left
G : Type u_1
inst✝ : Group G
⊢ ⊤.lowerCentralSeries 0 = ⊤

case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ ↔ nilpotencyClass G ≤ n

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ → nilpotencyClass G ≤ n

case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → upperCentralSeries G n = ⊤
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ ⊤.lowerCentralSeries n = ⊥ → nilpotencyClass G ≤ n

case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ FG G ↔ ∃ n, Nonempty (Generators G (Fin n))

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
⊢ FG G → ∃ n, Nonempty (Generators G (Fin n))

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n, Nonempty (Generators G (Fin n))) → FG G
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)
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
⊢ (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I

Tactic:
constructor

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
⊢ (y.1 / x.1, 1) ∈ I → (1, x.2 / y.2) ∈ I

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
⊢ (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' : 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)
⊢ Surjective (Prod.snd ∘ ⇑I'.subtype)

Tactic:
simp only [← MonoidHom.coe_snd, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']

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)
⊢ map (MonoidHom.snd ↥G' ↥H') (P.prod Q).range = ⊤
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 : G
h : H
⊢ (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:
constructor

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 := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
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
⊢ (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

case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
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
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range →
    (g, h) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ center G = ⊤

Tactic:
rw [← upperCentralSeries_one]

Goal state after:
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ upperCentralSeries G 1 = ⊤
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case e_5
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := ⋯
f : G → X := ⋯
F : G ⥤ CategoryTheory.SingleObj X := ⋯
⊢ F = (Functor.const G).obj ()

Tactic:
ext

Goal state after:
case e_5
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ F.map (of e✝) = ((Functor.const G).obj ()).map (of e✝)
Module: Mathlib.GroupTheory.GroupAction.Transitive

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

Tactic:
constructor

Goal state after:
case mp
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive M α → IsPretransitive N β

case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) ↔ IsTrivialBlock B

Tactic:
constructor

Goal state after:
case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B

case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock B → IsTrivialBlock (g • 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
N : Subgroup G
nN : N.Normal
a : X
g : G
⊢ (range fun i ↦ g • i • a) = range fun m ↦ m • g • a

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (x✝ ∈ range fun i ↦ g • i • a) ↔ x✝ ∈ range fun m ↦ m • g • a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, g • y • a = x✝) → ∃ y, y • g • a = x✝

case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = 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
N : Subgroup G
inst✝ : N.Normal
⊢ IsBlockSystem G (range fun a ↦ orbit (↥N) a)

Tactic:
constructor

Goal state after:
case left
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ Setoid.IsPartition (range fun a ↦ orbit (↥N) a)

case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ ∀ ⦃B : Set X⦄, (B ∈ range fun a ↦ orbit (↥N) a) → IsBlock G 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
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a ↔ x ∈ B

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit (↥(stabilizer G B)) a → x ∈ B

case mpr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ B → x ∈ orbit (↥(stabilizer G B)) a
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
exact normal_of_index_eq_two hHp

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

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

Tactic:
constructor

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

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