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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ (List.rec [w] (fun head tail tail_ih ↦ if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
        g.toWord)[0]? =
    some w

Tactic:
rw [show g.toWord = g.toWord.head (by grind) :: g.toWord.tail by grind]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ (List.rec [w] (fun head tail tail_ih ↦ if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
        (g.toWord.head ⋯ :: g.toWord.tail))[0]? =
    some w
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
⊢ {x_1 | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1} =
    (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
by
  ext i
  constructor
  · rintro ⟨-, ⟨⟨g, hg⟩, rfl⟩, rfl⟩
    set l := g.toWord with hl
    have h : (⟨g, hg⟩ : startsWith w) = ⟨mk g.toWord, by simp [g.mk_toWord, hg]⟩ := by
      simp [g.mk_toWord]
    match l with
    | [] => simp [← hl, startsWith] at hg
    | [a] =>
      simp_rw [h, ← hl, show a = w by simpa [← hl, startsWith] using hg, startsWith.smul_def,
        inv_smul_smul]
      exact Or.inr rfl
    | a :: b :: l =>
      have ha : a = w := by simpa [← hl, startsWith] using hg
      have h1 := isReduced_cons_cons.mp (hl ▸ isReduced_toWord)
      refine Or.inl (Set.mem_biUnion (x := b) (by grind) ?_)
      simp_rw [h, ← hl, ha, ← List.singleton_append (l := b :: l), ← mul_mk, startsWith.smul_def,
        mul_smul, inv_smul_smul]
      exact ⟨⟨mk (b :: l), by simp [startsWith, h1.2.reduce_eq]⟩, rfl⟩
  · rintro (⟨-, ⟨w', rfl⟩, -, ⟨hw, rfl⟩, ⟨g, hg⟩, rfl⟩ | rfl)
    · exact ⟨mk [w] • g • x, ⟨⟨mk [w] * g, startsWith_mk_mul g
        ((startsWith.disjoint_iff_ne.mpr hw).notMem_of_mem_left hg)⟩,
        mul_smul (mk [w]) g x⟩, inv_smul_smul (mk [w]) (g • x)⟩
    · exact ⟨mk [w] • i, ⟨⟨mk [w], rfl⟩, rfl⟩, inv_smul_smul (mk [w]) i⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
Group.nilpotencyClass_def,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ Nat.find ⋯ = 0 ↔ Subsingleton G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1

Tactic:
simp only [nilpotencyClass_zero_iff_subsingleton, zero_tsub] at *

Goal state after:
case pos.zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton (G ⧸ center G)
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
⊢ nilpotencyClass (G ⧸ center G) ≤ n

pp: case a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)

Tactic:
· apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
      apply comap_injective (f := (mk' (center G))) Quot.mk_surjective
      rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]
      exact upperCentralSeries_nilpotencyClass

Goal state after:
case a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
⊢ P G

Tactic:
by
  obtain ⟨n, h⟩ : ∃ n, Group.nilpotencyClass G = n := ⟨_, rfl⟩
  induction n generalizing G with
  | zero =>
    have := nilpotencyClass_zero_iff_subsingleton.mp h
    exact hbase _
  | succ n ih =>
    have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
    exact hstep _ (ih _ hn)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic 0)

Tactic:
← Nat.bot_eq_zero,

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic ⊥)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ IsBlock G ((fun a ↦ orbit (↥N) a) a)

Tactic:
exact .orbit_of_normal a

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ ∀ ⦃g : G⦄,
    ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inl
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).Subsingleton
⊢ ∀ (x : X), ∃ g, g • a = x

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:
· exfalso; apply ha
      rw [Set.subsingleton_iff_singleton (mem_orbit_self a)] at H
      simp only [mem_fixedPoints]
      intro g
      rw [← Set.mem_singleton_iff]; rw [← H]
      exact mem_orbit a g

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), ∃ g, g • a = x
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
⊢ False

