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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case pos
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

pp: case neg
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : ¬w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
·

Goal state after:
case pos
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case refine_2
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
⊢ comap (QuotientGroup.mk' K) H ≠ ⊤

Tactic:
·

Goal state after:
case refine_2
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
⊢ comap (QuotientGroup.mk' K) H ≠ ⊤
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ #{g | g.cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ #{g | g.cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case neg
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : ¬w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
·

Goal state after:
case neg
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : ¬w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos.H1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!

pp: case pos.H2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Fintype.card α)! =
    #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)

Tactic:
·

Goal state after:
case pos.H1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ 0 < (Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ #{g | g.cycleType = m} = 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ (kerParam g).range

Tactic:
kerParam_range_eq,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ Subgroup.map (Subgroup.centralizer {g}).subtype (toPermHom g).ker
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case «2»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 2 ∈ g.cycleType
hk4 : 2 ≤ 4
hk1 : 1 < 2
⊢ 2 = 2

pp: case «3»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : 3 ≤ 4
hk1 : 1 < 3
⊢ 3 = 2

pp: case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
⊢ 4 = 2

Tactic:
·

Goal state after:
case «2»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 2 ∈ g.cycleType
hk4 : 2 ≤ 4
hk1 : 1 < 2
⊢ 2 = 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case «3»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : 3 ≤ 4
hk1 : 1 < 3
⊢ 3 = 2

pp: case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
⊢ 4 = 2

Tactic:
·

Goal state after:
case «3»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : 3 ≤ 4
hk1 : 1 < 3
⊢ 3 = 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
⊢ 4 = 2

Tactic:
·

Goal state after:
case «4»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg0 : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ 2 ^ n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
⊢ 4 = 2
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

pp: case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
·

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

pp: case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
·

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case inl
ι : 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)
i✝ : ι
p : Pair d i✝
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i✝).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.tail.toList
⊢ g ∈ d.set i

pp: case inr
ι : 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)
i : ι
p : Pair d i
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
left✝ : ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ≠ 1
⊢ ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ∈ d.set i

Tactic:
·

Goal state after:
case inl
ι : 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)
i✝ : ι
p : Pair d i✝
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i✝).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.tail.toList
⊢ g ∈ d.set i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α) →
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ((∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
    ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α) →
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case inr
ι : 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)
i : ι
p : Pair d i
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
left✝ : ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ≠ 1
⊢ ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ∈ d.set i

Tactic:
·

Goal state after:
case inr
ι : 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)
i : ι
p : Pair d i
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
left✝ : ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ≠ 1
⊢ ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ∈ d.set i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ((∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
    ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ((∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
    ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
hN3 : Finite G
⊢ ∃ H, N.IsComplement' H

Tactic:
exact exists_right_complement'_of_coprime_aux' rfl hN

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ Nontrivial α

Tactic:
← Finite.one_lt_card_iff_nontrivial,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ 1 < Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2.e'_6
α : 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
⊢ ∏ c, sign ↑(uv c) = 1

pp: case e'_3
α : 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
⊢ 1 = sign y

Tactic:
·

Goal state after:
case e'_2.e'_6
α : 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
⊢ ∏ c, sign ↑(uv c) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ ↑S
⊢ k ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}}

pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Fintype.card ↑↑S

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ ↑S
⊢ k ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Fintype.card ↑↑S

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Fintype.card ↑↑S
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2
α : 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
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ Odd #(↑⟨c, hc⟩).support

pp: case e'_2
α : 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
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ (↑⟨c, hc⟩).IsCycle

Tactic:
·

Goal state after:
case e'_2
α : 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
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ Odd #(↑⟨c, hc⟩).support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2
α : 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
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ (↑⟨c, hc⟩).IsCycle

Tactic:
·

Goal state after:
case e'_2
α : 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
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ (↑⟨c, hc⟩).IsCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_3
α : 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
⊢ 1 = sign y

Tactic:
·

Goal state after:
case e'_3
α : 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
⊢ 1 = sign y