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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ✝ σ τ : ↥(range_toPermHom' g)
⊢ ⟨a.ofPermHom (σ * τ), ⋯⟩ = ⟨a.ofPermHom σ, ⋯⟩ * ⟨a.ofPermHom τ, ⋯⟩

Tactic:
by

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, (toPermHom G α) σ = 1 ∨ ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
⊢ Function.Surjective ⇑(toPermHom G α)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
⊢ a * b * c = a * (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ 1 * a = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ a * 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ a⁻¹ * a = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ } = { left := 1, right := x✝¹ } * { left := 1, right := x✝ }

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
⊢ rightHom.comp inl = MonoidHom.id Q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
q : Q
⊢ rightHom (inl q) = q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝ : Finite Q
⊢ Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ (fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
      ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ (fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
      ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right } =
    { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }

Tactic:
by

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ g (a.ofPermHomFun τ x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
← (mem_cycleFactorsFinset_iff.mp ((τ : Perm g.cycleFactorsFinset) c).prop).2

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ ↑(↑τ c) (a.ofPermHomFun τ x) = ↑(↑τ c) (a.ofPermHomFun τ x)

case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
this : a.ofPermHomFun τ (g x) = g (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
Λ : Type u_3
inst✝ : MulAction D Λ
⊢ ∀ (x y : D ≀ᵣ Q) (b : Λ × Q), (x * y) • b = x • y • b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
Λ : Type u_3
inst✝ : MulAction D Λ
⊢ ∀ (b : Λ × Q), 1 • b = b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
⊢ ∀ {m₁ m₂ : D ≀ᵣ Q}, (∀ (a : Λ × Q), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite (IteratedWreathProduct G n)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: G : Type u
n : ℕ
inst✝ : Finite G
⊢ Nat.card (IteratedWreathProduct G n) = Nat.card G ^ ∑ i ∈ Finset.range n, Nat.card G ^ i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
⊢ a.toCentralizer τ • c = ↑τ c

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group (IteratedWreathProduct G n)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝³ : Group D
inst✝² : Group Q
G✝ : Type u
n✝ : ℕ
inst✝¹ : Group G✝
G : Type u_3
inst✝ : Group G
n : ℕ
⊢ IteratedWreathProduct G (n + 1) →* Equiv.Perm (Fin (n + 1) → G)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ Function.Injective ⇑(iteratedWreathToPermHom G 0)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
⊢ List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧
    ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
n : ℕ
⊢ Function.Injective ⇑(iteratedWreathToPermHom G (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ ReducedWord.prod φ w = ReducedWord.prod φ w'

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ Nat.card (Fin n → G) = p ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (OnCycleFactors.toPermHom g) (a.toCentralizer τ) = ↑τ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
hw : ReducedWord.prod φ w ∈ of.range
⊢ w.toList = []

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, g ∉ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : ResiduallyFinite G
g h : G
hgh : g ≠ h
H : FiniteIndexNormalSubgroup G
hH : g⁻¹ * h ∉ H
⊢ ↑g ≠ ↑h

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : ResiduallyFinite G
g h : G
hgh : g ≠ h
⊢ ∃ H, ↑g ≠ ↑h

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : IteratedWreathProduct G n →* Equiv.Perm α := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf : Function.Injective ⇑f
g : ↥f.range ≃* IteratedWreathProduct G n := (MonoidHom.ofInjective hf).symm
⊢ Nat.card ↥f.range = p ^ (Nat.card (Equiv.Perm α)).factorization p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ ↥↑P ≃* IteratedWreathProduct G n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
g : G
hg : g ≠ 1
w✝² : Type u
w✝¹ : Group w✝²
w✝ : Finite w✝²
f : G →* w✝²
hf : f g ≠ 1
⊢ g ∉ f.ker

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ τ ∈ (toPermHom g).range ↔ ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
⊢ ResiduallyFinite G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : ResiduallyFinite G
H : Subgroup G
⊢ ResiduallyFinite ↥H

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ τ ∈ (toPermHom g).range ↔ (fun c ↦ #(↑c).support) ∘ ⇑τ = fun c ↦ #(↑c).support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : ResiduallyFinite G
inst✝ : ResiduallyFinite G'
⊢ ResiduallyFinite (G × G')

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β x✝ y✝ : H.LeftTransversal
h : diff (MonoidHom.id ↥H) x✝ y✝ = 1
⊢ diff (MonoidHom.id ↥H) y✝ x✝ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : sign c = 1
⊢ Odd ((card ∘ support) c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (toPermHom g).range = range_toPermHom' g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β x✝ y✝ z✝ : H.LeftTransversal
h : diff (MonoidHom.id ↥H) x✝ y✝ = 1
h' : diff (MonoidHom.id ↥H) y✝ z✝ = 1
⊢ diff (MonoidHom.id ↥H) x✝ z✝ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
i : ℕ
hi : i ∈ g.cycleType
⊢ Odd i

Tactic:
by

Goal state after:
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
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ⟨(unop g)⁻¹ * ↑1 * unop g, ⋯⟩ = 1

Tactic:
by

Goal state after:
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
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
h₁ h₂ : ↥H
⊢ ⟨(unop g)⁻¹ * ↑(h₁ * h₂) * unop g, ⋯⟩ = ⟨(unop g)⁻¹ * ↑h₁ * unop g, ⋯⟩ * ⟨(unop g)⁻¹ * ↑h₂ * unop g, ⋯⟩

Tactic:
by

Goal state after:
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
hH : H.Normal
g : Gᵐᵒᵖ
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Tactic:
by

Goal state after:
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
g : G
α β : H.LeftTransversal
h : { r := fun α β ↦ diff (MonoidHom.id ↥H) α β = 1, iseqv := ⋯ } α β
⊢ ↑(diff (MonoidHom.id ↥H) (op g⁻¹ • α) (op g⁻¹ • β)) = ↑1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := fun c ↦ #(↑c).support
hsc : sc = fun c ↦ #(↑c).support
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
by

Goal state after:
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
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op (g₁ * g₂)⁻¹ • α) T = (fun α ↦ op g₁⁻¹ • α) ((fun α ↦ op g₂⁻¹ • α) T)

Tactic:
by

Goal state after:
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
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op 1⁻¹ • α) T = T

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
by

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
⊢ Mul (PushoutI φ)

Tactic:
by

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
⊢ One (PushoutI φ)

Tactic:
by

Goal state after:
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 : ι
⊢ (of i).comp (φ i) = base φ

Tactic:
by

Goal state after:
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
⊢ (of i) ((φ i) x) = (base φ) x

Tactic:
by

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

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

Tactic:
by

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 : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
⊢ con φ ≤ Con.ker (Coprod.lift (CoprodI.lift f) k)

Tactic:
by

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 : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ (lift f k hf) ((of i) g) = (f i) g

Tactic:
by

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 : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ (lift f k hf) ((base φ) g) = k g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m} =
    if Even (m.sum + m.card) then {g | g.cycleType = m} else ∅

Tactic:
by

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

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

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ ↥(alternatingGroup α) ↪ ?m.76

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ Type ?u.64

Tactic:
map_subtype_of_cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ #(if Even (m.sum + m.card) then {g | g.cycleType = m} else ∅) *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) 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
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
⊢ diff (MonoidHom.id ↥H) α (op ↑h • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index

Tactic:
by

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
hn : Nonempty ι
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
⊢ f.comp (base φ) = g.comp (base φ)

Tactic:
by

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 : ι
⊢ ((fun i ↦ f.comp (of i), f.comp (base φ)).1 i).comp (φ i) = (fun i ↦ f.comp (of i), f.comp (base φ)).2

Tactic:
by

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
x✝ : PushoutI φ →* K
⊢ ∀ (i : ι),
    ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ((fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (of i) =
      x✝.comp (of i)

Tactic:
by

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
x✝ : PushoutI φ →* K
⊢ ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ((fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (base φ) =
    x✝.comp (base φ)

Tactic:
by

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
x✝ : { f // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }
fst✝ : (i : ι) → G i →* K
snd✝ : H →* K
property✝ : ∀ (i : ι), ((fst✝, snd✝).1 i).comp (φ i) = (fst✝, snd✝).2
⊢ (fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ⟨(fst✝, snd✝), property✝⟩) =
    ⟨(fst✝, snd✝), property✝⟩

Tactic:
by

Goal state after:
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 : ι
g : G i
⊢ ofCoprodI (CoprodI.of g) = (of i) g

Tactic:
by

Goal state after:
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 = diff (MonoidHom.id ↥H) (op ↑h⁻¹ • α) α

Tactic:
by

Goal state after:
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
⊢ diff (MonoidHom.id ↥H) β α * ((powCoprime hH).symm (diff (MonoidHom.id ↥H) β α))⁻¹ ^ H.index = 1

Tactic:
by

Goal state after: