mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace HM M
EN : Type u_3
inst✝⁴ : NormedAddCommGroup EN
inst✝³ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝² : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace HN N
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens ↑↑(locallyRingedSpace IN N).toPresheafedSpace
hxU : (ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x ∈ U
⊢ (locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
      (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
        smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    (locallyRingedSpace IN N).presheaf.germ U ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x) hxU ≫
      smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)

Tactic:
ext a

Goal state after:
𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace HM M
EN : Type u_3
inst✝⁴ : NormedAddCommGroup EN
inst✝³ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝² : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace HN N
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens ↑↑(locallyRingedSpace IN N).toPresheafedSpace
hxU : (ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x ∈ U
a : ↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U))
⊢ (CommRingCat.Hom.hom
        ((locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
          (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
            smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x))
      a =
    (CommRingCat.Hom.hom
        ((locallyRingedSpace IN N).presheaf.germ U ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x) hxU ≫
          smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)))
      a
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → AddCommGroup (V x)
inst✝³ : (x : M) → Module 𝕜 (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst✝ : Finite ι
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
t t' : (x : M) → V x
h : ∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)
this : Fintype ι := Fintype.ofFinite ι
⊢ ∑ i, (hs.coeff i x) (t x) • s i x = ∑ i, (hs.coeff i x) (t' x) • s i x

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹³ : TopologicalSpace M
inst✝¹² : ChartedSpace H M
F : Type u_5
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁹ : TopologicalSpace (TotalSpace F V)
inst✝⁸ : (x : M) → AddCommGroup (V x)
inst✝⁷ : (x : M) → Module 𝕜 (V x)
inst✝⁶ : (x : M) → TopologicalSpace (V x)
inst✝⁵ : FiberBundle F V
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
this : MDiffAt aux x
⊢ MDiffAt ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) x

Tactic:
apply this.congr_of_eventuallyEq
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrameCoeff_eq_coeff hy]

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

Goal state before:
pp: case inr.a.hab
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (r (1 : ZMod n))

Goal state after:
case e'_3
n : ℕ
hn : NeZero n
⊢ n = orderOf (r 1)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // Commute p.1 p.2 } × { p // Commute p.1 p.2 })) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
Commute,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // SemiconjBy p.1 p.2 p.2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // SemiconjBy p.1 p.2 p.2 } × { p // SemiconjBy p.1 p.2 p.2 })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // SemiconjBy p.1 p.2 p.2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // SemiconjBy p.1 p.2 p.2 } × { p // SemiconjBy p.1 p.2 p.2 })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
SemiconjBy,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // p.1 * p.2 = p.2 * p.1 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // Commute p.1 p.2 })) / ↑(Nat.card ((a : α) → i a)) ^ 2

Tactic:
Commute,

Goal state after:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // SemiconjBy p.1 p.2 p.2 }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // SemiconjBy p.1 p.2 p.2 })) / ↑(Nat.card ((a : α) → i a)) ^ 2
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // SemiconjBy p.1 p.2 p.2 }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // SemiconjBy p.1 p.2 p.2 })) / ↑(Nat.card ((a : α) → i a)) ^ 2

Tactic:
SemiconjBy,

Goal state after:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // p.1 * p.2 = p.2 * p.1 }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })) / ↑(Nat.card ((a : α) → i a)) ^ 2
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝¹ : Group W
inst✝ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < p
⊢ k + 1 < (alternatingWord i j p).length

Tactic:
by simp [h]

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

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] = alternatingWord j i (k + 1)

Tactic:
alternatingWord_succ,

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] = (alternatingWord i j k).concat i
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] = alternatingWord i j (k + 1)

Tactic:
alternatingWord_succ,

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] = (alternatingWord j i k).concat j
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Tactic:
(by ring : ↑(M i i') * 2 - (2 * k + 1) = -1 + (-k + ↑(M i i')) * 2),

Goal state after:
case inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + ↑(M.M i i')) * 2) / 2)
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
ω : List B
j : ℕ
h : j < ω.length
⊢ j < (cs.rightInvSeq ω).length

Tactic:
by simp [h]

Goal state after:
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
ω : List B
j : ℕ
h : j < ω.length
⊢ j < (cs.leftInvSeq ω).length

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m : M
⊢ ∀ ⦃a₂ : M⦄, (fun m ↦ mk m s) m = (fun m ↦ mk m s) a₂ → m = a₂

Tactic:
n

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m n : M
⊢ (fun m ↦ mk m s) m = (fun m ↦ mk m s) n → m = n
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
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < (alternatingWord i j (2 * p)).length

Tactic:
by simp [h]

Goal state after:
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
p : ℕ
i j : B
h : 0 < 2 * p
⊢ 0 < (alternatingWord i j (2 * p)).length

Tactic:
by simp [h]

Goal state after:
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
p : ℕ
i j : B
h : 0 < 2 * p
⊢ 0 < 2 * p

Tactic:
by simp [h]

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
x : DivisibleHull M
⊢ 1 • x = x

Tactic:
induction x with | mk m s
    simp [qsmul_of_nonneg zero_le_one, nnqsmul_mk]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
⊢ (archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M) = OrderHom.id

Tactic:
ext a

Goal state after:
case h₁
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ArchimedeanClass (DivisibleHull M)
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) a = OrderHom.id a
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 = g'
⊢ ∀ (φ : G →* Mˣ), φ g = φ g'

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₂
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
⊢ (archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M) = OrderHom.id

Tactic:
ext a

Goal state after:
case h₂
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ArchimedeanClass M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) a = OrderHom.id a
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤

Tactic:
simpa using c.1 q

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'
this : SemidirectProduct.rightHom.comp F' = MonoidHom.id G
⊢ ∀ (g : G), (F' g).right = g

Tactic:
exact DFunLike.ext_iff.mp this

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
x : G
⊢ ∀ (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)

Tactic:
n

Goal state after:
case right
G : Type u_1
inst✝ : Group G
x : G
n : ℕ
⊢ x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ map H.subtype (⊤.lowerCentralSeries n) = ⊥

Tactic:
top_subtype_lowerCentralSeries,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
top_subtype_lowerCentralSeries,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ H.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

Tactic:
generalize hn : Group.nilpotencyClass G = n

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⊤.lowerCentralSeries 1 = ⊥ ↔ IsMulCommutative G

Tactic:
rw [lowerCentralSeries_eq_bot_iff_upperCentralSeries_eq_top]
  exact upperCentralSeries_one_eq_top_iff

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

Goal state before:
pp: case mp
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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α → IsPreprimitive N β

Tactic:
intro _
    apply IsPreprimitive.of_surjective hf.surjective

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
⊢ IsPreprimitive G X

Tactic:
apply IsPreprimitive.of_isTrivialBlock_base a

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 = ⊤ := ⋯
⊢ ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
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
⊢ IsSimpleOrder (BlockMem G a) → IsPreprimitive G X

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 h; let h_bot_or_top := h.eq_bot_or_eq_top
    apply IsPreprimitive.of_isTrivialBlock_base a
    intro B haB hB
    rcases h_bot_or_top ⟨B, haB, hB⟩ with hB' | hB' <;>
      simp only [← Subtype.coe_inj] at hB'
    · left; rw [hB']; exact Set.subsingleton_singleton
    · right; rw [hB']; rfl

Goal state after:
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)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
apply mul_mem <;> grind [IsSwap.mul_mem_closure_three_cycles]

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
a b : α
h : a = b
⊢ 1 • a = b

Tactic:
by simp [h]

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

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
this : a ∉ Subtype.val '' t
⊢ t.ncard = (Subtype.val '' t).ncard

Tactic:
rw [Set.ncard_image_of_injective _ Subtype.coe_injective]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : ↑((ofFixingSubgroup_of_inclusion M hst) ⟨x, hx⟩) = ↑((ofFixingSubgroup_of_inclusion M hst) ⟨y, hy⟩)
⊢ ↑⟨x, hx⟩ = ↑⟨y, hy⟩

Tactic:
exact hxy

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
⊢ k = ↑g

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
hgk : ∀ (i : Fin (Fintype.card α)), (g • x) i = (k • x) i
a : α
⊢ k a = ↑g a
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
⊢ Function.Injective ⇑x

Tactic:
by exact x.2

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

Goal state before:
pp: case inr.inr.inr
α : 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' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card (Perm α)))
h : G = ⊤
⊢ ∃ g, g.IsSwap ∧ g ∈ ⊤

Tactic:
← stabilizer_univ_eq_top (Perm α) α

Goal state after:
case inr.inr.inr
α : 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' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card (Perm α)))
h : G = ⊤
⊢ ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) univ
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : 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
⊢ 4 < Nat.card α

Tactic:
rw [← Set.one_lt_ncard_iff_nontrivial] at h0

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : 1 < s.ncard
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
⊢ 4 < Nat.card α