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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ (x.1, 1) * (1, x.2) = x

Tactic:
Prod.fst_mul_snd

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ x = x
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
by
  rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift,
    range_sigma_eq_iUnion_range, Submonoid.closure_iUnion]
  simp +instances only [MonoidHom.mclosure_range]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈
      (↑(consRecOn (cons g tail h1 h2) ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
simp only [consRecOn_cons]

Goal state after:
case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈
      (↑(if ij : j = k then ⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩
            else ⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t

Tactic:
unfold IsRightInversion
  simp only [mul_assoc, ht.mul_self, mul_one, ht, true_and, not_lt]
  constructor
  · exact le_of_lt
  · exact (lt_of_le_of_ne' · (ht.length_mul_left_ne w))

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i

Tactic:
rw [isRightDescent_iff, not_isRightDescent_iff, simple_mul_simple_cancel_right]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 =
    rcons
      (have __src := { head := 1, tail := ls, fstIdx_ne := ?m.39 };
      { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.39 }.head, tail := __src.tail, fstIdx_ne := ⋯ })

Tactic:
simp [cons, rcons, h2]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.nil
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) × M i
hi :
  ∀ (hnot1 : ∀ l ∈ [], l.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []),
    { toList := [], ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := [], ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l ∈ [x], l.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ [], x.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) [x]
h : { toList := [x], ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := [x], ne_one := hnot1✝, chain_ne := hchain }.toList

pp: case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)),
    { toList := y :: l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain }.toList

Tactic:
· refine ⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩
      simp [toWord]

Goal state after:
case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)),
    { toList := y :: l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain }.toList
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b ↑H ↑K) (doubleCoset a ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K

Tactic:
have ha : a ∈ doubleCoset b H K := mem_doubleCoset_of_not_disjoint h

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b ↑H ↑K) (doubleCoset a ↑H ↑K)
ha : a ∈ doubleCoset b ↑H ↑K
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑H ↑⊥) a b ↔ (QuotientGroup.rightRel H) a b

Tactic:
rw [rel_iff, QuotientGroup.rightRel_apply]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_1.e'_3
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑t • m = (↑s * ↑t) • ↑t' • m'

