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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ NormalizerCondition G

Tactic:
by
  -- roughly based on https://groupprops.subwiki.org/wiki/Nilpotent_implies_normalizer_condition
  rw [normalizerCondition_iff_only_full_group_self_normalizing]
  apply @nilpotent_center_quotient_ind _ G _ _ <;> clear! G
  · intro G _ _ H _
    exact @Subsingleton.elim _ Unique.instSubsingleton _ _
  · intro G _ _ ih H hH
    have hch : center G ≤ H := Subgroup.center_le_normalizer H |>.trans (le_of_eq hH)
    have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
    have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective
    let H' := H.map (mk' (center G))
    have hH' : normalizer H' = H' := by
      apply comap_injective hsur
      rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
      exact hH
    apply map_injective_of_ker_le (mk' (center G)) hkh le_top
    exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)

Tactic:
rw [isBlock_iff_smul_eq_or_disjoint]
  intro h'
  obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
  simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply] at hh
  suffices h' • g • B = g • h • B by
    simp only [this]
    apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
    · intro; congr
    · exact Set.disjoint_image_of_injective (MulAction.injective g)
  suffices (h' : G) • g • B = g • h • B by
    rw [← this]; rfl
  rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g : G
x✝ : X
⊢ (∃ y, y • g • a = x✝) → ∃ y, g • y • a = x✝

Tactic:
rintro ⟨⟨k, hk⟩, rfl⟩
    use ⟨g⁻¹ * k * g, nN.conj_mem' k hk g⟩
    simp only [Subgroup.mk_smul]
    simp only [← smul_smul, smul_inv_smul]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B = Set.univ

Tactic:
Set.eq_univ_iff_ncard,

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B.ncard = Nat.card X
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
ha : (-1) ^ (g.cycleType.card • 2 + g.cycleType.card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
smul_eq_mul,

Goal state after:
g : Perm (Fin 5)
ha : (-1) ^ (g.cycleType.card * 2 + g.cycleType.card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
⊢ g a ≠ a

Tactic:
rw [← mem_support]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
⊢ a ∈ g.support
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ ↑b = ↑c

Tactic:
← hgbc,

Goal state after:
case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
h : G
hinvab : h⁻¹ • a = ↑b
⊢ ↑b = ↑(⟨g, hg⟩ • b)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case h.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ (MulAut.conj g⁻¹) k ∈ fixingSubgroup M t

Tactic:
apply Set.conj_mem_fixingSubgroup _ hk
      rw [inv_smul_eq_iff, hg]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
this : i = j
⊢ (g • x) i = (k • x) i

Tactic:
← this,

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑i < Fintype.card α - 1
this : i = j
⊢ (g • x) i = (k • x) i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: 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 = ⊤

Tactic:
intro G

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 α
G : Subgroup ↥(alternatingGroup α)
⊢ stabilizer (↥(alternatingGroup α)) s < G → G = ⊤
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inl
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : Nat.card α < sᶜ.ncard * 2
⊢ False

Tactic:
apply h0.ne_empty

Goal state after:
case inl
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : Nat.card α < sᶜ.ncard * 2
⊢ s = ∅
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : toPerm g = 1
⊢ g = 1

Tactic:
rwa [← toPermHom_apply, map_eq_one_iff] at h

Goal state after:
case hf
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : (toPermHom G ↑(powersetCard α n)) g = 1
⊢ Function.Injective ⇑(toPermHom G ↑(powersetCard α n))
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
x✝ : ↑(powersetCard α 1)
a : α
hs : {a} ∈ powersetCard α 1
⊢ ∃ a_1, (mulActionHom_singleton G α) a_1 = ⟨{a}, hs⟩

Tactic:
exact ⟨a, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
Knorm : K.Normal
⊢ H.Normal

Tactic:
obtain rfl | rfl := Knorm.eq_bot_or_eq_top
    · grind
    · grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w✝ w : ReducedWord G A B
⊢ w.head = 1 →
    ∃ w',
      ReducedWord.prod φ w'.toReducedWord = 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 ∈ toSubgroup A B (-u)

Tactic:
hw1

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w✝ w : ReducedWord G A B
hw1 : w.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = 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 ∈ toSubgroup A B (-u)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
this✝ : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
hx' : some (l.head hl).1 = some (-a.1, x).1
this : a.1 = (l.head hl).1
⊢ a.1 = -a.1

Tactic:
← this,

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
this✝ : w'.head ∈ toSubgroup A B a.1
hl : l ≠ []
hx' : some a.1 = some (-a.1, x).1
this : a.1 = (l.head hl).1
⊢ a.1 = -a.1
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:
rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
    · rw [← Nat.not_even_iff_odd, comp_apply]
      exact fun h ↦ this h.neg_one_pow
    · rw [mem_cycleFactorsFinset_iff] at hc
      exact hc.left

Goal state after:
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
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime N.index

Tactic:
refine h1.coprime_dvd_left ?_

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
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ Nat.card ↥(map (QuotientGroup.mk' K) N) ∣ Nat.card ↥N
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 ↥N
inst✝ : (map N.subtype K).Normal
⊢ K = ⊥ ∨ K = ⊤

Tactic:
by
  have key := step2 h1 h2 h3 (K.map N.subtype) (map_subtype_le K)
  rw [← map_bot N.subtype] at key
  conv at key =>
    rhs
    rhs
    rw [← N.range_subtype, N.subtype.range_eq_map]
  rwa [map_subtype_inj, map_subtype_inj] at key

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

Goal state before:
pp: case h
α : 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}
c : ↥g.cycleFactorsFinset
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)

Tactic:
rw [← Multiset.nodup_iff_count_le_one, cycleType_def,
    Multiset.nodup_map_iff_inj_on (cycleFactorsFinset g).nodup] at h_count

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : ↥g.cycleFactorsFinset
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)
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.card • 2 ≤ 4
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
smul_eq_mul,

Goal state after:
α : 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.card * 2 ≤ 4
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ (2 • (Nat.factorization 2) 2 + (Nat.factorization 3) 2) = 4

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ (2 * (Nat.factorization 2) 2 + (Nat.factorization 3) 2) = 4
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⟩)
⊢ -(-1) ^ #(↑⟨c, hc⟩).support = 1

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:
Odd.neg_one_pow,

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⟩)
⊢ - -1 = 1

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

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'_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

