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

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)

Tactic:
apply H _ (hB.translate g)

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ a ∈ g • B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: n : ℕ
⊢ finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))

Tactic:
by
  simp [mem_alternatingGroup]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
⊢ IsPretransitive (↥N) α

Tactic:
Set.ne_univ_iff_exists_notMem

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
hNX : ∃ a, a ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ).IsThreeCycle
hτ : (↑τ).IsThreeCycle
h5 : 5 ≤ card α
⊢ (↑σ).support.card + 2 ≤ card α

Tactic:
rwa [hσ.card_support]

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

Goal state before:
pp: case bc
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
⊢ ?a + g'.support.card ≤ ?a + 2

pp: case a
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
⊢ ℕ

Tactic:
rw [← hd.card_support_mul, h3]

Goal state after:
case bc
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
⊢ (c * g').support.card ≤ 3 + 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ map Perm.ofSubtype (alternatingGroup ↥s) = Perm.ofSubtype.range ⊓ alternatingGroup α

Tactic:
by
  ext k
  rw [Subgroup.mem_map, Subgroup.mem_inf, MonoidHom.mem_range]
  grind [sign_ofSubtype, mem_alternatingGroup]

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

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this✝ : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := ⋯
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := ⋯
hy : y' = append y
g : G
hg : g • x' = y'
this : g ∈ fixingSubgroup G s
i : Fin m
⊢ ↑((⟨g, this⟩ • x) i) = ↑(y i)

Tactic:
rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this✝ : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
this : g ∈ fixingSubgroup G s
i : Fin m
⊢ 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 α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • ↑((Classical.choice Hs) i) = ↑((Classical.choice Hs) i)

Tactic:
nth_rewrite 1 [← ofFixingSubgroup.append_left x i]

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • (append x) (castAdd m i) = ↑((Classical.choice Hs) i)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ : Set α
hs : s✝.encard + 1 = ↑0
⊢ IsPreprimitive ↥(fixingSubgroup M s✝) ↥(ofFixingSubgroup M s✝)

Tactic:
by simp at hs

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

Goal state before:
pp: case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
H1 : IsMultiplyPreprimitive M α 1
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(ofFixingSubgroup M ∅)

Tactic:
apply H1.isPreprimitive_ofFixingSubgroup (by simp)

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = ↑n
⊢ ↑n + 1 = ↑n.succ

pp: 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
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = ↑n
⊢ a ∉ Subtype.val '' s

Tactic:
Nat.cast_succ

Goal state after:
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
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = ↑n
⊢ ↑n + 1 = ↑n + 1

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
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = ↑n
⊢ a ∉ Subtype.val '' s
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case inr
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 ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩

Tactic:
have hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr ha.2

Goal state after:
case inr
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 ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

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

Tactic:
simp [hab, hc.1]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
n : ℕ
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α (n + 2)

Tactic:
by
  have hα : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by
    simp [Nat.card_eq_zero_of_infinite] at hsn')
  induction n generalizing α hα G with
  -- case n = 0
  | zero => simpa using is_two_preprimitive hG hsn hsn' hprim
  -- Induction step
  | succ n hrec =>
    suffices ∃ (a : α) (t : Set (SubMulAction.ofStabilizer G a)),
      a ∈ s ∧ s = insert a (Subtype.val '' t) by
      obtain ⟨a, t, _, hst⟩ := this
      have ha' : a ∉ Subtype.val '' t := by
        intro h; rw [Set.mem_image] at h; obtain ⟨x, hx⟩ := h
        apply x.prop; rw [hx.right]; exact Set.mem_singleton a
      have ht_prim : IsPreprimitive (stabilizer G a) (SubMulAction.ofStabilizer G a) := by
        rw [← is_one_preprimitive_iff]
        rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
        · apply is_two_preprimitive hG hsn hsn' hprim
        · norm_num
      have : IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
          (ofFixingSubgroup G (insert a (Subtype.val '' t))) :=
        IsPreprimitive.of_surjective
          (ofFixingSubgroup_of_eq_bijective (hst := hst)).surjective
      have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
        (ofFixingSubgroup (stabilizer G a) t) :=
        IsPreprimitive.of_surjective
          ofFixingSubgroup_insert_map_bijective.surjective
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
      refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
      · -- t.card = Nat.succ n
        rw [← Set.ncard_image_of_injective t Subtype.val_injective]
        apply Nat.add_right_cancel
        rw [← Set.ncard_insert_of_notMem ha', ← hst, hsn]
      · -- n + 2 < Nat.card (SubMulAction.ofStabilizer G α a)
        rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]
        exact hsn'
    -- ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
    suffices s.Nonempty by
      obtain ⟨a, ha⟩ := this
      use a, Subtype.val ⁻¹' s, ha
      ext x
      by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]
    rw [← Set.ncard_pos, hsn]; apply Nat.succ_pos

Goal state after:
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
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
this : φ g = φ 1
| a

Tactic:
rw [← one_smul K a]

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
H : Subsingleton ↥φ.range
a : α
a✝ : a ∈ _root_.Set.univ
g : K
this : φ g = φ 1
| 1 • a
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≤ 2
this : Nonempty ↥G
⊢ 2 ≤ Fintype.card ↥G

