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

Goal state before:
pp: case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
h2 : (∀ y ∈ w.head?, m.fst ≠ y.fst) ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w
⊢ { toList := w, ne_one := ⋯, chain_ne := ⋯ }.fstIdx ≠ some m.fst

Tactic:
simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]

Goal state after:
case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
h2 : (∀ y ∈ w.head?, m.fst ≠ y.fst) ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w
⊢ ∀ (x : M m.fst), ¬w.head? = some ⟨m.fst, x⟩
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : cs.IsReduced ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Tactic:
simpa [hω₁.eq, hω₂.eq, wordProd_append] using this

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos.mpr
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂ →
    m₁ = m₂ * (w.toList.head ⋯).snd

Tactic:
rintro (⟨_, h, rfl⟩ | hm')
          · simp only [Sigma.ext_iff, heq_eq_eq, true_and] at h
            subst h
            rfl
          · simp only [fstIdx, Option.map_eq_some_iff, Sigma.exists,
              exists_and_right, exists_eq_right, not_exists] at hm'
            exact (hm'.1 (w.toList.head hnil).2 (by rw [List.head?_eq_some_head])).elim

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : x ∈ _w₁✝.toList.getLast?
y : (i : ι) × M i
hy : y ∈ _w₂✝.toList.head?
⊢ x.fst ≠ y.fst

Tactic:
rw [toList_getLast?, Option.mem_some_iff] at hx

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : ⟨j✝, _w₁✝.last⟩ = x
y : (i : ι) × M i
hy : y ∈ _w₂✝.toList.head?
⊢ x.fst ≠ y.fst
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ cs.rightInvSeq (i :: ω)
⊢ cs.IsReflection t

Tactic:
dsimp [rightInvSeq] at ht

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
⊢ cs.IsReflection t
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * cs.wordProd (alternatingWord j i (2 * (k + 1)))

Tactic:
(by ring : 2 * (k + 1) = 2 * k + 1 + 1),

Goal state after:
case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * cs.wordProd (alternatingWord j i (2 * k + 1 + 1))
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ g / (fun x ↦ x) g = 1

Tactic:
div_self'

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ 1 = 1
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
⊢ Odd (Nat.card G)

Tactic:
have := Fintype.ofFinite G
  by_contra h
  rw [Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card] at h
  obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card 2 h
  exact hφ.orderOf_ne_two_of_involutive h2 g hg

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ map f (S.lowerCentralSeries (d + 1)) = (map f S).lowerCentralSeries (d + 1)

Tactic:
rw [lowerCentralSeries_succ, lowerCentralSeries_succ, Subgroup.map_commutator, hd]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥

Tactic:
· intro h
    rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]
    exact lowerCentralSeries_antitone _ h

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G✝ : Type u_1
inst✝² : Group G✝
N : Subgroup G✝
inst✝¹ : N.Normal
G : Type u_2
inst✝ : CommGroup G
⊢ Group.IsNilpotent G

Tactic:
by
  use 1
  rw [upperCentralSeries_one]
  apply CommGroup.center_eq_top

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

Goal state before:
pp: case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B

Tactic:
convert! IsTrivialBlock.smul H g⁻¹

Goal state after:
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ B = g⁻¹ • g • B
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ Group.IsNilpotent G

Tactic:
have hcq : Nat.card (G ⧸ center G) < Nat.card G := by
      rw [card_eq_card_quotient_mul_card_subgroup (center G)]
      apply lt_mul_of_one_lt_right Nat.card_pos
      exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)