Tactic:
apply h_odd
        rw [cycleType_def, Multiset.mem_map]
        exact ⟨c, hc, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this : closure {b | (↑b).IsThreeCycle} = ⊤
⊢ ⊤ ≤ _root_.commutator ↥(alternatingGroup α)

Tactic:
← this,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this : closure {b | (↑b).IsThreeCycle} = ⊤
⊢ closure {b | (↑b).IsThreeCycle} ≤ _root_.commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

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

Tactic:
and_iff_right hk,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ + η)

Tactic:
refine ⟨⟨κ.bound + η.bound, ENNReal.add_lt_top.mpr ⟨κ.bound_lt_top, η.bound_lt_top⟩, fun a => ?_⟩⟩
  exact add_le_add (Kernel.measure_le_bound _ _ _) (Kernel.measure_le_bound _ _ _)

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (swap α β)

Tactic:
rw [swap]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a ↦ ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)

Tactic:
have (a : _) : Kernel.sum (Kernel.seq κ) a (Prod.mk a ⁻¹' t) =
      ∑' n, Kernel.seq κ n a (Prod.mk a ⁻¹' t) :=
    Kernel.sum_apply' _ _ (measurable_prodMk_left ht)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ μ s✝ * (κ x✝) Set.univ = (κ x✝) Set.univ • μ s✝

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
x✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ μ s✝ * (κ x✝) Set.univ = (κ x✝) Set.univ * μ s✝
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : ∀ r ≥ 1, (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑(S.sup List.length)
⊢ ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length ≤ 1

Tactic:
contrapose! h_kraft

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
⊢ ∃ r ≥ 1, ↑r * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r