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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ ∑ i, (Set.range ⇑f ∩ ↑i).ncard ≤ (orbit H B).ncard

Tactic:
apply le_trans (Finset.sum_le_card_nsmul _ _ 1 _)

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ Finset.univ.card • 1 ≤ (orbit H B).ncard

G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ ∀ x ∈ Finset.univ, (Set.range ⇑f ∩ ↑x).ncard ≤ 1
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 α
t : Set ↥(ofFixingSubgroup M s)
⊢ Disjoint s (Subtype.val '' t)

Tactic:
Set.disjoint_iff

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
t : Set ↥(ofFixingSubgroup M s)
⊢ 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 α
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'
⊢ s' = insert a (Subtype.val '' t)

Tactic:
ext x

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'
x : α
⊢ x ∈ s' ↔ x ∈ insert a (Subtype.val '' t)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case h
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)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ s
k : M
hk : k ∈ fixingSubgroup M s
hkax : ⟨k, hk⟩ • ⟨a, ⋯⟩ = ⟨x, hx⟩
⊢ ⟨k, ⋯⟩ • ⟨a, ha'⟩ = ⟨x, hx✝⟩

Tactic:
rwa [Subtype.ext_iff] at hkax ⊢

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h✝ : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
i : Fin (Nat.card α - 2)
h : x i ∈ Finset.image (⇑x) Finset.univ
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i

Tactic:
rw [← Finset.notMem_compl, hs, Finset.mem_insert, Finset.mem_singleton, not_or] at h

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h✝ : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
i : Fin (Nat.card α - 2)
h : ¬x i = a ∧ ¬x i = b
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right.hf.right
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
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
y : α
hx : ∀ x ∈ s, ¬f x = f y
⊢ y ∉ s

Tactic:
exact fun hy ↦ hx y hy rfl

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
⊢ toPerm ⟨⟨Perm.ofSubtype g * k, ⋯⟩, ⋯⟩ = g

Tactic:
ext x

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ ↑((toPerm ⟨⟨Perm.ofSubtype g * k, ⋯⟩, ⋯⟩) x) = ↑(g x)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ ↑x ∉ k.support

Tactic:
exact hk_support x.prop

Goal state after:
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
⊢ s = insert a (Subtype.val '' Subtype.val ⁻¹' s)

Tactic:
ext x

Goal state after:
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)
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
this : Nontrivial α
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
obtain ⟨a, ha⟩ := h

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

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
a : α
ha : g • a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : (toPerm g) s = 1 s
⊢ g • a ∈ s

Tactic:
simp only [toPerm_apply, coe_one, id_eq] at has'

Goal state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
a : α
ha : g • a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g • s = s
⊢ g • a ∈ s
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.GroupAction.Jordan

Goal state before:
pp: α : 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
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ {x | x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ} = g.support

Tactic:
ext x

Goal state after:
α : 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
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
x : α
⊢ x ∈ {x | x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ} ↔ x ∈ g.support
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
⊢ H.IsSubnormal

Tactic:
have key := Hsn.trans' Ksn
  rwa [map_subgroupOf_eq_of_le HK] at key

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: case f.f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝¹ : α
b✝¹ : ↥s
a✝ : α
b✝ : ↥s
⊢ ↑b✝ * a✝¹ ≤ ↑b✝¹ * a✝ → ↑b✝¹ * a✝ ≤ ↑b✝ * a✝¹ → mk a✝¹ b✝¹ = mk a✝ b✝

Tactic:
mk_eq_mk_iff,

Goal state after:
case f.f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝¹ : α
b✝¹ : ↥s
a✝ : α
b✝ : ↥s
⊢ ↑b✝ * a✝¹ ≤ ↑b✝¹ * a✝ → ↑b✝¹ * a✝ ≤ ↑b✝ * a✝¹ → (r s) (a✝¹, b✝¹) (a✝, b✝)
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : x ∈ Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))
⊢ Prime x

Tactic:
rw [Multiset.mem_filter, Multiset.mem_map] at hx
      obtain ⟨p, hp, rfl⟩ := hx.1
      exact f.map_prime (prime_of_factor _ hp)
        (mt (fun h ↦ eq_zero_of_zero_dvd <| h ▸ map_dvd f (dvd_of_mem_factors hp)) hn) hx.2

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
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
hcan : ¬Cancels 1 w
⊢ (let g' := unitsSMulGroup φ d 1 (↑g • w).head;
    cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      let g' := unitsSMulGroup φ d 1 w.head;
      cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
simp +instances only [toSubgroup_neg_one, unitsSMulGroup, toSubgroup_one, toSubgroupEquiv_one,
      SetLike.coe_sort_coe, group_smul_head, mul_inv_rev, ← mul_smul, mul_assoc, inv_mul_cancel,
      mul_one, smul_cons]

Goal state after:
case neg
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
hcan : ¬Cancels 1 w
⊢ cons (↑(φ (⋯.equiv (↑g * w.head)).1)) 1 ((↑(⋯.equiv (↑g * w.head)).2 * w.head⁻¹) • w) ⋯ ⋯ =
    cons (↑(φ g) * ↑(φ (⋯.equiv w.head).1)) 1 ((↑(⋯.equiv w.head).2 * w.head⁻¹) • w) ⋯ ⋯
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
⊢ ¬closure S ≤ stabilizer G T

Tactic:
have ⟨b, hb⟩ := nonempty

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
b : α
hb : b ∈ T
⊢ ¬closure S ≤ stabilizer G T
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
y z : α
h : z ∈ {z, y}ᶜ
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
x z : α
h : z ∈ {x, z}ᶜ
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a✝ b✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(a✝ ⟨a, b⟩)).support = #a.support
hτ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(b✝ ⟨a, b⟩)).support = #a.support
⊢ ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(a✝ (b✝ ⟨a, b⟩))).support = #a.support

Tactic:
intro c hc

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a✝ b✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(a✝ ⟨a, b⟩)).support = #a.support
hτ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(b✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ #(↑(a✝ (b✝ ⟨c, hc⟩))).support = #c.support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝ ⟨a, b⟩)).support = #a.support
⊢ ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝⁻¹ ⟨a, b⟩)).support = #a.support

Tactic:
intro c hc

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ #(↑(x✝⁻¹ ⟨c, hc⟩)).support = #c.support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (a.ofPermHom τ).support = (↑τ).support.biUnion fun c ↦ (↑c).support

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ x ∈ (a.ofPermHom τ).support ↔ x ∈ (↑τ).support.biUnion fun c ↦ (↑c).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ a.ofPermHom τ * g = g * a.ofPermHom τ

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ (a.ofPermHom τ * g) x = (g * a.ofPermHom τ) x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
⊢ ↑(a.toCentralizer τ) * ↑c = ↑(↑τ c) * ↑(a.toCentralizer τ)

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
⊢ (↑(a.toCentralizer τ) * ↑c) x = (↑(↑τ c) * ↑(a.toCentralizer τ)) x
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β x✝ y✝ z✝ : H.LeftTransversal
h : diff (MonoidHom.id ↥H) x✝ y✝ = 1
h' : diff (MonoidHom.id ↥H) y✝ z✝ = 1
⊢ diff (MonoidHom.id ↥H) x✝ z✝ = 1

Tactic:
by rw [← diff_mul_diff, h, h', one_mul]

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H := { toFun := fun h ↦ ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
x : G ⧸ H
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ =
    ϕ
      ((MonoidHom.id ↥H)
        ⟨(↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)))⁻¹ * ↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)),
          ⋯⟩)

Tactic:
simp only [ϕ, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc,
    MonoidHom.id_apply, toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
⊢ (of i).comp (φ i) = base φ

Tactic:
ext x

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ((of i).comp (φ i)) x = (base φ) x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: 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

Tactic:
ext x

Goal state after:
case h
α : 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 : α
⊢ ((kerParam g) (u, v)) x = ↑p x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
⊢ (kerParam g).range = Subgroup.centralizer {g}

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
⊢ x ∈ (kerParam g).range ↔ x ∈ Subgroup.centralizer {g}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ σ ∈ kleinFour ↥s ∧ True ↔ ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}

Tactic:
and_true,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ σ ∈ kleinFour ↥s ↔ ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic ↥↑P
⊢ commutator G < ⊤

Tactic:
let f := MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic ↥↑P
f : G →* ↥↑P := MonoidHom.transferSylow P ⋯
⊢ commutator G < ⊤
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a

Tactic:
by rw [h]

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

Goal state before:

Tactic:
_ = ∫⁻ b, (s ∩ t).indicator 1 b ∂κ a := by
    congr with b
    simp [Set.inter_indicator_one]
  _ = κ a (s ∩ t) := lintegral_indicator_one <| hs.inter ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (η ∘ₖ κ)

Tactic:
by
  refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩
  calc (η ∘ₖ κ) a Set.univ
  _ ≤ κ a Set.univ * η.bound := comp_apply_univ_le κ η a
  _ ≤ κ.bound * η.bound := by gcongr; exact measure_le_bound κ a Set.univ

Goal state after:
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 α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η

Tactic:
ext x

Goal state after:
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 α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum κ ∥ₖ η) x) s✝ = ((Kernel.sum fun i ↦ κ i ∥ₖ η) x) s✝
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 κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

Tactic:
ext x

Goal state after:
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✝