Tactic:
simp_rw [smul_smul, mul_rotate s'.val, ← smul_smul, h, smul_smul]
    ring_nf

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c

Tactic:
simp_rw [qsmul_of_nonneg ha.le]

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ ⟨a, ⋯⟩ • b < ⟨a, ⋯⟩ • c
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
g g' : G
h : ∀ (φ : G →* Mˣ), φ g = φ g'
⊢ g = g'

Tactic:
simpa [← not_forall, not_imp_not, mul_inv_eq_one, h] using
    exists_apply_ne_one_of_hasEnoughRootsOfUnity G M (a := g * g'⁻¹)

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : Subgroup (G →* Mˣ)
g : G
⊢ g ∈
      (OrderIso.symm
          { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
            invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
            left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ })
        (OrderDual.toDual Φ) ↔
    ∀ φ ∈ Φ, φ g = 1

Tactic:
OrderIso.symm_mk,

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : Subgroup (G →* Mˣ)
g : G
⊢ g ∈
      {
          toEquiv :=
            { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
                invFun := fun Φ ↦
                  (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
                left_inv := ⋯, right_inv := ⋯ }.symm,
          map_rel_iff' := ⋯ }
        (OrderDual.toDual Φ) ↔
    ∀ φ ∈ Φ, φ g = 1
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ (FreeGroup.map f).ker.IsFinitelyNormallyGenerated

Tactic:
rw [(FreeGroup.map f).ker_eq_bot (FreeGroup.map_injective hf_inj.injective)]

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ ⊥.IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
else

Goal state after:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ SemidirectProduct.rightHom.comp F' = MonoidHom.id G

Tactic:
apply IsFreeGroup.ext_hom (fun x ↦ ?_)

Goal state after:
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
x : IsFreeGroup.Generators G
⊢ (SemidirectProduct.rightHom.comp F') (IsFreeGroup.of x) = (MonoidHom.id G) (IsFreeGroup.of x)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.18
inst✝ : Monoid X
f : End (root' T) →* X
⊢ ∀ (X_1 : G), f (loopOfHom T (𝟙 X_1)) = 𝟙 ()

Tactic:
by
    intro a
    dsimp only [loopOfHom]
    rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]

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 (Prod.fst ∘ ⇑I'.subtype)

Tactic:
simp only [← MonoidHom.coe_fst, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']

Goal state after:
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
⊢ map (MonoidHom.fst ↥G' ↥H') (P.prod Q).range = ⊤
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case pos
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = 1

Tactic:
loopOfHom_eq_id T e h,

Goal state after:
case pos
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ E (𝟙 (root' T)) = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h : Group.IsNilpotent G
n : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ derivedSeries G n ≤ ⊤.lowerCentralSeries n

Tactic:
exact derived_le_lower_central n

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
hcq : Nat.card (G ⧸ center G) < Nat.card G
hnq : Group.IsNilpotent (G ⧸ center G)
⊢ Group.IsNilpotent G

Tactic:
exact of_quotient_center_nilpotent hnq

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
hG0,

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = minFac 0
hG0 : Nat.card G = 0
⊢ H.Normal
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«0»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 0 < 2
key : B.ncard * 0 = Nat.card X
⊢ B = Set.univ

pp: case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard * 1 = Nat.card X
⊢ B = Set.univ

Tactic:
· rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key
    exact (IsEmpty.exists_iff.mp hB_ne).elim

Goal state after:
case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard * 1 = Nat.card X
⊢ B = Set.univ
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 B

Tactic:
← IsTrivialBlock.smul_iff g

Goal state after:
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)
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
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B

Tactic:
← IsTrivialBlock.smul_iff g

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mpr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsPreprimitive G X → IsSimpleOrder (BlockMem G a)

Tactic:
intro hGX'; apply IsSimpleOrder.mk
    rintro ⟨B, haB, hB⟩
    simp only [← Subtype.coe_inj]
    cases hGX'.isTrivialBlock_of_isBlock hB with
    | inl h =>
      simp [BlockMem.coe_bot, h.eq_singleton_of_mem haB]
    | inr h =>
      simp [BlockMem.coe_top, h]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ (alternatingGroup α).index = 1

Tactic:
rw [Subgroup.index_eq_one]; apply Subsingleton.elim

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
⊢ x = g⁻¹ • a → x = a

Tactic:
intro hgx

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
⊢ x = a
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : (conjMap hg) ⟨x, hx⟩ = (conjMap hg) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simp only [Subtype.mk_eq_mk]

Goal state after:
case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : (conjMap hg) ⟨x, hx⟩ = (conjMap hg) ⟨y, hy⟩
⊢ x = y
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:
hσ.card_support

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ).IsThreeCycle
hτ : (↑τ).IsThreeCycle
h5 : 5 ≤ card α
⊢ 3 + 2 ≤ card α
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)
⊢ a ∉ Subtype.val '' t

Tactic:
exact notMem_val_image M t

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 α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
⊢ IsMultiplyPreprimitive M α n ↔ IsMultiplyPreprimitive N β n

Tactic:
refine ⟨IsMultiplyPreprimitive.of_bijective_map hf, ?_⟩

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 : ℕ
⊢ IsMultiplyPreprimitive N β n → IsMultiplyPreprimitive M α n
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ ∃ g ∈ stabilizer (Perm α) sᶜ, g.IsThreeCycle

Tactic:
exact exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard (by grind)

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c : 1 < sᶜ.encard
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
obtain ⟨g, hg, hg'⟩ := this sᶜ h1c
    use g, hg
    rw [stabilizer_compl] at hg'
    exact hG.le hg'

Goal state after: