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

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
⊢ Function.Injective ⇑(FreeGroup.lift a)

Tactic:
have : FreeGroup.lift a =
      (CoprodI.lift fun i => FreeGroup.lift fun _ => a i).comp
        (@freeGroupEquivCoprodI ι).toMonoidHom := by
    ext i
    simp

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
this : FreeGroup.lift a = (lift fun i ↦ FreeGroup.lift fun x ↦ a i).comp freeGroupEquivCoprodI.toMonoidHom
⊢ Function.Injective ⇑(FreeGroup.lift a)
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
⊢ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * q * y

Tactic:
obtain ⟨a, ha⟩ : ∃ a : H, x = a * q := by
    obtain ⟨a, ha⟩ : ∃ a : H, a * x = q := Quotient.eq.mp hx
    exact ⟨⟨a⁻¹, by simp⟩, eq_inv_mul_of_mul_eq ha⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : x = ↑a * q
⊢ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * q * y
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ_surj : Function.Surjective ⇑φ
hφ_ker : φ.ker.IsFinitelyNormallyGenerated
⊢ (Subgroup.comap φ f.ker).IsFinitelyNormallyGenerated

Tactic:
exact hf_ker.comap hφ_surj hφ_ker

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hg : IsFinitelyPresented G
⊢ ∃ n s, s.Finite ∧ Nonempty (G ≃* PresentedGroup s)

Tactic:
obtain ⟨n, φ, hφ, s, hs, hsφ⟩ := hg

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ : Function.Surjective ⇑φ
s : Set (FreeGroup (Fin n))
hs : s.Finite
hsφ : Subgroup.normalClosure s = φ.ker
⊢ ∃ n s, s.Finite ∧ Nonempty (G ≃* PresentedGroup s)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Finite ↥(_root_.commutator G)

Tactic:
by
  have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
  refine Nat.finite_of_card_ne_zero fun h => ?_
  rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2
  exact FiniteIndex.index_ne_zero (eq_zero_of_pow_eq_zero h2)

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩ ∈ H.focalSubgroupOf

Tactic:
rw [focalSubgroupOf_def, mem_subgroupOf]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ↑(⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩) ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α × Bool
⊢ reduceCyclically [a] = [a]

Tactic:
by
  simp [reduceCyclically]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a b : α × Bool
L : List (α × Bool)
⊢ reduceCyclically (a :: (L ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically L else a :: L ++ [b]

Tactic:
by
  simp [reduceCyclically]

Goal state after:
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 * x✝⁻¹ * y⁻¹ ∈ N ↔ x✝ * y * (x✝⁻¹ * y⁻¹) ∈ N

Tactic:
mul_assoc

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: 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)

Tactic:
MonoidHom.comp_apply,

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 (F' (IsFreeGroup.of x)) = (MonoidHom.id G) (IsFreeGroup.of x)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n

Tactic:
rw [top_subtype_lowerCentralSeries]
  exact lowerCentralSeries_mono n le_top

Goal state after:
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
⊢ ‖g' y - g' x‖ * ‖w‖ * ‖w‖ + ((g' x) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' x) w) w

Tactic:
mul_assoc

Goal state after:
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
⊢ ‖g' y - g' x‖ * (‖w‖ * ‖w‖) + ((g' x) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' x) w) w
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ (pi Set.univ fun i ↦ ⊤.lowerCentralSeries n) = ⊥

Tactic:
pi_eq_bot_iff

Goal state after:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ (pi Set.univ fun i ↦ ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i))) = ⊥

Tactic:
pi_eq_bot_iff

Goal state after:
case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∀ (i : η), ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
⊢ H = ⊤

Tactic:
have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective

Goal state after:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
⊢ H = ⊤
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.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
· apply Or.intro_right; simp only [hB]; apply Set.preimage_univ

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

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

Tactic:
exact IsTrivialBlock.smul H 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 : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ ↑h' • g • B = g • h • B

Tactic:
rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ ConjAct.ofConjAct k⁻¹ • a✝ ∈ g.support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support

Tactic:
ConjAct.ofConjAct_inv,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a✝ : α
⊢ (ConjAct.ofConjAct k)⁻¹ • a✝ ∈ g.support ↔ a✝ ∈ ConjAct.ofConjAct k • g.support
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
← smul_eq_iff_eq_inv_smul

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
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 : α
hgx : x = g⁻¹ • a
⊢ a = g⁻¹ • a

Tactic:
← smul_eq_iff_eq_inv_smul

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
⊢ g • a = a
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
⊢ ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
induction n with intro l hl hn
  | zero => simp [List.length_eq_zero_iff.1 hn, one_mem]
  | succ n ih =>
    rw [Nat.mul_succ] at hn
    obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.length_cons, Nat.succ_inj] at hn
    obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.prod_cons, List.prod_cons, ← mul_assoc]
    apply mul_mem <;> grind [IsSwap.mul_mem_closure_three_cycles]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ closure {g | (↑g).IsThreeCycle} = ⊤

Tactic:
by
  rw [← map_subtype_inj, MonoidHom.map_closure]
  have : (alternatingGroup α).subtype '' _ = {g : Perm α | IsThreeCycle g} :=
    Subtype.coe_image_of_subset isThreeCycle_subset_alternatingGroup
  aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ (2 * 1).succ ≤ (Nat.card α).factorial

Tactic:
exact le_trans h3 (Nat.card α).self_le_factorial

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 α
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'
⊢ Disjoint s t'

Tactic:
· apply disjoint_val_image

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

Goal state before:
pp: case inr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = ↑n
m : ℕ
hm : n = Nat.succ 0 + m
hs' : s.encard = ↑m
this : Finite ↑s
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2

Tactic:
apply ofFixingSubgroup.isMultiplyPretransitive (G := M) s (n := n.succ)

Goal state after:
case inr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = ↑n
m : ℕ
hm : n = Nat.succ 0 + m
hs' : s.encard = ↑m
this : Finite ↑s
⊢ s.ncard + 2 = n.succ
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: 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)ᶜ
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
rw [MulAction.isPretransitive_iff_base (⟨a, ha'⟩ : ofFixingSubgroup M (s ∩ g • s))]

Goal state after:
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 : ↥(ofFixingSubgroup M (s ∩ g • s))), ∃ g_1, g_1 • ⟨a, ha'⟩ = x
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 α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ B = univ

Tactic:
suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    rw [← Set.ncard_add_ncard_compl s]
    lia

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
hB' : ¬B.Subsingleton
⊢ sᶜ ⊆ B
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
n : ℕ
s : ↑(powersetCard α n)
⊢ stabilizer G s = stabilizer G ↑s

Tactic:
by
  ext g
  simp [mem_stabilizer_iff, ← Subtype.coe_inj, ← coe_inj]

Goal state after:
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 α
s : Finset α
hs : s ∈ powersetCard α n
⊢ Fintype.card ?m.29 = n

Tactic:
Fintype.card_fin

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
⊢ ?m.38 = n

G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
⊢ ℕ
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 α < 3
⊢ G = ⊤

Tactic:
rw [Nat.lt_succ_iff] at hα3
    apply Subgroup.eq_top_of_card_eq
    simp only [Nat.card_eq_fintype_card]
    apply le_antisymm (Fintype.card_subtype_le _)
    rw [← Nat.card_eq_fintype_card, Nat.card_perm]
    refine le_trans (Nat.factorial_le hα3) ?_
    rw [Nat.factorial_two]
    have : Nonempty G := One.instNonempty
    apply Nat.le_of_dvd Fintype.card_pos
    rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
    exact orderOf_dvd_card

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : normalizer ↑H = ⊤
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
normalizer_eq_top_iff

Goal state after:
case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : H.Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_3
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : P
⊢ x ∈ f.range ⊓ g.range → x ∈ ⊥

Tactic:
⟨⟨y, hy⟩, z, hz⟩

Goal state after:
case refine_3
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)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : P
y : M
hy : f y = x
z : N
hz : g z = x
⊢ x ∈ ⊥
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ t⁻¹ * of ↑⟨g✝, ⋯⟩ * (t * ReducedWord.prod φ w✝.toReducedWord) =
    t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))

Tactic:
mul_assoc

Goal state after:
case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ t⁻¹ * (of ↑⟨g✝, ⋯⟩ * (t * ReducedWord.prod φ w✝.toReducedWord)) =
    t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (g * k * k⁻¹).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset

Tactic:
mul_assoc

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (g * (k * k⁻¹)).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset