mathlib-initiative/mathlib-tactics huggingface dataset:
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
hab : g a ≠ a
⊢ False

Tactic:
have : 2 ≤ (({a, g a} : Finset α)ᶜ).card := by
    rw [← Nat.add_le_add_iff_left, Finset.card_add_card_compl]
    rw [← Nat.card_eq_fintype_card]
    rw [Finset.card_pair hab.symm]
    exact hα4

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
hab : g a ≠ a
this : 2 ≤ {a, g a}ᶜ.card
⊢ False
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
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
⊢ (swap (g a) d) ((swap (g a) c) a) = a

Tactic:
swap_apply_of_ne_of_ne (x := a) hab.symm hc.1.symm

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
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
⊢ (swap (g a) d) a = a
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ map Perm.ofSubtype (alternatingGroup ↥s).subtype.range =
    map (alternatingGroup α).subtype (Perm.ofSubtype.range.subgroupOf (alternatingGroup α))

Tactic:
range_subtype,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ map Perm.ofSubtype (alternatingGroup ↥s) =
    map (alternatingGroup α).subtype (Perm.ofSubtype.range.subgroupOf (alternatingGroup α))
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
⊢ h⁻¹ • a = ⟨g, hg⟩ • h⁻¹ • a

Tactic:
inv_smul_eq_iff,

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
⊢ a = h • ⟨g, hg⟩ • h⁻¹ • a
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
⊢ Injective ⇑(ofFixingSubgroup_equivariantMap M s)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (ofFixingSubgroup_equivariantMap M s) ⟨x, hx⟩ = (ofFixingSubgroup_equivariantMap M s) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: 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
⊢ g⁻¹ • s = t

Tactic:
inv_smul_eq_iff,

Goal state after:
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
⊢ s = g • t
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
⊢ Injective ⇑(ofFixingSubgroup_of_inclusion M hst)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : (ofFixingSubgroup_of_inclusion M hst) ⟨x, hx⟩ = (ofFixingSubgroup_of_inclusion M hst) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩,
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ s.encard + 1 = (⇑f '' s).encard + 1

Tactic:
hf.injective.encard_image

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩,
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ s.encard + 1 = s.encard + 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ sᶜ ≠ Set.univ

Tactic:
simpa [Set.nonempty_iff_ne_empty] using hs_nonempty

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
x : α
hx : x ∈ s
⊢ k x = x

Tactic:
← Perm.notMem_support

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
x : α
hx : x ∈ s
⊢ x ∉ k.support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ ⟨swap a b * swap c d, ⋯⟩ • a = b

Tactic:
simp only [Subgroup.smul_def, Perm.smul_def, Perm.coe_mul]

Goal state after:
case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
c d : α
hc : c ∈ tᶜ
hd : d ∈ tᶜ
hcd : c ≠ d
⊢ (⇑(swap a b) ∘ ⇑(swap c d)) 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 α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ a ∈ ⟨k, ?m.152⟩ • B

Tactic:
rw [mem_fixingSubgroup_iff] at hk

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk✝ : k ∈ fixingSubgroup M s
hk : ∀ y ∈ s, k • y = y
hx' : ⟨k, hk✝⟩ • b ∈ sᶜ
⊢ a ∈ ⟨k, ⋯⟩ • 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
n : N
⊢ S.rightHom (S.inl n) = 1

Tactic:
rw [← MonoidHom.mem_ker, ← S.range_inl_eq_ker_rightHom, MonoidHom.mem_range]
  exact exists_apply_eq_apply S.inl n

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g +ᵥ a = a
⊢ AddAction.toPerm g = 1

Tactic:
← addAction_faithful hn hα

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g +ᵥ a = a
⊢ AddAction.toPerm g = 1
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
⊢ g = 1

Tactic:
apply toPerm_injective (α := G) (β := α)

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 = toPerm 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
⊢ ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a

Tactic:
intro x hx

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
⊢ ∃ k, x = k • a
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
h₁ : S.IsConj s₁ s₂
h₂ : S.IsConj s₂ s₃
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁

Goal state after:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
h₂ : S.IsConj s₂ s₃
n₁ : N
hn₁ : ⇑s₁ = fun g ↦ S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
⊢ S.IsConj s₁ s₃
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ Nat.Prime (Nat.card ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ))

Tactic:
convert! Nat.prime_two

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ Nat.card ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ) = 2
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map f x = Pi.map f y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
choose c hc using fun i ↦ (hf i).exists_of_eq congr($eq i)
    exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ stabilizerEquiv_invFun g (stabilizerEquiv_invFun (fun i ↦ Equiv.symm (g i)) a) = a

Tactic:
rw [stabilizerEquiv_invFun_eq _ (comp_stabilizerEquiv_invFun _ a)]
    exact congr_arg Subtype.val ((g <| f a).right_inv _)

Goal state after:
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
⊢ ∀ x ∈ p, 2 ≤ x.length

Tactic:
intro x hx

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
x : List α
hx : x ∈ p
⊢ 2 ≤ x.length
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : 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 ∈ p, ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) a = a.length

Tactic:
intro x hx

Goal state after:
case h
α : 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
x : List α
hx : x ∈ p
⊢ ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) x = x.length
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ Function.fixedPoints ⇑g
⊢ ∀ (d : ↥g.cycleFactorsFinset), x ∉ (↑d).support

Tactic:
intro d hx'

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ Function.fixedPoints ⇑g
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d).support
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ #((↑τ).support.biUnion fun c ↦ (↑c).support) = ∑ c ∈ (↑τ).support, #(↑c).support

Tactic:
Finset.card_biUnion

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ ∑ u ∈ (↑τ).support, #(↑u).support = ∑ c ∈ (↑τ).support, #(↑c).support

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (↑(↑τ).support).PairwiseDisjoint fun c ↦ (↑c).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
α β x✝ y✝ z✝ : H.LeftTransversal
h : diff (MonoidHom.id ↥H) x✝ y✝ = 1
h' : diff (MonoidHom.id ↥H) y✝ z✝ = 1
⊢ 1 * diff (MonoidHom.id ↥H) y✝ z✝ = 1

Tactic:
h',

Goal state after:
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
⊢ 1 * 1 = 1
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), ⋯⟩ =
    (∏ q, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩) * h ^ H.index

Tactic:
index_eq_card,

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), ⋯⟩ =
    (∏ q, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩) * h ^ Nat.card (G ⧸ H)
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
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ N.relIndex K.subtype.range = N.index

Tactic:
range_subtype,

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
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ N.relIndex K = N.index
Module: Mathlib.GroupTheory.Perm.Centralizer

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

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

Tactic:
· have : 0 < m.prod := Multiset.prod_pos <| fun a ha => zero_lt_two.trans_le (hm.2 a ha)
      positivity

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Characteristic
⊢ (kleinFour α).Normal

Tactic:
apply Subgroup.normal_of_characteristic

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ g ∈ commutatorSet ↥(alternatingGroup α)

Tactic:
exact hg.mem_commutatorSet_alternatingGroup h5

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
x✝ : Subgroup G
⊢ IsCyclic ↥⁅x✝, x✝⁆

Tactic:
induction (⊤ : Subgroup G) using WellFoundedLT.induction with

Goal state after:
case ind
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⁅H, H⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
hϕ : ∀ (a : K), ϕ a = 1
p : G
k : K
⊢ ϕ k - 1 = ↑0

Tactic:
rw [hϕ, sub_self, Int.cast_zero]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ⁅K, ↑P⁆ ≤ ⁅⊤, ⊤⁆

Tactic:
exact Subgroup.commutator_mono le_top le_top

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
i : ι
a✝ : i ∈ univ
⊢ x i = y i → f i (x i) = f i (y i)

Tactic:
simp +contextual

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 α β
s t : Set β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ a) (Set.univ ∩ s) ≤ κ.bound

Tactic:
exact measure_le_bound κ a _

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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (κ a) (f '' Set.univ) ≤ κ.bound

Tactic:
exact measure_le_bound κ a _

Goal state after:
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 γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((η.restrict hs ∘ₖ κ) a) t = (((η ∘ₖ κ).restrict hs) a) t

Tactic:
comp_apply' _ _ _ ht,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ((η.restrict hs) b) t ∂κ a = (((η ∘ₖ κ).restrict hs) a) t