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

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ BddAbove (Set.range fun a ↦ period m a)

Tactic:
use Monoid.exponent M

Goal state after:
case h
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ Monoid.exponent M ∈ upperBounds (Set.range fun a ↦ period m a)
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
a : α
ha : a ∈ s
⊢ ∀ b ∈ s, ∃ g ∈ stabilizer (Perm α) s, g • a = b

Tactic:
b

Goal state after:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → ∃ g ∈ stabilizer (Perm α) s, g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
h : stabilizer (Perm α) s = ⊤
⊢ False

Tactic:
Set.mem_compl_iff

Goal state after:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ False
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ s.Nonempty

Tactic:
Set.nonempty_iff_ne_empty

Goal state after:
case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ s ≠ ∅
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ sᶜ.Nonempty

Tactic:
Set.nonempty_iff_ne_empty

Goal state after:
case a
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this✝ : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : 1 + 1 = 2
⊢ sᶜ ≠ ∅
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : ↑(Nat.card α) = 2
x✝ : Finite α
⊢ Nat.card α = 2

Tactic:
exact ENat.natCast_inj.mp hα

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
⊢ ∀ b ∈ t, ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
b

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
⊢ b ∈ t → ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case hs
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
ha : a ∈ s
⊢ ∀ b ∈ s, ∃ g, g • a = b

Tactic:
b

Goal state after:
case hs
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → ∃ g, g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case hs'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
ha : a ∈ sᶜ
⊢ ∀ b ∈ sᶜ, ∃ g, g • a = b

Tactic:
b

Goal state after:
case hs'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
a : α
ha : a ∈ sᶜ
b : α
⊢ b ∈ sᶜ → ∃ g, g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ IsPretransitive (↥G) α

Tactic:
by
  apply IsPretransitive.of_partition (s := s)
  · intro a ha b hb
    obtain ⟨g, hg, rfl⟩ := moves a ha b hb
    exact ⟨⟨g, hG.le hg⟩, rfl⟩
  · intro a ha b hb
    obtain ⟨g, hg, rfl⟩ := moves a ha b hb
    rw [stabilizer_compl] at hg
    exact ⟨⟨g, hG.le hg⟩, rfl⟩
  · contrapose hG
    apply not_lt_of_ge
    --  `G ≤ stabilizer (Equiv.Perm α) s`
    have : G = Subgroup.map G.subtype ⊤ := by
      rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]
    rw [this, Subgroup.map_le_iff_le_comap]
    rw [show Subgroup.comap G.subtype (stabilizer M s) = stabilizer G s from rfl, hG]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
use stabilizer_ne_top h0.nonempty h1

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
⊢ ∀ (b : Subgroup ↥(alternatingGroup α)), stabilizer (↥(alternatingGroup α)) s < b → b = ⊤
Module: Mathlib.GroupTheory.GroupAction.Support

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
⊢ Supports G (g • s) (g • b)

Tactic:
rintro g' hg'

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
⊢ g' • g • b = g • b
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
s : S.Splitting
⊢ S.rightHom.comp ↑s = MonoidHom.id G

Tactic:
ext g
  simp only [MonoidHom.comp_apply, MonoidHom.id_apply, MonoidHom.coe_coe, rightHom_splitting]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
⊢ g • a = a

Tactic:
suffices φ g = φ 1 by
    conv_rhs => rw [← one_smul K a]
    simp only [← toPerm_apply, ← toPermHom_apply K α g]
    exact congrFun (congrArg DFunLike.coe this) a

Goal state after:
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
⊢ φ g = φ 1
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : toPerm g = 1
⊢ toPerm g = 1

Tactic:
contrapose h with h
    have : ∃ a, (g • a : α) ≠ a := by simpa [Equiv.ext_iff] using h
    obtain ⟨a, ha⟩ := this
    obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)
    rw [Equiv.ext_iff, not_forall]
    use s
    contrapose! has'
    simp only [toPerm_apply, coe_one, id_eq] at has'
    rw [← has']
    simpa only [coe_smul, smul_mem_smul_finset_iff, ← mem_coe_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g • a = a
⊢ toPerm g = toPerm 1

Tactic:
rw [toPerm_one, ← mulAction_faithful hn hα]

Goal state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g • a = a
⊢ toPerm g = 1
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * of ↑b * t

Tactic:
rw [mul_assoc, of_mul_t]; simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))

Tactic:
convert! φ.symm <;>
    cases Int.units_eq_one_or u

Goal state after:
case e'_1.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = 1
⊢ toSubgroup A B u = B

case e'_1.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = -1
⊢ toSubgroup A B u = B

case e'_2.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = 1
⊢ toSubgroup A B (-u) = A

case e'_2.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = -1
⊢ toSubgroup A B (-u) = A

case e'_3.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_1✝ : ↥(toSubgroup A B u) = ↥B
h✝ : u = 1
⊢ toSubgroup A B u = B

case e'_3.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_1✝ : ↥(toSubgroup A B u) = ↥B
h✝ : u = -1
⊢ toSubgroup A B u = B

case e'_4.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_2✝ : ↥(toSubgroup A B (-u)) = ↥A
h✝ : u = 1
⊢ toSubgroup A B (-u) = A

case e'_4.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_2✝ : ↥(toSubgroup A B (-u)) = ↥A
h✝ : u = -1
⊢ toSubgroup A B (-u) = A
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
w : NormalWord d
ofGroup : (g : G) → motive (NormalWord.ofGroup g)
cons :
  (g : G) →
    (u : ℤˣ) →
      (w : NormalWord d) →
        (h1 : w.head ∈ d.set u) →
          (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') →
            motive w → motive (NormalWord.cons g u w h1 h2)
⊢ motive w

Tactic:
by
  rcases w with ⟨⟨g, l, chain⟩, mem_set⟩
  induction l generalizing g with
  | nil => exact ofGroup _
  | cons a l ih =>
    exact cons g a.1
      { head := a.2
        toList := l
        mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h),
        chain := (List.isChain_cons.1 chain).2 }
      (mem_set a.1 a.2 List.mem_cons_self)
      (by simpa using (List.isChain_cons.1 chain).1)
      (ih _ _ _)

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ ((comap f H).subgroupOf (comap f K)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer ↑(comap f H)
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
⊢ ∀ (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
b

Goal state after:
case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
⊢ f a * g b = 1 → a = 1 ∧ b = 1
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a : List α
⊢ ∀ {b : List α}, a ∈ p → b ∈ p → a.Disjoint b → a.formPerm.Disjoint b.formPerm

Tactic:
b

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
⊢ a ∈ p → b ∈ p → a.Disjoint b → a.formPerm.Disjoint b.formPerm
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₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
w₂' : NormalWord d
hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂'.toReducedWord

Tactic:
hw₂'1,

Goal state after:
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₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
w₂' : NormalWord d
hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
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:
rw [mem_range_toPermHom_iff, funext_iff]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) ↔
    ∀ (x : ↥g.cycleFactorsFinset), ((fun c ↦ #(↑c).support) ∘ ⇑τ) x = #(↑x).support
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:
split_ifs with hm

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m} = {g | g.cycleType = m}

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m} = ∅
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

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

Tactic:
split_ifs with hm

Goal state after:
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)
⊢ #{g | (↑g).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))

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))
⊢ #{g | (↑g).cycleType = m} = 0
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)
⊢ (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    0

Tactic:
if_neg

Goal state after:
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

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.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'
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
⊢ Nat.card (G ⧸ K) < Nat.card G

Tactic:
← index_eq_card,

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'
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
⊢ K.index < Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : ¬x = ⟨c, hc⟩
hx' : ¬x = ⟨d, hd⟩
⊢ #(↑(τ x)).support = #(↑x).support

Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hx hx']

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ #{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 then (Fintype.card α)! else 0

Tactic:
split_ifs with hm

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 α)!

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: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ #{g | g.cycleType = m} =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0

Tactic:
split_ifs with hm

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)!)

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.KleinFour

Goal state before:
pp: α : 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 : k ∈ g.cycleType
hk4 : k ≤ 4
hk1 : 1 < k
⊢ k = 2

Tactic:
interval_cases k

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

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

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