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

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
⊢ ↑P ≤ centralizer ↑(zpowers x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsSimpleGroup α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
⊢ x ^ m = f a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
⊢ x ^ n = f b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
⊢ y ^ (-m) * a ∈ f.ker

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
⊢ y ^ (-n) * b ∈ f.ker

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ ↑(g • P) ≤ centralizer ↑(zpowers x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
⊢ IsMulCommutative G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsCyclic (G ⧸ center G)
⊢ IsMulCommutative G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
⊢ IsCyclic α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.card α ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsMulTorsion G
g : G
⊢ g ^ (orderOf g - 1) * g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsMulTorsion G
h : H
⊢ IsOfFinOrder h

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ g ∈ Subgroup.zpowers (g ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
⊢ orderOf g ∣ n ∨ n.Coprime (orderOf g)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : orderOf g = 0
⊢ ¬orderOf g ∣ 37 ∧ Nat.gcd 37 (orderOf g) ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
⊢ Nat.Prime (Nat.card α)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
n : ℤ
⊢ (fun x ↦ x • 1) n = n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Nat.Prime (Nat.card (ZMod p))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ G ⧸ stabilizer G P ≃ G ⧸ normalizer ↑P

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
⊢ g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
gn : ↥N
h : ↑gn = g ^ ngn
hmem : ↑gn ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ g ^ (ngn * nn) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
⊢ IsOfFinOrder g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ExponentExists G
g : G
⊢ IsOfFinOrder g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Function.Surjective fun x ↦ x • -g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ -g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
⊢ ∃ n, 0 < n ∧ n • f = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
⊢ torsion (G × H) = (torsion G).prod (torsion H)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ 0 < -g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
⊢ IsAddCyclic A ↔ Nonempty (A ≃+o ℤ)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑((fun x_1 ↦ ⟨x, ⋯⟩ * x_1)^[n] 1) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_4
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
⊢ IsCyclic G ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
⊢ exponent α = Nat.card α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: n : ℕ
⊢ AddMonoid.exponent (ZMod n) = n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p ↥Q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ p ^ 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ ∃ a < 3, p ^ a = orderOf g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ ?m.163

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ (a * b) ^ p ^ (m + n) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = Nat.card α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
⊢ 1 ^ p ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
⊢ ¬p ∣ (↑P).index

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
⊢ ¬IsCyclic α ↔ exponent α = p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
⊢ ((zmultiplesHom G) g).ker = zmultiples ↑(addOrderOf g)

Tactic:
ext
  simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ n, orderOf g = p ^ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
⊢ ((zmultiplesHom G) g).ker = zmultiples ↑(addOrderOf g)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ zmultiples ↑n = ((zmultiplesHom G) g).ker

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
⊢ ¬p ∣ (↑P).index

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ ¬p ∣ (↑P).index

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (zmodAddEquivOfGenerator hg hn) ↑i = i • g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg : g ∈ primaryComponent G p
hg' : g ∈ primaryComponent G p'
⊢ g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (zmodAddEquivOfGenerator hg hn).symm (i • g) = ↑i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
tG : IsMulTorsion G
⊢ torsion G = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ (zmodAddEquivOfGenerator hg hn) 1 = g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
⊢ (zmodAddEquivOfGenerator hg hn).symm g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ IsMulTorsionFree G ↔ torsion G = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
⊢ torsion G ≤ Subgroup.comap f (torsion H)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
⊢ ∃ p, Nat.Prime p ∧ Nonempty (Additive G ≃+ ZMod p)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ Subgroup.comap f (torsion H) = torsion G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
e : G ≃* H
⊢ Subgroup.map (↑e) (torsion G) = torsion H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
⊢ G ≃* G'

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
⊢ ¬p ∣ Q.index

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
⊢ torsion (G × H) = (torsion G).prod (torsion H)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
⊢ Function.Bijective ⇑((zpowersHom G) g)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
⊢ (intEquivOfZPowersEqTop g hg).symm g = Multiplicative.ofAdd 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
k : ℤ
⊢ (intEquivOfZPowersEqTop g hg).symm (g ^ k) = Multiplicative.ofAdd k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ IsMulTorsion (G ⧸ (powMonoidHom n).range)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
p : ℕ
g : G
x✝ : g ∈ (CommMonoid.primaryComponent G p).carrier
k : ℕ
hk : g ^ p ^ k = 1
⊢ g⁻¹ ^ p ^ k = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
⊢ StrictMono ⇑(intEquivOfZPowersEqTop g hg)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
p : ℕ
g : ↥(primaryComponent G p)
x✝ : ℕ
hk : ↑g ^ p ^ x✝ = 1
⊢ ↑(g ^ p ^ x✝) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ freeRank G = 0 ↔ IsMulTorsion G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Function.Surjective (mapSurjective hf)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : g < 1
⊢ StrictAnti ⇑(intEquivOfZPowersEqTop g hg)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : AddGroup G
g : G
hg : zmultiples g = ⊤
⊢ Function.Bijective ⇑((zmultiplesHom G) g)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : AddGroup G
g : G
hg : zmultiples g = ⊤
⊢ (intEquivOfZMultiplesEqTop g hg).symm g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
⊢ IsMulTorsionFree (G ⧸ torsion G)

Tactic:
by

Goal state after: