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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ∏ q, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ∏ x, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ * h

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ∏ q, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ∏ x, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ * h
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (base φ) x = (base φ) x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈ (↑((u, v).2 a)).support
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
⊢ x ∈ Function.fixedPoints ⇑g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Even (m.sum + m.card)
⊢ False

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Even (m.sum + m.card)
⊢ False
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ (g.comp ((of i).comp (φ i))) x✝ = (g.comp ((of i).comp (φ i))) x✝

Tactic:
]

Goal state after:
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 : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : PushoutI φ →* K
i : ι
⊢ f.comp (base φ) = (fun i ↦ f.comp (of i), f.comp (base φ)).2

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : PushoutI φ → Prop
x : PushoutI φ
of : ∀ (i : ι) (g : G i), motive ((PushoutI.of i) g)
base : ∀ (h : H), motive ((PushoutI.base φ) h)
mul : ∀ (x y : PushoutI φ), motive x → motive y → motive (x * y)
⊢ motive x

Tactic:
delta PushoutI PushoutI.of PushoutI.base at *

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
x : (con φ).Quotient
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
⊢ motive x
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : h • Quotient.mk'' α = Quotient.mk'' α
⊢ h ^ H.index = h ^ H.index

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case H.inl.mul
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive ↑(inl x)
ihy : motive ↑(inl y)
⊢ motive ↑(inl x * inl y)

Tactic:
]

Goal state after:
case H.inl.mul
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive ↑(inl x)
ihy : motive ↑(inl y)
⊢ motive ↑(inl x * inl y)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k✝ : ℤ
hk✝ : ↑a ^ k✝ = ↑(v a)
k : ℤ
ha2 : g x = x
hk : ↑⟨g.cycleOf x, hx⟩ ^ k = ↑(v ⟨g.cycleOf x, hx⟩)
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k✝ : ℤ
hk✝ : ↑a ^ k✝ = ↑(v a)
k : ℤ
ha2 : g x = x
hk : ↑⟨g.cycleOf x, hx⟩ ^ k = ↑(v ⟨g.cycleOf x, hx⟩)
⊢ x ∈ Function.fixedPoints ⇑g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

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

Tactic:
simp only [and_comm (b := Even _)]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ β✝ : H.QuotientDiff
β α : H.LeftTransversal
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ x ∉ ((noncommPiCoprod ⋯) (u, v).2).support

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ x ∉ ((noncommPiCoprod ⋯) (u, v).2).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑ofSubtype ∧
    Function.Injective ⇑(noncommPiCoprod ⋯) ∧ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑ofSubtype ∧
    Function.Injective ⇑(noncommPiCoprod ⋯) ∧ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: 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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.relIndex (K ⊔ N)

Tactic:
]

Goal state after:
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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.relIndex (K ⊔ N)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ (↑a).Disjoint ↑b

Tactic:
]

Goal state after:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ (↑a).Disjoint ↑b
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: 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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ Nat.card ↥K < K.index * Nat.card ↥K

Tactic:
]

Goal state after:
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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ Nat.card ↥K < K.index * Nat.card ↥K
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (⨆ i, zpowers ↑i)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (⨆ i, zpowers ↑i)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : 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
⊢ ↑(⋯.equiv (if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1)).2 =
    if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1

Tactic:
]

Goal state after:
ι : 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
⊢ ↑(⋯.equiv (if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1)).2 =
    if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: 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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
⊢ (Nat.card ↥(comap K.subtype N)).Coprime N.index

Tactic:
]

Goal state after:
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'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
⊢ (Nat.card ↥(comap K.subtype N)).Coprime N.index
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    ∀ (i : ↥g.cycleFactorsFinset), zpowers ↑i ≤ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
]

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    ∀ (i : ↥g.cycleFactorsFinset), zpowers ↑i ≤ map (centralizer {g}).subtype (toPermHom g).ker
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ (if Even (m.sum + m.card) then #{g | g.cycleType = m} else 0) = 0
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
h : ¬∃ (h : w.toList ≠ []), (w.toList.head h).fst = i
⊢ ↑(⟨1, ⋯⟩, ⟨1, ⋯⟩).2 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a.left.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a * g = g * ofSubtype a

Tactic:
]

Goal state after:
case a.left.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a * g = g * ofSubtype a
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a.left.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a ∈ centralizer {g}

Tactic:
rw [mem_centralizer_singleton_iff]

Goal state after:
case a.left.refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a * g = g * ofSubtype a
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ 0 = 0

pp: case pos.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
]

Goal state after:
case pos.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c) := fun c ↦ ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x) = ↑p x

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c) := fun c ↦ ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x) = ↑p x