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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
have ⟨⟨m₂, s₂⟩, eq₂⟩ := f.surj n₂

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂
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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
⊢ ∀ (u' : ℤˣ) (x : G), w.toList.head? = some (u', x) → ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u → u = u'

Tactic:
intro u'

Goal state after:
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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
⊢ ∀ (x : G), w.toList.head? = some (u', x) → ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u → u = u'
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: 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)
⊢ (f.noncommCoprod g comm).range = f.range ⊔ g.range

Tactic:
apply le_antisymm

Goal state after:
case a
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)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range

case a
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)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_

Goal state after:
case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise (fun s t ↦ s.Disjoint t) l
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
x✝ : i ∈ Finset.univ
⊢ Nat.card (Perm { a // f a = i }) = (Fintype.card { a // f a = i })!

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
x✝ : i ∈ Finset.univ
⊢ Fintype.card (Perm { a // f a = i }) = (Fintype.card { a // f a = i })!
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: case hi
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, ↑a ∈ Finset.image f Finset.univ

pp: case i_inj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a₁ ∈ Finset.univ, ∀ a₂ ∈ Finset.univ, ↑a₁ = ↑a₂ → a₁ = a₂

pp: case i_surj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ b ∈ Finset.image f Finset.univ, ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = b

pp: case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, (Fintype.card { a_1 // φ a_1 = a })! = (Fintype.card { a_1 // f a_1 = ↑a })!

Tactic:
· exact fun g _ => Finset.coe_mem g

Goal state after:
case i_inj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a₁ ∈ Finset.univ, ∀ a₂ ∈ Finset.univ, ↑a₁ = ↑a₂ → a₁ = a₂

case i_surj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ b ∈ Finset.image f Finset.univ, ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = b

case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, (Fintype.card { a_1 // φ a_1 = a })! = (Fintype.card { a_1 // f a_1 = ↑a })!
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : DecidableEq α
a b : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hab' : a ≠ b
hbc : Equiv.swap b a ∈ M
⊢ Equiv.swap a a ∈ M

Tactic:
exact swap_self a ▸ one_mem M

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : x✝ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}
⊢ x✝⁻¹ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}

Tactic:
simp only [Subtype.forall, Set.mem_ofPred_eq] at hσ ⊢
    intro c hc
    rw [← hσ _ (by simp)]
    simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
this :
  ∀ (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)
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⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
simp only [hw1, inv_mem_iff, mul_one]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
this :
  ∀ (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)
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.Perm.Centralizer

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑1 c)) = x

Tactic:
OneMemClass.coe_one,

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (1 c)) = x
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case hS
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 α
h : closure (⇑(toPermHom G α) '' S \ {1}) = (toPermHom G α).range
this : IsPretransitive (↥(closure (⇑(toPermHom G α) '' S \ {1}))) α
⊢ ∀ σ ∈ ⇑(toPermHom G α) '' S \ {1}, σ.IsSwap

Tactic:
rintro - ⟨⟨σ, hσ, rfl⟩, hσ1⟩

Goal state after:
case hS
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 α
h : closure (⇑(toPermHom G α) '' S \ {1}) = (toPermHom G α).range
this : IsPretransitive (↥(closure (⇑(toPermHom G α) '' S \ {1}))) α
σ : G
hσ : σ ∈ S
hσ1 : (toPermHom G α) σ ∉ {1}
⊢ ((toPermHom G α) σ).IsSwap
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:
simp [smul_smul, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
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
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left (m₁.right * (m₁.right⁻¹ * q)) • a = m₂.left (m₁.right * (m₁.right⁻¹ * q)) • a
⊢ m₁.left q = m₂.left q

Tactic:
group at hh

Goal state after:
case left
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
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left q • a = m₂.left q • a
⊢ m₁.left q = m₂.left q
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 rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]

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

Tactic:
Nat.card_eq_fintype_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 ^ Fintype.card (G ⧸ H)
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
simp only [ne_eq, ← Subtype.ext_iff]

Goal state after:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ ¬a = b
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 : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i✝ : ι
g✝ : G i✝
w : NormalWord d
hmw : w.fstIdx ≠ some i✝
hgr : g✝ ∉ (φ i✝).range
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv (g✝ * (φ i✝) w.head)
w' : Word G := Word.cons (↑n.2) w.toWord hmw ⋯
i : ι
g : G i
hg : i = i✝ ∧ g ≍ ↑n.2 ∨ ⟨i, g⟩ ∈ w.toList
⊢ g ∈ d.set i

Tactic:
rcases hg with ⟨rfl, hg | hg⟩

Goal state after:
case inl
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
w : NormalWord d
i : ι
g : G i
hmw : w.fstIdx ≠ some i
hgr : g ∉ (φ i).range
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv (g * (φ i) w.head)
w' : Word G := Word.cons (↑n.2) w.toWord hmw ⋯
β : Type u_2
⊢ ↑n.2 ∈ d.set i

case inr
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i✝ : ι
g✝ : G i✝
w : NormalWord d
hmw : w.fstIdx ≠ some i✝
hgr : g✝ ∉ (φ i✝).range
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv (g✝ * (φ i✝) w.head)
w' : Word G := Word.cons (↑n.2) w.toWord hmw ⋯
i : ι
g : G i
h✝ : ⟨i, g⟩ ∈ w.toList
⊢ g ∈ d.set i
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range = map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range ≤ map (centralizer {g}).subtype (toPermHom g).ker

case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ map (centralizer {g}).subtype (toPermHom g).ker ≤ (kerParam g).range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ #{g | (↑g).cycleType = {n}} = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
rw [← card_map, map_subtype_of_cycleType, apply_ite Finset.card]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even ({n}.sum + {n}.card) then #{g | g.cycleType = {n}} else #∅) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
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
⊢ K = ⊥ ∨ K = N

Tactic:
have : Function.Surjective (QuotientGroup.mk' K) := Quotient.mk''_surjective

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)
⊢ K = ⊥ ∨ K = N
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Nat.card { h // IsConj g h }

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Fintype.card { h // IsConj g h }
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
⊢ closure {σ | σ.IsSwap} ≤ ⨆ s, ofSubtype.range

Tactic:
Subgroup.closure_le

Goal state after:
α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
⊢ {σ | σ.IsSwap} ⊆ ↑(⨆ s, ofSubtype.range)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ IsPreprimitive (Perm α) ↑(Set.powersetCard α 2)

Tactic:
apply Set.powersetCard.isPreprimitive_perm

Goal state after:
case h_one_le
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

case hn
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 2 < Nat.card α

case hα
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ closure {g | (↑g).IsThreeCycle} ≤ ⨆ s, (ofSubtype ↑s).range

Tactic:
Subgroup.closure_le

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ {g | (↑g).IsThreeCycle} ⊆ ↑(⨆ s, (ofSubtype ↑s).range)
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} = ⊤
⊢ closure {b | (↑b).IsThreeCycle} ≤ _root_.commutator ↥(alternatingGroup α)

Tactic:
Subgroup.closure_le

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ N = ⊤

Tactic:
have : IsPreprimitive (alternatingGroup α) (Set.powersetCard α 3) := by
    refine Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num) ?_ ?_
    · exact lt_of_lt_of_le (by norm_num) hα
    · simpa using hα'

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ N = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ ∀ (a : QuaternionGroup n), a * 1 = a

Tactic:
rintro (i | i)
    · exact congr_arg a (add_zero i)
    · exact congr_arg xa (add_zero i)

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

Goal state before:
pp: case hx
⊢ orderOf ?x = Nat.card (QuaternionGroup 1)

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case hx
⊢ orderOf ?x = Fintype.card (QuaternionGroup 1)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ closure {g | (↑g).cycleType = {2, 2}} ≤ ⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s)

Tactic:
Subgroup.closure_le

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ {g | (↑g).cycleType = {2, 2}} ⊆ ↑(⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Subgroup.map (commutator ↥H).subtype (commutator ↥(commutator ↥H)) ≤ Subgroup.centralizer ↑(commutator ↥H)
⊢ commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)

Tactic:
by
      simpa [SetLike.le_def, Subgroup.mem_center_iff, Subgroup.mem_centralizer_iff] using h

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 ↔ x = y

Tactic:
hammingDist_eq_zero

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ x = y ↔ x = y
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ ⊥.sets ↔ x✝ ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, ↑(hammingDist (ofHamming x) (ofHamming y)) ≤ C}

Tactic:
refine iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => ?_⟩

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝⁴ : Set (Hamming β)
x✝³ : Hamming β
x✝² : x✝³ ∈ x✝⁴ᶜ
x✝¹ : Hamming β
x✝ : x✝¹ ∈ x✝⁴ᶜ
⊢ ↑(hammingDist (ofHamming x✝³) (ofHamming x✝¹)) ≤ ↑(Fintype.card ι)
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 γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ∞
h : ∀ᵐ (b : β) ∂κ a, (η b) (toMeasurable ((η ∘ₖ κ) a) s) < ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η b) s < ∞

Tactic:
filter_upwards [h] with b hb using (measure_mono (subset_toMeasurable _ _)).trans_lt hb

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 : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ (if a ∈ s then (κ a) Set.univ else (η a) Set.univ) = 1

Tactic:
measure_univ,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ (if a ∈ s then 1 else (η a) Set.univ) = 1