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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ Nat.card G ∣ ∏ _x, Monoid.exponent G

Tactic:
have hf : Function.Surjective f := by
    rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]
    exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Function.Surjective ⇑f
⊢ Nat.card G ∣ ∏ _x, Monoid.exponent G
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ n • (X i)ᶜ ⊆ Y i

Tactic:
by
          clear hnne0 hgt
          induction n, h1n using Int.leInductionDown with
          | base => rw [zpow_neg, zpow_one]; exact hY i
          | pred n hle hi =>
            calc
              a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ := by rw [zpow_sub, zpow_one]
              _ = a i ^ n • (a i)⁻¹ • (X i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • Y i := smul_set_mono <| hY i
              _ ⊆ a i ^ n • (X i)ᶜ := smul_set_mono (hXYdisj i i).symm.subset_compl_right
              _ ⊆ Y i := hi

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Tactic:
obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : closure ↑S = ⊤
T : Finset ↥H
hT₀ : #T ≤ H.index * #S
hT : closure ↑T = ⊤
⊢ Group.rank ↥H ≤ H.index * Group.rank G
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 ⇑φ
g : G
hg : orderOf g = 2
key : φ g = g
⊢ False

Tactic:
hφ g key,

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 ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf 1 = 2
key : φ g = g
⊢ False
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ normalizer ↑P ≤ centralizer ↑P

Tactic:
rw [Subsingleton.elim (normalizer _) (centralizer P)]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ S.lowerCentralSeries (n + 1) = ⊥

Tactic:
rw [lowerCentralSeries_succ, commutator_def, closure_eq_bot_iff, Set.subset_singleton_iff]
  rintro x ⟨y, hy1, z, _, rfl⟩
  rw [commutatorElement_def, mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]
  exact mem_center_iff.mp (h hy1) z

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
⊢ Surjective ⇑P

Tactic:
exact (MonoidHom.fst ..).subgroupMap_surjective I

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : ↑(P ⟨(g₂, h₂), ⋯⟩) = g
hQ : ↑(Q ⟨(g₂, h₂), ⋯⟩) = h
⊢ (↑(P ⟨(g₂, h₂), ⋯⟩), h) ∈ I

Tactic:
← hQ

Goal state after:
case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : ↑(P ⟨(g₂, h₂), ⋯⟩) = g
hQ : ↑(Q ⟨(g₂, h₂), ⋯⟩) = h
⊢ (↑(P ⟨(g₂, h₂), ⋯⟩), ↑(Q ⟨(g₂, h₂), ⋯⟩)) ∈ I
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
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ IsNilpotent (G₁ × G₂)

Tactic:
by
  rw [nilpotent_iff_lowerCentralSeries]
  refine ⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), ?_⟩
  rw [top_lowerCentralSeries_prod,
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
    lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]

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

Goal state before:
pp: g : Perm (Fin 5)
ha : ((-1) ^ g.cycleType.card) ^ 2 * (-1) ^ g.cycleType.card = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
Int.units_pow_two,

Goal state after:
g : Perm (Fin 5)
ha : 1 * (-1) ^ g.cycleType.card = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
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 ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
⊢ ∃ g, g • x = y

Tactic:
use gy⁻¹ * g * gx

Goal state after:
case h
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 ↪ α
gx : G
x1 : Fin n ↪ ↥(ofStabilizer G a)
hgx : gx • x = snoc x1
gy : G
y1 : Fin n ↪ ↥(ofStabilizer G a)
hgy : gy • y = snoc y1
g : ↥(stabilizer G a)
hg : g • x1 = y1
⊢ (gy⁻¹ * ↑g * gx) • x = y
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1

Tactic:
rw [isMultiplyPreprimitive_iff]

Goal state after:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1 ∧
    ∀ {s : Set α}, s.encard + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
rw [isMultiplyPreprimitive_iff]

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n ∧
    ∀ {s : Set ↥(ofStabilizer M a)},
      s.encard + 1 = ↑n →
        IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr
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
⊢ IsMultiplyPreprimitive M α n.succ

Tactic:
rw [isMultiplyPreprimitive_iff]

Goal state after:
case mpr
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
⊢ IsMultiplyPretransitive M α n.succ ∧
    ∀ {s : Set α}, s.encard + 1 = ↑n.succ → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ IsMultiplyPreprimitive M α n

Tactic:
rw [isMultiplyPreprimitive_iff]

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α}, s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
⊢ IsMultiplyPreprimitive M α n

Tactic:
rw [isMultiplyPreprimitive_iff]

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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α}, s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M 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
ht : 2 < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
· rw [← Set.ncard_pair hab] at ht
    replace ht := Set.sdiff_nonempty_of_ncard_lt_ncard ht
    obtain ⟨c, hct, hc⟩ := ht
    simp only [mem_insert_iff, not_or] at hc
    refine ⟨⟨swap c a * swap a b, by simp [hab, hc.1]⟩, ?_, ?_⟩
    · simp only [mem_stabilizer_set' t.toFinite, Subgroup.mk_smul, Perm.smul_def, coe_mul]
      grind
    · simp only [Subgroup.mk_smul, Perm.smul_def, coe_mul]
      grind

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝⁴ : Group N
inst✝³ : Group E
inst✝² : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝¹ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst✝ : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
⊢ (⇑S''.rightHom ∘ ⇑equiv'.toMulEquiv) ∘ ⇑equiv.toMulEquiv = ⇑S.rightHom

Tactic:
equiv'.rightHom_comm,

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝⁴ : Group N
inst✝³ : Group E
inst✝² : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝¹ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst✝ : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
⊢ ⇑S'.rightHom ∘ ⇑equiv.toMulEquiv = ⇑S.rightHom
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w

Tactic:
unfold unitsSMul

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u)
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯)
      hcan =
    w
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
⊢ unitsSMul φ 1 (↑g • w) = ↑(φ g) • unitsSMul φ 1 w

Tactic:
unfold unitsSMul

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
⊢ (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 neg.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels (-1) w
⊢ t⁻¹ * of ↑(⋯.equiv w.head).1 * t *
      (t⁻¹ * (of ↑(⋯.equiv w.head).2 * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord

Tactic:
(d.compl (-1)).equiv_snd_eq_inv_mul

Goal state after:
case neg.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels (-1) w
⊢ t⁻¹ * of ↑(⋯.equiv w.head).1 * t *
      (t⁻¹ * (of ((↑(⋯.equiv w.head).1)⁻¹ * w.head) * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
⊢ Equiv.swap x (f x) ∈ closure fun x ↦ ∃ x_1 y, x_1 ≠ y ∧ x = Equiv.swap x_1 y

Tactic:
by_cases h : x = f x

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ Equiv.swap x (f x) ∈ closure fun x ↦ ∃ x_1 y, x_1 ≠ y ∧ x = Equiv.swap x_1 y

case neg
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : ¬x = f x
⊢ Equiv.swap x (f x) ∈ closure fun x ↦ ∃ x_1 y, x_1 ≠ y ∧ x = Equiv.swap x_1 y
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τ⟩
⊢ ↑(k ^ 2) = 1

Tactic:
← Subgroup.coe_one,

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τ⟩
⊢ ↑(k ^ 2) = ↑1

α : 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 := ⋯
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := ⋯
hk : k = a.toCentralizer ⟨τ, hτ⟩
⊢ Subgroup (Perm α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = #(↑⟨c, hc⟩).support

Tactic:
exact ⟨c, hc, rfl⟩

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
⊢ Monoid.exponent ↥(kleinFour α) = 2

Tactic:
have : Monoid.exponent (kleinFour α) ∣ 2 := by
    rw [Monoid.exponent_dvd]
    rintro ⟨⟨g, hg⟩, hg'⟩
    simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4] at hg'
    rcases hg' with hg' | hg'
    · convert! one_pow _
      simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'
    · convert! pow_orderOf_eq_one g
      rw [← Equiv.Perm.lcm_cycleType, hg']
      simp

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent ↥(kleinFour α) ∣ 2
⊢ Monoid.exponent ↥(kleinFour α) = 2
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case inr
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
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
⊢ IsCyclic ↥↑P

Tactic:
· have := (P.2.map f').isCyclic_of_isZGroup
    apply isCyclic_of_injective (f'.subgroupMap P)
    rwa [← MonoidHom.ker_eq_bot_iff, P.ker_subgroupMap f', Subgroup.subgroupOf_eq_bot]

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 η
⊢ IsFiniteKernel (Kernel.piecewise hs κ η)

Tactic:
refine ⟨⟨max κ.bound η.bound, max_lt κ.bound_lt_top η.bound_lt_top, fun a => ?_⟩⟩

Goal state after:
α : 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 : α
⊢ ((Kernel.piecewise hs κ η) a) Set.univ ≤ max κ.bound η.bound
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 α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
⊢ η.restrict hs ∘ₖ κ = (η ∘ₖ κ).restrict hs

Tactic:
by
  ext a t ht
  simp_rw [comp_apply' _ _ _ ht, restrict_apply' _ _ _ ht, comp_apply' _ _ _ (ht.inter hs)]

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 α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
b : Bool
⊢ ((boolKernel μ ν) b) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

Tactic:
by cases b <;> simp

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∫⁻ (a : α), (κ a) univ ∂μ = 0

Tactic:
← setLIntegral_univ,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∫⁻ (x : α) in univ, (κ x) univ ∂μ = 0
Module: Mathlib.Probability.Kernel.Composition.CompNotation

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ⇑(Kernel.deterministic id ⋯) ∘ₘ μ = μ

Tactic:
deterministic_comp_eq_map,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ map id μ = μ
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ∫⁻ (a_1 : β), (η (a, a_1)) Set.univ ∂κ a = 0

Tactic:
← setLIntegral_univ,

Goal state after:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ∫⁻ (x : β) in Set.univ, (η (a, x)) Set.univ ∂κ a = 0
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
X' : Type u_5
Y' : Type u_6
Z' : Type u_7
mX' : MeasurableSpace X'
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X' Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = Kernel.id ∥ₖ η' ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')

Tactic:
parallelComp_id_left_comp_parallelComp,

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
X' : Type u_5
Y' : Type u_6
Z' : Type u_7
mX' : MeasurableSpace X'
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X' Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ (η' ∘ₖ Kernel.id) ∘ₖ (κ ∥ₖ κ')