mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case st
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ⋯
⊢ Icc 0 1 ⊆ ⇑η ⁻¹' Icc a b

Tactic:
← image_subset_iff,

Goal state after:
case st
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
⊢ ⇑η '' Icc 0 1 ⊆ Icc a b
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
⊢ ∀ x ∈ {x | IsSubmersionAt I J n f x}, ∃ t ⊆ {x | IsSubmersionAt I J n f x}, IsOpen[inst✝³] t ∧ x ∈ t

Tactic:
exact fun x hx ↦ ⟨{x | IsSubmersionAtOfComplement hx.complement I J n f x },
    fun y hy ↦ hy.isSubmersionAt,
    isOpen_isSubmersionAtOfComplement, by simp [hx.isSubmersionAtOfComplement_complement]⟩

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
n : ℕ∞ω
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 n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
⊢ ∀ {x : M}, x ∈ e.baseSet → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ e.localFrame b x_1 x)

Tactic:
intro x hx
    convert! (e.basisAt b hx).span_eq.ge
    simp [hx, basisAt]

Goal state after:
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | (g • H).Commensurable H}
hb : b✝ ∈ {g | (g • H).Commensurable H}
⊢ a✝ * b✝ ∈ {g | (g • H).Commensurable H}

Tactic:
by
    rw [Set.mem_ofPred_eq, mul_smul]
    exact trans ((commensurable_conj _).mp hb) ha

Goal state after:
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 ∈ {g | (g • H).Commensurable H}

Tactic:
by rw [Set.mem_ofPred_eq, one_smul]

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
⊢ (center G).FiniteIndex

Tactic:
by
  obtain ⟨S, -, hS⟩ := Group.rank_spec G
  exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩

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

Goal state before:
pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
⊢ e (x * y) = e x * e y

Tactic:
by_cases hxy : x = y

Goal state after:
case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : x = y
⊢ e (x * y) = e x * e y

case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ e (x * y) = e x * e y
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * r i = r i * g
⊢ r i = 1

Tactic:
have heq := sr.inj (h (sr i))
    simp_all

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
⊢ Injective simple

Tactic:
intro cs1

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 : CoxeterSystem M W
⊢ ∀ ⦃a₂ : CoxeterSystem M W⦄, cs1.simple = a₂.simple → cs1 = a₂
Module: Mathlib.GroupTheory.Coxeter.Matrix

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
by unfold Matrix.IsSymm; aesop

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
      if i = j then 1
      else
        if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4
        else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
by unfold Matrix.IsSymm; aesop

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
      if i = j then 1
      else
        if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
        else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
by unfold Matrix.IsSymm; aesop

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else m + 2).IsSymm

Tactic:
by unfold Matrix.IsSymm; aesop

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
⊢ (cs.rightInvSeq ω).getD j 1 =
    (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)

Tactic:
getD_rightInvSeq

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω) =
    (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : ⟨j✝, _w₁✝.last⟩ = x
y : (i : ι) × M i
hy : y ∈ _w₂✝.toList.head?
⊢ x.fst ≠ y.fst

Tactic:
toList_head?,

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : ⟨j✝, _w₁✝.last⟩ = x
y : (i : ι) × M i
hy : y ∈ some ⟨k✝, _w₂✝.head⟩
⊢ x.fst ≠ y.fst
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
⊢ (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹

Tactic:
simp [rightInvSeq, ih, wordProd_cons]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
⊢ (lift f) w.prod ≠ 1

Tactic:
have hnot1 : h * w.head ≠ 1 := by
    rw [← div_inv_eq_mul]
    exact div_ne_one_of_ne hnh

Goal state after:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
hnot1 : h * w.head ≠ 1
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H

Tactic:
rwa [one_mul, inv_mul_cancel_left]

Goal state after:
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
⊢ ∃ a, x = ↑a * q

Tactic:
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:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
have : FiniteIndex (center G) := ⟨hG⟩

Goal state after:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

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

Tactic:
← append_assoc

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Group.IsNilpotent ↥H

Tactic:
nilpotent_iff_lowerCentralSeries

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : Group.IsNilpotent H
⊢ Group.IsNilpotent G

Tactic:
nilpotent_iff_lowerCentralSeries

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : Group.IsNilpotent H
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons
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'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
e : b✝ ⟶ c✝
ih : F'.map (homOfPath T p) = 1
⊢ F'.map (homOfPath T (p.cons e)) = 1

Tactic:
rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]

Goal state after:
case refine_1.cons
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'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
e : b✝ ⟶ c✝
ih : F'.map (homOfPath T p) = 1
⊢ F'.map (Sum.recOn (↑e) (fun e ↦ of e) fun e ↦ inv (of e)) = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ map f (⊤.lowerCentralSeries (nilpotencyClass H)) = ⊥

Tactic:
rw [map_lowerCentralSeries, ← le_bot_iff,
    ← lowerCentralSeries_nilpotencyClass (G := H)]

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ (map f ⊤).lowerCentralSeries (nilpotencyClass H) ≤ ⊤.lowerCentralSeries (nilpotencyClass H)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a

Tactic:
rw [nilpotencyClass_of_not_nilpotent hG]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ 0 ≤ a
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) = FreeGroup.of (WeaklyConnectedComponent.mk (symgen a))

Tactic:
←
    mul_inv_eq_one

Goal state after:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ IsNilpotent (G₁ × G₂)

Tactic:
nilpotent_iff_lowerCentralSeries

Goal state after:
G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
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
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ (g, h) ∈
      ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
simp_rw [G', H', MonoidHom.mem_ker, MonoidHom.coe_prodMap, Prod.map_apply, Subgroup.mem_prod,
      Prod.one_eq_mk, Prod.ext_iff, ← MonoidHom.mem_ker, QuotientGroup.ker_mk']

Goal state after:
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
⊢ IsNilpotent ((i : η) → Gs i)

Tactic:
nilpotent_iff_lowerCentralSeries

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
⊢ ∃ n, ⊤.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 η
⊢ IsNilpotent ((i : η) → Gs i)

Tactic:
nilpotent_iff_lowerCentralSeries

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 η
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.GroupAction.Blocks

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

Tactic:
← Group.preimage_smul_setₛₗ,

Goal state after:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ g₂ • ⇑j ⁻¹' B
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (g₂ • ⇑j ⁻¹' B)
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'
⊢ (g * h * g⁻¹ * g) • B = g • h • B

Tactic:
smul_smul g h B,

Goal state after:
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'
⊢ (g * h * g⁻¹ * g) • B = (g * h) • B
Module: Mathlib.GroupTheory.Perm.ConjAct

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

Tactic:
ext
  rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]

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
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'
⊢ b ∈ g • B'

Tactic:
exact hb'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
a✝ : Nontrivial α
hα' : Nat.card α = 2
⊢ Nat.factorial 2 = 2

Tactic:
Nat.factorial_two

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
a✝ : Nontrivial α
hα' : Nat.card α = 2
⊢ 2 = 2
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inr.left
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
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
rw [← ofStabilizer.isMultiplyPretransitive]

Goal state after:
case inr.left
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
⊢ IsMultiplyPretransitive M α n.succ
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case succ
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)
⊢ (fixingSubgroup (↥(stabilizer G a)) t).index * (stabilizer G a).index * (Nat.card α - (k + 1))! = (Nat.card α)!

Tactic:
have htcard : t.ncard = k := by
      rw [← Nat.succ_inj, Nat.succ_eq_add_one, Nat.succ_eq_add_one, ← hs, hat', eq_comm]
      suffices ¬ a ∈ (Subtype.val '' t) by
        convert! Set.ncard_insert_of_notMem this ?_
        · rw [Set.ncard_image_of_injective _ Subtype.coe_injective]
        apply Set.toFinite
      intro h
      obtain ⟨⟨b, hb⟩, _, hb'⟩ := h
      apply hb
      simp only [← hb', Set.mem_singleton_iff]

Goal state after:
case succ
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)
htcard : t.ncard = k
⊢ (fixingSubgroup (↥(stabilizer G a)) t).index * (stabilizer G a).index * (Nat.card α - (k + 1))! = (Nat.card α)!