Tactic:
apply Nat.le_of_dvd Fintype.card_pos

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≤ 2
this : Nonempty ↥G
⊢ 2 ∣ Fintype.card ↥G
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
rw [stabilizer_coe]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer (Perm α) ↑s)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hsn.a
α : 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
⊢ Nat.card α = g.support.card + (n + 1)

Tactic:
h3g.card_support,

Goal state after:
case inr.hsn.a
α : 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
⊢ Nat.card α = 3 + (n + 1)
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
⊢ (lift f x hx) t = x

Tactic:
delta HNNExtension; simp [lift, t]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
Knorm : ⊤.Normal
⊢ H.Normal

Tactic:
grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w w' : NormalWord d
h1 : w.head = w'.head
h2 : w.toList = w'.toList
⊢ w = w'

Tactic:
by
  rcases w with ⟨⟨⟩, _⟩; cases w'; simp_all

Goal state after:
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
u : ℤˣ
w : NormalWord d
⊢ (g : G) → Cancels u (ofGroup g) → NormalWord d

Tactic:
by simp [Cancels, ofGroup]; tauto

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

Goal state before:
pp: case mul.inr
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hai : Irreducible (f a) ∧ IsUnit (f i)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
· obtain ⟨u, m', hu, hm', rfl⟩ := ha hai.1
      exact ⟨u * i, m', by simpa using hu.mul hai.2, hm', by ac_rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
hf : ∀ (a : M), f a = 1 → a = 1
hg : ∀ (a : N), g a = 1 → a = 1
hp : f.range ⊓ g.range ≤ ⊥
a : M
b : N
h : f a * g b = 1
⊢ f a⁻¹ = g b

Tactic:
rwa [map_inv, inv_eq_iff_mul_eq_one]

Goal state after:
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
w : NormalWord d
⊢ unitsSMul φ 1 (unitsSMul φ (-1) w) = w

Tactic:
convert! unitsSMul_neg _ _ w

Goal state after:
case e'_7
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
w : NormalWord d
⊢ 1 = - -1
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i })!

Tactic:
by
  set φ : α → Finset.univ.image f :=
    Set.codRestrict f (Finset.univ.image f) (fun a => by simp)
  suffices ∀ g : Perm α, f ∘ g = f ↔ φ ∘ g = φ by
    simp only [this, stabilizer_card]
    apply Finset.prod_bij (fun g _ => g.val)
    · exact fun g _ => Finset.coe_mem g
    · exact fun g _ g' _ => SetCoe.ext
    · simp
    · intro i _
      apply congr_arg
      apply Fintype.card_congr
      apply Equiv.subtypeEquiv (Equiv.refl α)
      intro a
      rw [refl_apply, ← Subtype.coe_inj]
      simp only [φ, Set.val_codRestrict_apply]
  · intro g
    simp only [funext_iff]
    apply forall_congr'
    intro a
    simp only [Function.comp_apply, φ, ← Subtype.coe_inj, Set.val_codRestrict_apply]

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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
· simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
      ← mem_support]
    rintro ⟨c, -, hc⟩
    rw [Function.mem_fixedPoints_iff] at hx
    exact mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∈ (fixedBy α (Equiv.swap (f a) a * f))ᶜ
⊢ b ∈ s

Tactic:
contrapose hb
    simp_rw [notMem_compl_iff, mem_fixedBy, Perm.smul_def, Perm.mul_apply, swap_apply_def,
      apply_eq_iff_eq]
    by_cases hb' : f b = b
    · rw [hb']; split_ifs with h <;> simp only [h]
    simp [show b = a by simpa [hb] using supp_subset hb']

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
⊢ ↥↑P ≃* IteratedWreathProduct G n

Tactic:
let e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans
    (Finite.equivFinOfCardEq (by rw [Nat.card_fun, Nat.card_fin, hG])).symm

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
⊢ ↥↑P ≃* IteratedWreathProduct G n
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx hx' : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, Ne, ← Function.mem_fixedPoints_iff] at hx'

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x
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
motive : (con φ).Quotient → Prop
x : (con φ).Quotient
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
⊢ motive x

Tactic:
induction x using Con.induction_on with

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (⨆ i, zpowers ↑i)

Tactic:
← ofSubtype.range.closure_eq

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint (closure ↑ofSubtype.range) (⨆ i, zpowers ↑i)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
hU : U.Pairwise fun i j ↦ (↑(v i)).Disjoint ↑(v j)
⊢ (ofSubtype k).cycleType + ∑ i ∈ g.cycleFactorsFinset.attach, (↑(v i)).cycleType =
    k.cycleType + ∑ c ∈ g.cycleFactorsFinset.attach, (↑(v c)).cycleType

Tactic:
exact congr_arg₂ _ cycleType_ofSubtype rfl

Goal state after:
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
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (of i) g • w = g • w

Tactic:
by
  rw [summand_smul_def, summand_smul_def']

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

Goal state before:
pp: case inl
⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4

Tactic:
simp only [lcm_zero_left, mul_zero]
    exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
⊢ IsCyclic ↥↑P

Tactic:
specialize hG' p hp Q

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hG' : IsCyclic ↥↑Q
hQ : Subgroup.comap f ↑Q = ↑P
⊢ IsCyclic ↥↑P
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (discard α)

Tactic:
by rw [discard]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : ¬Measurable f
⊢ κ.map f = 0

Tactic:
simp [map, hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ κ.mapOfMeasurable f hf = κ.map f

Tactic:
simp [map, hf]

Goal state after: