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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • (fun m ↦ m • x) ⟨g, hg⟩ ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
simp_rw [h, ← hl, show a = w by simpa [← hl, startsWith] using hg, startsWith.smul_def,
        inv_smul_smul]
      exact Or.inr rfl

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1

Tactic:
classical apply Nat.find_min'

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ ⊤.lowerCentralSeries (nilpotencyClass H + 1) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries G n.succ = ⊤

Tactic:
Nat.succ_eq_add_one,

Goal state after:
case pos.succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries G (n + 1) = ⊤
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : IsTrivialBlock B
⊢ IsTrivialBlock (⇑f '' B)

Tactic:
obtain hB | hB := hB

Goal state after:
case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f '' B)

case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ IsTrivialBlock (⇑f '' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : IsTrivialBlock B
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
obtain hB | hB := hB

Goal state after:
case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f ⁻¹' B)

case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ Disjoint B (s • B)

Tactic:
by
  simpa using hB.disjoint_smul_set_smul (g := 1) (by simpa using hs)

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
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ a ∈ g • B

Tactic:
rw [← hg]

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ g • b ∈ g • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ ∃ g, g • a = x

Tactic:
← MulAction.mem_orbit_iff,

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ x ∈ orbit G a
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ sign l.prod = 1 ↔ Even l.length

Tactic:
sign_prod_list_swap hl,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ (-1) ^ l.length = 1 ↔ Even l.length
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg : g.cycleType = {2, 2}
⊢ g ∈ ↑(alternatingGroup α)

Tactic:
simp [mem_alternatingGroup, sign_of_cycleType, hg, ← Units.val_inj]

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

Goal state before:
pp: case inr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ B = univ

Tactic:
rw [← top_eq_univ, eq_top_iff]

Goal state after:
case inr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ ⊤ ⊆ B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ (↑((MulAut.conj g⁻¹) k)).support ⊆ s ↔ (↑k).support ⊆ g • s

Tactic:
← ConjAct.toConjAct_smul_eq_mulAut_conj,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ (↑(ConjAct.toConjAct g⁻¹ • k)).support ⊆ s ↔ (↑k).support ⊆ g • s
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard.succ = k.succ

Tactic:
Nat.succ_eq_add_one,

Goal state after:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard + 1 = k.succ
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard + 1 = k.succ

Tactic:
Nat.succ_eq_add_one,

Goal state after:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ t.ncard + 1 = k + 1
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 = s'.encard

Tactic:
hst

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 = (insert a (Subtype.val '' t)).encard
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 : s = t
x✝ : ↥(ofFixingSubgroup M t)
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M s

Tactic:
hst

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
hst : s = t
x✝ : ↥(ofFixingSubgroup M t)
x : α
hxt : x ∈ ofFixingSubgroup M t
⊢ x ∈ ofFixingSubgroup M t
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) t)

Tactic:
rw [htt']

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
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' := ⋯ }
y : β
hy : y ∈ ofFixingSubgroup N t
x : α
hx : f x = y
⊢ ∃ a, f' a = ⟨y, hy⟩

Tactic:
use ⟨x, ?_⟩

Goal state after:
case h
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 α := ⋯
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) := ⋯
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) := ⋯
y : β
hy : y ∈ ofFixingSubgroup N t
x : α
hx : f x = y
⊢ f' ⟨x, ?w⟩ = ⟨y, hy⟩

case w
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' := ⋯ }
y : β
hy : y ∈ ofFixingSubgroup N t
x : α
hx : f x = y
⊢ x ∈ ofFixingSubgroup M s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ k • g • a = x

Tactic:
hgab,

Goal state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ k • b = x
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h.inr.inr
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
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := ⋯
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hsgs_ne_top : s ∪ g • s ≠ ⊤
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsPretransitive ↥(fixingSubgroup G t) ↥(ofFixingSubgroup G t)

Tactic:
exact IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs_trans hsgs_ne_top

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : g ∈ stabilizer (Perm α) s
hg3 : g.IsThreeCycle
⊢ G = ⊤

Tactic:
rw [eq_top_iff, ← Subgroup.map_subtype_le_map_subtype,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : g ∈ stabilizer (Perm α) s
hg3 : g.IsThreeCycle
⊢ alternatingGroup α ≤ Subgroup.map (alternatingGroup α).subtype G
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : 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 α ≤ 2
⊢ Nat.card ↥G = Nat.card (Perm α)

Tactic:
simp only [Nat.card_eq_fintype_card]

Goal state after:
case inl
α : 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 α ≤ 2
⊢ Fintype.card ↥G = Fintype.card (Perm α)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
⊢ a ∈ m → 2 ≤ a

Tactic:
rw [← hg]

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
a : ℕ
⊢ a ∈ g.cycleType → 2 ≤ a
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ ((kerParam g) (u, v)) x = (ofSubtype u) x

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq,
      ← notMem_support]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : x ∉ g.support
⊢ x ∉ ((noncommPiCoprod ⋯) (u, v).2).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c) := fun c ↦ ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ↑(v ⟨g.cycleOf x, hx⟩) x = ↑p x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support] at hx

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c) := fun c ↦ ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx✝ : g.cycleOf x ∈ g.cycleFactorsFinset
hx : g x ≠ x
⊢ ↑(v ⟨g.cycleOf x, hx✝⟩) x = ↑p x
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons.refine_1
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ w'.fstIdx ≠ some i

Tactic:
Word.fstIdx,

Goal state after:
case cons.refine_1
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ Option.map Sigma.fst w'.toList.head? ≠ some i
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ (base φ).range ≤ (of i).range

Tactic:
rw [← of_comp_eq_base i]
          rintro _ ⟨h, rfl⟩
          exact MonoidHom.mem_range.2 ⟨φ i h, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
by
  rw [deterministic_apply, setLIntegral_dirac' hf hs]

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:
simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
this : (fun i ↦ ((if i = 0 then κ else 0) a) s) = fun i ↦ if i = 0 then (κ a) s else 0
⊢ (κ a) s = ∑' (n : ℕ), ((if n = 0 then κ else 0) a) s

Tactic:
rw [this, tsum_ite_eq]

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
⊢ 0 < hammingDist x y ↔ x ≠ y

Tactic:
← hammingDist_ne_zero,

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingNorm (-x + y)

Tactic:
by
  simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
⊢ (concatFn w).length = ∑ i, (↑(w i)).length

Tactic:
simp [List.sum_ofFn, concatFn]

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ (concatFn w).length ∈ Finset.Icc r (r * S.sup List.length)

Tactic:
concatFn_length,

Goal state after:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ ∑ i, (↑(w i)).length ∈ Finset.Icc r (r * S.sup List.length)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ ((κ ∥ₖ η) x) s = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1

Tactic:
parallelComp_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ ((κ x.1).prod (η x.2)) s = ∫⁻ (b : β), (η x.2) (Prod.mk b ⁻¹' s) ∂κ x.1