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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ x✝ * y / (y * x✝) ∈ N

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ x✝ * y * (y * x✝)⁻¹ ∈ N
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
intros a ha b hb ab

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a : ℕ
ha : a ∈ Set.Iic (nilpotencyClass G)
b : ℕ
hb : b ∈ Set.Iic (nilpotencyClass G)
ab : a < b
⊢ upperCentralSeries G a < upperCentralSeries G b
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ (⇑f '' B).Subsingleton

Tactic:
apply Set.Subsingleton.image hB

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

Goal state before:
pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ ⇑f '' B = univ

Tactic:
hB

Goal state after:
case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ ⇑f '' univ = univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

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

Tactic:
right
    rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ g₂ • ⇑j ⁻¹' B
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (g₂ • ⇑j ⁻¹' B)

Tactic:
← Group.preimage_smul_setₛₗ

Goal state after:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ ⇑j ⁻¹' (φ g₂ • B)
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (⇑j ⁻¹' (φ g₂ • B))
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ δ * C * ‖G.symm w‖ ^ 2 + ((g' x) w) w = δ * C * ((g x) (G.symm w)) (G.symm w) + ((g' x) w) w

Tactic:
simp [← hg]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ IsBlockSystem G (range fun a ↦ orbit (↥N) a)

Tactic:
constructor
  · apply IsPartition.of_orbits
  · intro b; rintro ⟨a, rfl⟩
    exact .orbit_of_normal a

Goal state after:
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:
by
    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.GroupAction.Primitive

Goal state before:
pp: case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
⊢ IsBlock G B → IsTrivialBlock B

Tactic:
hB

Goal state after:
case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inr.«2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h✝ : Nontrivial α
hα : 2 ≤ 3
this : 1 < 2
⊢ Nat.factorial 2 / 2 ∣ 3

Tactic:
simp [Nat.factorial_succ]

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

Goal state before:
pp: case inr.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h✝ : Nontrivial α
hα : 3 ≤ 3
this : 1 < 3
⊢ Nat.factorial 3 / 2 ∣ 3

Tactic:
simp [Nat.factorial_succ]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
⊢ IsBlock G B → IsTrivialBlock B

Tactic:
hB

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

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

Tactic:
· intro h
    rw [isMultiplyPreprimitive_iff]
    constructor
    · exact is_one_pretransitive_iff.mpr h.toIsPretransitive
    · simpa using isPreprimitive_of_fixingSubgroup_empty_iff.mpr h

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ (fixingSubgroup G s).index = (Nat.card α).choose s.ncard * s.ncard !

Tactic:
apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)
  rw [hMk.index_of_fixingSubgroup_mul rfl, Nat.choose_mul_factorial_mul_factorial]
  rw [← ncard_univ]
  exact ncard_le_ncard (subset_univ s)

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 : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
constructor
  · apply isMultiplyPreprimitive_ofStabilizer
  · intro H
    rw [isMultiplyPreprimitive_iff]
    constructor
    · exact ofStabilizer.isMultiplyPretransitive.mpr H.isMultiplyPretransitive
    · intro s hs
      have : ∃ b : α, b ∈ s := by
        rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
        intro h
        apply not_lt.mpr hn
        rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
        simp only [← hs, zero_lt_one]
      obtain ⟨b, hb⟩ := this
      obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a
      rw [isPreprimitive_ofFixingSubgroup_conj_iff (g := g)]
      set s' := g • s with hs'
      let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s'
      have hst : s' = insert a (Subtype.val '' t) := by
        ext x
        constructor
        · intro hxs
          by_cases hxa : x = a
          · simp [hxa]
          · exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
        · rw [Set.mem_insert_iff]
          rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
          · simpa [s', ← hg]
          · simpa only using! hy
      rw [hst, isPreprimitive_fixingSubgroup_insert_iff]
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
      apply ENat.add_left_injective_of_ne_top ENat.one_ne_top
      simp only
      rw [← Nat.cast_one, ← Nat.cast_add, ← hs]
      apply congr_arg₂ _ _ rfl
      rw [show s = g⁻¹ • s' by simp [hs'],
        ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.natCast_one]
      exact notMem_val_image M t

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

Goal state before:
pp: case succ.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn' : m < n + 1
⊢ n ≤ n + 1

Tactic:
exact Nat.le_succ n

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

Goal state before:
pp: α : Type u_2
s : Set α
g : Perm ↑s
⊢ ∃ a, toPerm a = g

Tactic:
by
  classical
  use! Perm.ofSubtype g
  · apply ofSubtype_mem_stabilizer
  · aesop

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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
⊢ IsBlock (↥G) B → IsTrivialBlock B

Tactic:
hB

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
⊢ IsBlock (↥G) B → IsTrivialBlock B

Tactic:
hB

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'✝ : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : sᶜ.ncard * 2 ≤ Nat.card α
⊢ False

Tactic:
· rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]

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

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
⊢ sᶜ ⊆ B

Tactic:
have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le h0
      (hBsc.ssubset_of_ne (by aesop)) -- uses Step 1
      hG.le hB

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
⊢ sᶜ ⊆ B
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
⊢ ((toPermHom K α) g) a = (toPerm 1) a

Tactic:
exact congrFun (congrArg DFunLike.coe this) a

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

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * f ↑(∏ i, (x (n i)).2) = f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)

Tactic:
← univ.mul_prod_erase _ (mem_univ i),

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ n i * f ↑((x (n i)).2 * ∏ x_1 ∈ univ.erase i, (x (n x_1)).2) =
    f ((fun i ↦ (x (n i)).1 * ↑(∏ j ∈ univ.erase i, (x (n j)).2)) i)
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsSimpleGroup G
hN : H.IsSubnormal
⊢ H.Normal

Tactic:
induction hN with
  | top => simp
  | step H K h_le hSubn hN Knorm =>
    obtain rfl | rfl := Knorm.eq_bot_or_eq_top
    · grind
    · 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
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
⊢ ∀ (b : NormalWord d), 1 • b = b

Tactic:
by simp +instances [instHSMul]

Goal state after:
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
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S

Tactic:
clear supp_eq

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
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
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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head? = Option.map Prod.fst (some (-a.1, x))
⊢ False

Tactic:
Option.map_some

Goal state after:
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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head? = some (-a.1, x).1
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : _root_.Disjoint (↑c).support (↑d).support
H' : _root_.Disjoint (↑(↑τ c)).support (↑(↑τ d)).support
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
Finset.disjoint_right

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : ∀ ⦃a : α⦄, a ∈ (↑d).support → a ∉ (↑c).support
H' : ∀ ⦃a : α⦄, a ∈ (↑(↑τ d)).support → a ∉ (↑(↑τ c)).support
⊢ a (↑τ d) ∈ (↑(↑τ c)).support ↔ x ∈ (↑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)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
| (g ^ j) x

Tactic:
rw [← hx, ← mul_apply, ← zpow_add_one]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
| (g ^ (j + 1)) x
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, g ∉ H

Tactic:
by
  simp_rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup, ← not_forall, not_imp_not]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m} = ∅

Tactic:
Finset.eq_empty_iff_forall_notMem

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ ∀ (x : Perm α), x ∉ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m}
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ (f.comp ((of i).comp (φ i))) x✝ = (g.comp ((of i).comp (φ i))) x✝

Tactic:
← MonoidHom.comp_assoc,

Goal state after:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ ((f.comp (of i)).comp (φ i)) x✝ = (g.comp ((of i).comp (φ i))) x✝
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
⊢ ∀ (b : NormalWord d), 1 • b = b

Tactic:
by simp +instances [instHSMul]

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

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

Tactic:
rw [Fintype.card_coeSort_range (kerParam_injective g)]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card (Perm ↑(Function.fixedPoints ⇑g) × ((c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c))) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case neg
ι : 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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
push Not at hep

Goal state after:
case neg
ι : 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)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
rw [card_of_cycleType_mul_eq, if_pos hm]

Goal state after: