mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {1}
⊢ g ^ 2 = 1

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {1}
⊢ g ^ 2 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
this : Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - g.cycleType.sum
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) ≤ 1

Tactic:
by lia

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {1}
⊢ g ^ 2 = 1

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1

Tactic:
· convert! one_pow _
      simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ 2 = g.cycleType.lcm

Tactic:
hg'

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ 2 = {2, 2}.lcm
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case e'_9
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
⊢ head = ((PushoutI.base φ) head • { toWord := w, head := 1, normalized := h3 }).head

pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
⊢ motive { toWord := w, head := 1, normalized := h3 }

Tactic:
·

Goal state after:
case e'_9
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
⊢ head = ((PushoutI.base φ) head • { toWord := w, head := 1, normalized := h3 }).head
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
⊢ motive { toWord := w, head := 1, normalized := h3 }

Tactic:
·

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i
⊢ motive { toWord := w, head := 1, normalized := h3 }
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) * Nat.card ↥(kleinFour α) = 3 * Nat.card ↥(kleinFour α)

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card ↥(kleinFour α) ≠ 0

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) * Nat.card ↥(kleinFour α) = 3 * Nat.card ↥(kleinFour α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ 3 < Nat.card α

pp: case refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 3

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ 3 < Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 3

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 3
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
⊢ Nontrivial ↥(alternatingGroup α)

Tactic:
← Finite.one_lt_card_iff_nontrivial,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
⊢ 1 < Nat.card ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case a
n : ℕ
i : ZMod (2 * n)
⊢ 1 * a i = a i

pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i

Tactic:
·

Goal state after:
case a
n : ℕ
i : ZMod (2 * n)
⊢ 1 * a i = a i
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i

Tactic:
·

Goal state after:
case xa
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : (↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : (↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case a
n : ℕ
i : ZMod (2 * n)
⊢ a i * 1 = a i

pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i

Tactic:
·

Goal state after:
case a
n : ℕ
i : ZMod (2 * n)
⊢ a i * 1 = a i
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i

Tactic:
·

Goal state after:
case xa
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case a
n : ℕ
i : ZMod (2 * n)
⊢ (a i).inv * a i = 1

pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1

Tactic:
·

Goal state after:
case a
n : ℕ
i : ZMod (2 * n)
⊢ (a i).inv * a i = 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case e'_9
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ 1 = (NormalWord.cons g { toWord := w, head := 1, normalized := ⋯ } h1 ?cons).head

pp: case cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ g ∉ (φ i).range

Tactic:
·

Goal state after:
case e'_9
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ 1 = (NormalWord.cons g { toWord := w, head := 1, normalized := ⋯ } h1 ?cons).head
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1

Tactic:
·

Goal state after:
case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
⊢ 1 ∈ commutator ↥(alternatingGroup α)

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
⊢ 1 ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ g ∈ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ g ∉ (φ i).range

Tactic:
·

Goal state after:
case cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ g ∉ (φ i).range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1

pp: case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1

Tactic:
·

Goal state after:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1

Tactic:
·

Goal state after:
case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hx
⊢ orderOf ?x = Nat.card (QuaternionGroup 1)

pp: case x
⊢ QuaternionGroup 1

Tactic:
·

Goal state after:
case hx
⊢ orderOf ?x = Nat.card (QuaternionGroup 1)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
⊢ orderOf (a 1) = 2 * 0

pp: case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n

Tactic:
·

Goal state after:
case inl
⊢ orderOf (a 1) = 2 * 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4

pp: case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Tactic:
·

Goal state after:
case inl
⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4

pp: case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
·

Goal state after:
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1

pp: case inr.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1

Tactic:
·

Goal state after:
case inr.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1

Tactic:
·

Goal state after:
case inr.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
⊢ IsCyclic ↥↑P

Tactic:
obtain ⟨Q, hQ⟩ := P.exists_comap_eq_of_injective hf

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
⊢ IsCyclic ↥↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
⊢ commutator G < ⊤

Tactic:
let p := (Nat.card G).minFac

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
p : ℕ := (Nat.card G).minFac
⊢ commutator G < ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
·

Goal state after:
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)

pp: case hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
·

Goal state after:
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
·

Goal state after:
case hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)