Tactic:
have hab : g a ≠ a := by rw [← mem_support]; exact ha

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
⊢ 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
hka : k • a = a
⊢ False

Tactic:
have hkga : k • (g a) = c := by
    simp only [Perm.smul_def, coe_mul, Function.comp_apply, swap_apply_left, k]
    rw [swap_apply_of_ne_of_ne hc.2 hcd]

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
hka : k • a = a
hkga : k • g a = c
⊢ False
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
h : B.Nontrivial
⊢ B = univ

Tactic:
obtain ⟨a, ha, b, hb, h⟩ := h

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 = univ
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
⊢ ∃ g, g • x = y

Tactic:
· -- gx • x = x1 :: a
    obtain ⟨gx, x1, hgx⟩ := exists_smul_of_last_eq G a x
    -- gy • y = y1 :: a
    obtain ⟨gy, y1, hgy⟩ := exists_smul_of_last_eq G a y
    -- g • x1 = y1,
    obtain ⟨g, hg⟩ := hn.exists_smul_eq x1 y1
    use gy⁻¹ * g * gx
    ext i
    simp only [mul_smul, smul_apply, inv_smul_eq_iff]
    simp only [← smul_apply _ _ i, hgy, hgx]
    simp only [smul_apply]
    rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
    · simp [ofStabilizer.snoc_castSucc, ← hg, SetLike.val_smul, subgroup_smul_def]
    · simp only [ofStabilizer.snoc_last, ← hg]
      exact g.prop

Goal state after:
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
hn1 : 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 α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ s ∪ g • s ≠ ⊤

Tactic:
by
        apply Set.union_ne_univ_of_ncard_add_ncard_lt
        rwa [Set.ncard_smul_set, hsn, ← two_mul]

Goal state after:
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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
x✝ : ↥(fixingSubgroup M s)
g : M
hg : g ∈ fixingSubgroup M s
⊢ φ g ∈ fixingSubgroup N t

Tactic:
simp only [mem_fixingSubgroup_iff] at hg ⊢
      intro y hy
      suffices ∃ x ∈ s, y = f x by
        obtain ⟨x, hx, rfl⟩ := this
        rwa [← map_smulₛₗ, hg]
      obtain ⟨x, rfl⟩ := hf.surjective y
      simpa only [Set.mem_image, t, eq_comm] using! hy

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

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α < 4
⊢ alternatingGroup α ≤ G

Tactic:
rw [Nat.lt_succ_iff] at hα4

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ alternatingGroup α ≤ G
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)

Tactic:
show Nat.card α - 2 = n + 2 by grind

Goal state after:
case inr
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
· suffices Subsingleton (powersetCard α n) by infer_instance
      rw [not_le] at hn'
      rw [← Finite.card_le_one_iff_subsingleton, powersetCard.card,
        Nat.choose_eq_zero_iff.mpr hn']
      simp

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
⊢ derivedSeries G n = ⊤

Tactic:
match n with
  | 0 => simp
  | n + 1 =>
    rw [derivedSeries_succ, derivedSeries_eq_top, commutator_eq_self]

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

Goal state before:
pp: case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
this : ∃ σ ∈ S, ∃ a ∈ {x | Equiv.swap x y ∈ closure S}, σ • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ False

Tactic:
obtain ⟨σ, hσ, a, ha, hσa⟩ := this
    obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ
    have := ne_of_mem_of_not_mem ha hσa
    rw [Perm.smul_def, ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at this
    refine hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha)
    obtain rfl | rfl := this <;> simpa [Equiv.swap_comm] using subset_closure hσ

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ #{g | (↑g).cycleType = m} = 0

Tactic:
· -- m does not correspond to a permutation, or to an odd one,
    rw [← Finset.card_map, map_subtype_of_cycleType]
    rw [apply_ite Finset.card, Finset.card_empty]
    split_ifs with hm'
    · rw [Equiv.Perm.card_of_cycleType, if_neg]
      obtain hm | hm := not_and_or.mp hm
      · exact hm
      · contradiction
    · rfl

Goal state after:
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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
⊢ ∑ c ∈ τ.support, #(↑c).support = #c.support * 2

Tactic:
have H : (⟨c, hc⟩ : g.cycleFactorsFinset) ≠ ⟨d, hd⟩ := Subtype.coe_ne_coe.mp hm'

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
H : ⟨c, hc⟩ ≠ ⟨d, hd⟩
⊢ ∑ c ∈ τ.support, #(↑c).support = #c.support * 2
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 φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.36
w : NormalWord d
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
⊢ motive w

Tactic:
rcases w with ⟨w, head, h3⟩
  convert! base head ⟨w, 1, h3⟩ rfl ?_
  · simp [base_smul_def]
  · induction w using Word.consRecOn with
    | empty => exact empty
    | cons i g w h1 hg1 ih =>
      convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
      · simp only [Word.cons, NormalWord.cons, map_one, mul_one,
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
      · apply d.injective i
        simp only [NormalWord.cons, equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm,
          map_one, mul_one, mul_inv_cancel, (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
      · rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / (2 * n).gcd i.val

Tactic:
conv_lhs => rw [← ZMod.natCast_zmod_val i]
  rw [← a_one_pow, orderOf_pow, orderOf_a_one]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
by
  refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_ <;>
      refine fun hP h ↦ P.not_dvd_index (h.trans ?_)
  · rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]
    exact Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)
  · exact Subgroup.index_dvd_of_le hP

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Nonempty α
⊢ ¬IsMarkovKernel 0

Tactic:
by_contra h
  let x : α := Nonempty.some inferInstance
  have h1 : (0 : Measure β) .univ = 1 := (h.isProbabilityMeasure x).measure_univ
  simp at h1

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 z : (i : ι) → β i
⊢ hammingDist x z ≤ hammingDist x y + hammingDist y z

Tactic:
classical
    unfold hammingDist
    refine le_trans (card_mono ?_) (card_union_le _ _)
    rw [← filter_or]
    exact monotone_filter_right _ fun i _ h ↦ (h.ne_or_ne _).imp_right Ne.symm

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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (if a ∈ s then (κ a) Set.univ else (η a) Set.univ) ≤ max κ.bound η.bound

Tactic:
exact (ite_le_sup _ _ _).trans (sup_le_sup (measure_le_bound _ _ _) (measure_le_bound _ _ _))

Goal state after:
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
this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
n : ℕ
⊢ Measurable fun a ↦ ((κ.seq n) a) (Prod.mk a ⁻¹' t)

Tactic:
exact measurable_kernel_prodMk_left_of_finite ht inferInstance

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ ((κ.map fun x ↦ (f x, g x)).snd x) s = ((κ.map g) x) s

Tactic:
snd_apply' _ _ hs,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ ((κ.map fun x ↦ (f x, g x)) x) (Prod.snd ⁻¹' s) = ((κ.map g) x) s
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ.swapRight.snd a) s = (κ.fst a) s

Tactic:
snd_apply' _ _ hs,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ.swapRight a) (Prod.snd ⁻¹' s) = (κ.fst a) s
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst✝¹ : IsSFiniteKernel η
κ : Kernel X Y
inst✝ : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), (η b) s ∂κ a = ((κ ⊗ₖ prodMkLeft X η).snd a) s

Tactic:
snd_apply' _ _ hs,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst✝¹ : IsSFiniteKernel η
κ : Kernel X Y
inst✝ : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), (η b) s ∂κ a = ((κ ⊗ₖ prodMkLeft X η) a) (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ((κ ⊗ₖ prodMkLeft X (Kernel.id ×ₖ η)).snd a) s

Tactic:
snd_apply' _ _ hs,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝ : IsSFiniteKernel η
a : X
s : Set (Y × Z)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y), ((prodMkLeft X η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a =
    ((κ ⊗ₖ prodMkLeft X (Kernel.id ×ₖ η)) a) (Prod.snd ⁻¹' s)