Goal state after:
case hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
hcq : Nat.card (G ⧸ center G) < Nat.card G
⊢ Group.IsNilpotent G
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
⊢ (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
    ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B

Tactic:
← not_disjoint_iff_nonempty_inter,

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
⊢ (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
    ∀ ⦃g₁ g₂ : G⦄, ¬Disjoint (g₁ • B) (g₂ • B) → g₁ • B = g₂ • B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B

Tactic:
← not_disjoint_iff_nonempty_inter,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, ¬Disjoint (g • B) B → g • B = B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = g • h • B

Tactic:
by
    rw [← this]; rfl

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
rw [hG0, minFac_zero] at hHp

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : B.ncard * 0 = Nat.card X
⊢ B = Set.univ

Tactic:
rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key
    exact (IsEmpty.exists_iff.mp hB_ne).elim

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : IsCyclic ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3

Tactic:
rw [← isMulCommutative_iff_card_le_three]; exact IsCyclic.isMulCommutative

Goal state after:
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 α
a : α
s : Set ↥(ofStabilizer M a)
m : ↥(fixingSubgroup (↥(stabilizer M a)) s)
⊢ ↑↑m ∈ fixingSubgroup M (insert a (Subtype.val '' s))

Tactic:
simp [fixingSubgroup_of_insert]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
hgxt : g • x ∈ s
⊢ x ∈ t

Tactic:
rw [← hg] at hgxt

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
hgxt : g • x ∈ g • t
⊢ x ∈ t
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
have hα : Set.encard (_root_.Set.univ : Set α) = 2 := by
    rw [← Set.encard_add_encard_compl s]
    have : (1 + 1 : ENat) = 2 := by norm_num
    convert! this <;>
    · apply le_antisymm
      · assumption
      rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
      aesop

Goal state after:
case inr.inr
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : univ.encard = 2
⊢ ∃ g, g.IsSwap ∧ g ∈ G
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case right
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
ha : a ∈ s
x : α
⊢ x ∈ s ↔ x ∈ insert a (Subtype.val '' Subtype.val ⁻¹' s)

Tactic:
by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]

Goal state after:
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
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (S.rightHom (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * S'.rightHom e' = 1

Tactic:
simpa only [Function.surjInv_eq] using inv_mul_cancel (S'.rightHom e')

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

Goal state before:
pp: α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
wlog! hn : 2 * n ≤ Nat.card α

Goal state after:
case inr
α : 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
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α 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
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) ((u, w.head) :: w.toList)

Tactic:
refine List.isChain_cons.2 ⟨?_, w.chain⟩

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
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ∀ y ∈ w.toList.head?, (u, w.head).2 ∈ toSubgroup A B (u, w.head).1 → (u, w.head).1 = y.1
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G},
    (∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤) → H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), ((F i).subgroupOf (F (i + 1))).Normal
ih1 : F (n + 1) = ⊤
⊢ (F (0 + 1)).IsSubnormal

Tactic:
refine ih ⟨fun n ↦ F (n + 1), ?_⟩

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G},
    (∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤) → H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), ((F i).subgroupOf (F (i + 1))).Normal
ih1 : F (n + 1) = ⊤
⊢ (Monotone fun n ↦ F (n + 1)) ∧
    (∀ (i : ℕ), (((fun n ↦ F (n + 1)) i).subgroupOf ((fun n ↦ F (n + 1)) (i + 1))).Normal) ∧
      (fun n ↦ F (n + 1)) 0 = F (0 + 1) ∧ (fun n ↦ F (n + 1)) n = ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
⊢ (comap f H).IsSubnormal

Tactic:
apply step _ (comap f K) (comap_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]
    exact (comap_mono hN).trans (le_normalizer_comap f)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∉ Function.fixedPoints ⇑g
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
Function.mem_fixedPoints_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : ¬g x = x
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
simp [SameCycle.rfl, hx, and_self]

Goal state after:
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
hx' : x ∈ (↑d).support
⊢ False

Tactic:
Function.mem_fixedPoints_iff,

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 : g x = x
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d).support
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0

Tactic:
Equiv.Perm.card_of_cycleType_mul_eq

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
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
⊢ False

Tactic:
let τ : Equiv.Perm g.cycleFactorsFinset := Equiv.swap ⟨c, hc⟩ ⟨d, hd⟩

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⟩
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↥(kerParam g).range = (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
by
  rw [Fintype.card_coeSort_range (kerParam_injective g)]
  rw [Fintype.card_prod, Fintype.card_perm, Fintype.card_pi, card_fixedPoints]
  apply congr_arg
  rw [Finset.univ_eq_attach, g.cycleFactorsFinset.prod_attach (fun i ↦ Fintype.card (zpowers i)),
    cycleType, Finset.prod_map_val]
  refine Finset.prod_congr rfl (fun x hx ↦ ?_)
  rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ Nat.card ↥(alternatingGroup α) = 12

Tactic:
have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp
  rw [nat_card_alternatingGroup, hα4]
  decide

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False

Tactic:
injection h1 with h2

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False
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]

Goal state after:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑i.val) = 2 * n / (2 * n).gcd i.val
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : Nontrivial ↥H
⊢ ⁅H, H⁆ < H

Tactic:
rw [← H.range_subtype, MonoidHom.range_eq_map, ← Subgroup.map_commutator,
    Subgroup.map_subtype_lt_map_subtype]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : Nontrivial ↥H
⊢ ⁅⊤, ⊤⁆ < ⊤
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Nonempty α
h : IsMarkovKernel 0
x : α := ⋯.some
h1 : 0 Set.univ = 1
⊢ False

Tactic:
simp at h1

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 β
inst✝ : Fintype ι
κ : ι → Kernel α β
⊢ Kernel.sum κ = ∑ i, κ i

Tactic:
ext a s hs
  simp only [sum_apply' κ a hs, finsetSum_apply' _ κ a s, tsum_fintype]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
⊢ ∃ η, ⇑κ =ᵐ[μ] ⇑η ∧ IsMarkovKernel η

Tactic:
classical
  obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using! h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
  obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using! measure_univ_le_add_compl s (μ := μ)
  refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
  · filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
    simp [hb, piecewise]
  · refine ⟨fun b ↦ ?_⟩
    by_cases hb : b ∈ s
    · simpa [hb, piecewise] using! hs _ ha
    · simpa [hb, piecewise] using! hs _ hb

Goal state after: