mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (Subtype.val '' s).encard + 1 + 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:
Subtype.coe_injective.encard_image,

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
⊢ s.encard + 1 + 1 = ↑n.succ

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.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a})
⊢ IsMultiplyPreprimitive G α 2

Tactic:
isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G {a}) ↥(ofFixingSubgroup G {a})
⊢ IsMultiplyPreprimitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
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'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 = (Subtype.val '' t).encard + 1

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'
hst : s' = insert a (Subtype.val '' t)
⊢ a ∉ Subtype.val '' t

Tactic:
Subtype.coe_injective.encard_image,

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'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 = t.encard + 1

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'
hst : s' = insert a (Subtype.val '' t)
⊢ a ∉ 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 α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + t'.encard + 1 = ↑n

Tactic:
Subtype.coe_injective.encard_image,

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + t.encard + 1 = ↑n
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
k : G
⊢ k ∈ fixingSubgroup G s → k ∈ stabilizer G s

Tactic:
hk

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ s
⊢ ∃ g, g • a = x

pp: case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x

Tactic:
· exact hs a ha x hx

Goal state after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ k • b = x

Tactic:
hk

Goal state after:
case h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ x = x
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right.hφ
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' := ⋯ }
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
hy : y ∈ s
⊢ φ k • f y = f y

Tactic:
hk

Goal state after:
case right.hφ
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' := ⋯ }
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
hy : y ∈ s
⊢ f y = f y

case right.hφ.a
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' := ⋯ }
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
hy : y ∈ s
⊢ f y ∈ ⇑f '' s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t

Tactic:
intro t

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
⊢ 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
this : s = g • s
⊢ b ∈ s

Tactic:
rw [this]
        simpa only [Set.smul_set_compl, Set.mem_compl_iff, Set.not_notMem] using hgb

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : g ∈ stabilizer (Perm α) s
hg3 : g.IsThreeCycle
φ : ↥G →* ↥(Subgroup.map (alternatingGroup α).subtype G) := (alternatingGroup α).subtype.subgroupMap G
⊢ IsPreprimitive (↥(Subgroup.map (alternatingGroup α).subtype G)) α

Tactic:
let f : α →ₑ[φ] α := {
      toFun := id
      map_smul' _ _ := rfl }

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
g : Perm α
hg : g ∈ stabilizer (Perm α) s
hg3 : g.IsThreeCycle
φ : ↥G →* ↥(Subgroup.map (alternatingGroup α).subtype G) := (alternatingGroup α).subtype.subgroupMap G
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive (↥(Subgroup.map (alternatingGroup α).subtype G)) α
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) α
⊢ IsPreprimitive (↥G) α

Tactic:
apply IsPreprimitive.mk

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 α}, 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) α
⊢ IsPreprimitive (↥G) α

Tactic:
apply IsPreprimitive.mk

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 α}, 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 α
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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)

Tactic:
have := isMultiplyPretransitive α

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
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
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
n : N
⊢ (S.rightHom.comp S.inl) n = 1 n

Tactic:
rw [MonoidHom.one_apply, MonoidHom.comp_apply]

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
n : N
⊢ S.rightHom (S.inl n) = 1
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
⊢ FaithfulSMul G ↑(powersetCard α n)

Tactic:
by
  rw [faithfulSMul_iff]
  intro g hg
  apply toPerm_injective (α := G) (β := α)
  rw [toPerm_one, ← mulAction_faithful hn hα]
  exact Perm.ext_iff.mpr hg

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
⊢ comap (QuotientGroup.mk' (center G)) (Subgroup.upperCentralSeries (G ⧸ center G) 1) =
    (QuotientGroup.mk' (center G)).ker

Tactic:
QuotientGroup.ker_mk',

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
⊢ comap (QuotientGroup.mk' (center G)) (Subgroup.upperCentralSeries (G ⧸ center G) 1) = center G
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
⊢ ∃ s x, ∀ (i : ι), n i * f ↑s = f (x i)

Tactic:
have ⟨_⟩ := nonempty_fintype ι

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 ι
⊢ ∃ s x, ∀ (i : ι), n i * f ↑s = f (x i)
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
· grind only [iff_eq_top_or_exists, exists_normal_and_le_and_lt_top_of_ne]

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

Goal state before:
pp: case h
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
⊢ (∀ b ∈ Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m)), Prime b) ∧
    Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod n

Tactic:
refine ⟨fun x hx ↦ ?_, .trans (eq ▸ ?_) ((associated_mul_unit_left _ _ (f.map_units s)))⟩

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

case h.refine_2
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
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)
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)
a : M
⊢ (f.noncommCoprod g comm) (a, 1) = f a

Tactic:
rw [noncommCoprod_apply, map_one, mul_one]

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

Goal state before:
pp: case i_inj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a₁ ∈ Finset.univ, ∀ a₂ ∈ Finset.univ, ↑a₁ = ↑a₂ → a₁ = a₂

Tactic:
exact fun g _ g' _ => SetCoe.ext

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise Disjoint (List.map (fun l ↦ l.formPerm) p)

Tactic:
rw [List.pairwise_map]

Goal state after:
case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise (fun a b ↦ a.formPerm.Disjoint b.formPerm) p
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : a.Disjoint b
⊢ a.Disjoint b

Tactic:
exact hab

Goal state after:
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
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ (fixedBy α g)ᶜ.Finite

Tactic:
by
    refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_)
      (by simp) hg
    simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]

Goal state after:
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
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun m ↦ m • a) σ ∈ T
h : closure S ≤ stabilizer G T
⊢ a ∈ T

Tactic:
exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
⊢ Injective ⇑of

Tactic:
by
  rcases TransversalPair.nonempty G A B with ⟨d⟩
  refine Function.Injective.of_comp
    (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_
  intro _ _ h
  exact eq_of_smul_eq_smul (fun w : NormalWord d =>
    by simp_all [funext_iff, of_smul_eq_smul])

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Tactic:
ofPermHomFun_apply_of_cycleOf_mem a τ hc hm,

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) ((g ^ m) (a (↑τ c)))
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)
x : α
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
by_cases hx : x ∈ c.val.support

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)