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

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

Tactic:
rw [← Set.image_preimage_eq B hf]
    apply IsTrivialBlock.image hf
    exact isTrivialBlock_of_isBlock (IsBlock.preimage f hB)

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

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ n ∣ 2

Tactic:
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]

Goal state after:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ g'.support.card ≤ 2
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : g • aux x = aux y
i : n
⊢ (σ g • x) i = y i

Tactic:
DFunLike.ext_iff

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : ∀ (x_1 : n), (g • aux x) x_1 = (aux y) x_1
i : n
⊢ (σ g • x) i = y i
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

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

Tactic:
DFunLike.ext_iff

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : ∀ (x_1 : Fin n.succ), (g • snoc x) x_1 = (snoc y) x_1
⊢ g ∈ stabilizer G a
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
β : Type u_3
x y : ι ↪ β
⊢ ∃ σ, σ • x = y

Tactic:
obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair x y x.injective y.injective

Goal state after:
ι : Type u_2
inst✝ : Finite ι
β : Type u_3
x y : ι ↪ β
σ : Perm β
hσ : ∀ (a : ι), σ (x a) = y a
⊢ ∃ σ, σ • x = y
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 α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
have ha' : a ∈ (s ∩ g • s)ᶜ := by
    rw [Set.compl_inter]
    exact Set.mem_union_left _ ha.1

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
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
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
⊢ φ m • ↑⟨y, hy⟩ = ↑⟨y, hy⟩

Tactic:
← hs',

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : y ∈ ⇑f '' s
⊢ φ m • ↑⟨y, hy✝⟩ = ↑⟨y, hy✝⟩
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

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

Tactic:
← hs',

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

Tactic:
simpa only [Set.mem_image, t, eq_comm] using! hy

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ∃ g, g ∉ stabilizer (↥(alternatingGroup α)) s

Tactic:
use ⟨Equiv.swap a b * Equiv.swap a c, by aesop⟩

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ⟨swap a b * swap a c, ⋯⟩ ∉ stabilizer (↥(alternatingGroup α)) s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
refine ⟨⟨swap c a * swap a b, by simp [hab, hc.1]⟩, ?_, ?_⟩

Goal state after:
case pos.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ ⟨swap c a * swap a b, ⋯⟩ ∈ stabilizer (↥(alternatingGroup α)) t

case pos.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ ⟨swap c a * swap a b, ⋯⟩ • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ ⟨k, hk⟩ • b ∈ B

Tactic:
suffices k • B = B from this.le (smul_mem_smul_set hb)

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ k • B = B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial]
    grind

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
s : Set α
h : s.Nonempty
h1 : s.Subsingleton
this : Nontrivial α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝¹ : Finite α
this✝ : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsPretransitive (Perm α) (Fin 2 ↪ α)

Tactic:
← hα

Goal state after:
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝¹ : Finite α
this✝ : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsPretransitive (Perm α) (Fin (Nat.card α) ↪ α)
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) α (n + 2)

Tactic:
apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))

Goal state after:
case inr.hsn
α : 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
⊢ (↑g.support)ᶜ.ncard = n + 1

case inr.hsn'
α : 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
⊢ n + 2 < Nat.card α

case inr.hprim
α : 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
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
have : IsPretransitive (alternatingGroup α) (powersetCard α n) :=
    isPretransitive_alternatingGroup (le_trans h_three_le hn.le)

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
⊢ IsPreprimitive ↥(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
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
g : G
⊢ (lift f x hx) (of g) = f g

Tactic:
simp [lift, of]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ Monotone fun x ↦
    match x with
    | 0 => H
    | n.succ => f n

pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal

Tactic:
· refine monotone_nat_of_le_succ ?_
        grind only [monotone_iff_forall_lt]

Goal state after:
case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by
    simp [Cancels, Subgroup.mul_mem_cancel_left]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ List.map Prod.fst ((t ^ ↑a.1 * of a.2) • w').toList =
      List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      ((t ^ ↑a.1 * of a.2) • w').head ∈ toSubgroup A B (-u)

Tactic:
· have : ¬ Cancels a.1 (a.2 • w') := by
        simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some_iff,
          Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
        intro hS x hx
        have hx' := congr_arg (Option.map Prod.fst) hx
        rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
        have : w'.head ∈ toSubgroup A B a.fst := by
          simpa using hw'3 _ hx'
        rw [mul_mem_cancel_right this] at hS
        have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
            (List.head?_eq_some_head _) hS
          rwa [List.head?_eq_some_head hl, Option.map_some, ← this, Option.some_inj] at hx'
        simp at this
      simp [mul_smul, of_smul_eq_smul, t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2]

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
this : (-1) ^ #c.support ≠ 1
⊢ ¬Even #c.support

Tactic:
exact fun h ↦ this h.neg_one_pow

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

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

Tactic:
rintro - ⟨a, rfl⟩
      refine ⟨⟨ofSubtype a, ?_⟩, ?_, rfl⟩
      · rw [mem_centralizer_singleton_iff]
        exact Disjoint.commute (disjoint_iff_disjoint_support.mpr (ofSubtype_support_disjoint a))
      · exact Perm.ext fun x ↦ Subtype.ext (disjoint_iff_disjoint_support.mpr
          ((ofSubtype_support_disjoint a).mono_right
            (mem_cycleFactorsFinset_support_le x.2))).commute.mul_inv_cancel

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

Goal state before:
pp: case a
α : 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 ⋯), ⋯⟩
⊢ ↑p ∈ (kerParam g).range

Tactic:
use (u, v)

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := ⋯
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) := ⋯
⊢ (kerParam g) (u, v) = ↑p
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

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

Tactic:
rw [Sylow.ext_iff]
    simp [two_sylow_eq_kleinFour_of_card_eq_four hα4]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : IsCyclic ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
h : H ≠ ⊥
f : ↥⁅commutator ↥H, commutator ↥H⁆ ≃* ↥(Subgroup.map H.subtype ⁅commutator ↥H, commutator ↥H⁆) :=
  ⁅commutator ↥H, commutator ↥H⁆.equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆

Tactic:
rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : IsCyclic ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
h : H ≠ ⊥
f : ↥⁅commutator ↥H, commutator ↥H⁆ ≃* ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
⊢ IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.InformationTheory.Coding.UniquelyDecodable

Goal state before:
pp: α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L // ∀ (x : List α), x ∈ L → x ∈ S }
hflat : (fun L ↦ (↑L).flatten) L₁ = (fun L ↦ (↑L).flatten) L₂
⊢ L₁ = L₂

Tactic:
apply Subtype.ext

Goal state after:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L // ∀ (x : List α), x ∈ L → x ∈ S }
hflat : (fun L ↦ (↑L).flatten) L₁ = (fun L ↦ (↑L).flatten) L₂
⊢ ↑L₁ = ↑L₂
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)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
i✝ : ℕ
a✝ : (i : ι) × G i
⊢ w.toList[i✝]? = some a✝ ↔ Word.empty.toList[i✝]? = some a✝

Tactic:
simp [hw'map]

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

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

Tactic:
exact Subgroup.index_dvd_of_le hP

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ {i | x i ≠ x i} = ∅

Tactic:
filter_eq_empty_iff

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε > 0, ∀ {a b : Hamming β}, dist a b < ε → (a, b) ∈ s

Tactic:
push_cast
    constructor
    · refine fun hs ↦ ⟨1, zero_lt_one, fun hab ↦ hs <| by simpa using hab⟩
    · rintro ⟨_, hε, hs⟩ ⟨_, _⟩ rfl
      refine hs (lt_of_eq_of_lt ?_ hε)
      exact mod_cast hammingDist_self _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ Kernel.id ∘ₖ κ = κ

Tactic:
ext a s hs
  simpa [comp_apply' _ _ _ hs, id_apply, Measure.dirac_apply' _ hs]
    using lintegral_indicator_one hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = 0

Tactic:
Kernel.compProd_of_not_isSFiniteKernel_left,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ 0 () = 0

case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ ¬IsSFiniteKernel (Kernel.const Unit μ)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((κ ∥ₖ Kernel.sum η) x) s✝ = ((Kernel.sum fun i ↦ κ ∥ₖ η i) x) s✝

Tactic:
simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
⊢ κ ⊗ₖ 0 = 0

Tactic:
by
  by_cases h : IsSFiniteKernel κ
  · ext a s hs
    rw [Kernel.compProd_apply hs]
    simp
  · rw [Kernel.compProd_of_not_isSFiniteKernel_left _ _ h]

Goal state after: